whonore / Coqtail

Interactive Coq Proofs in Vim
MIT License
274 stars 34 forks source link

Add elpi support #278

Closed Lysxia closed 2 years ago

Lysxia commented 2 years ago
whonore commented 2 years ago

Thanks, this looks good overall. I was initially concerned that using { twice in a row to focus the goal is valid (if unidiomatic) Coq, so skipping over it might break that use case. But it seems that's not a problem because _skip_br2 is only triggered after we check for braces in _find_next_sequence, so it will only skip something like lp:{{.

This seems to work, but it's a bit fragile if the parsing code ever gets refactored, and it seems like there could potentially still be issues if someone uses {{ in a notation. I don't know much about Elpi, but if it's true that the top level quoting always starts with lp:{{ then I think it would be better to make a _skip_elpi function that's defined like so:

return _skip_block(lines, sline, scol, b"lp:{{", b"}}", {b"{{": _skip_br2})

This way at the top level we only try to skip double braces with a leading lp:, but inside it still ignores matched {{/}} pairs to avoid closing the block prematurely. Does that seem reasonable to you?

Could you also add a couple test cases to _parse_tests in tests/unit/test_parse.py?

Lysxia commented 2 years ago

Indeed, toplevel elpi blocks all start with lp:{{ so we can use that as a more accurate delimiter. I'll also add some tests.