Li-yao (Apr 04 2022 at 22:47): Li-yao (Apr 04 2022 at 22:47):It seems that lp:{{ blocks can be terminated in the same line as a % comment, and braces {{ can be nested in such comments:
From elpi Require Import elpi.
Elpi Program w lp:{{
% {{
% }} }}.
How is the end of an antiquotation determined exactly? I'm adding elpi support to coqtail and I'm not sure how to understand this corner case. I'm currently just ignoring the rest of the line after a % but that's not what the Coq/elpi parser is doing.
Enrico Tassi (Apr 05 2022 at 06:37):You have to think that in order to find the end, you don't need the elpi parser. Coq has to parse the string without calling elpi, so % is no different than, say, x. just count for {{ and }}.
Then I believe it is a bit smarter than that, as in you can start with any number of { and the end is when you find the same. But for example vscoq does not understand that.
Enrico Tassi (Apr 05 2022 at 06:39):https://github.com/coq/coq/blob/f2bf445b8f4f5241ebdc348b69961041b4e57883/parsing/cLexer.ml#L542
Last updated: Oct 13 2024 at 01:02 UTC