Zulip Chat Archive

Stream: metaprogramming / tactics

Topic: parse string literal


view this post on Zulip Patrick Massot (Jan 24 2021 at 13:32):

This looks like a really stupid question but I can't find the answer myself. How do I parse a string literal as an argument to user command?

view this post on Zulip Rob Lewis (Jan 24 2021 at 13:38):

You can parse an expr and evaluate it as a string. See e.g. src#localized_cmd

view this post on Zulip Patrick Massot (Jan 24 2021 at 14:02):

Great thanks! I think this deserves a dedicated parser, but this trick will do.


Last updated: May 09 2021 at 23:10 UTC