search

cpitclaudel / alectryon

A collection of tools for writing technical documents that mix Coq code and prose.
MIT License
227 stars 36 forks source link

pygment style for elpi #61

Closed gares closed 3 years ago

gares commented 3 years ago

This works for me, but it is the ugliest option we discussed by mail. I tried the other options, but I could not get it working :-/

Given the entry point is really small, I wonder if "monkey patching" could be an option. I mean, the _quotation and antiquotation non terminals could be there and empty, and one could inject all the rest (and keep it out of alectryon, which is probably a good thing, unless you like elpi so much).

gares commented 3 years ago

This is a screenshot of how it looks like with this patch plus a bunch of CSS rules. The think is very very close to how it looks in vscode, which was my objective.

Screenshot from 2021-08-21 12-05-45

cpitclaudel commented 3 years ago

This looks very nice, thanks for sharing!

Given the entry point is really small, I wonder if "monkey patching" could be an option. I mean, the _quotation and antiquotation non terminals could be there and empty, and one could inject all the rest (and keep it out of alectryon, which is probably a good thing, unless you like elpi so much).

But if that works, then wouldn't it work to also inject the nonterminals?

gares commented 3 years ago

I did not try but yes. I was suggesting to keep a quotation and antiquotation nonterminals because they could/should be used by ltac1 and ltac2 as well. I mean ltac:(...) is really like lp:{{ ... }}.

cpitclaudel commented 3 years ago

they could/should be used by ltac1 and ltac2 as well. I mean ltac:(...) is really like lp:{{ ... }}.

Fair, although ltac1 can contain Gallina in a bunch of places, so it's tricky to know when you exit the quotation (that's why I handle both together at the moment).

gares commented 3 years ago

I managed to separate the elpi lexer in this way (I pushed it ontop of the other PR because I wanted to test it on the actual doc).

https://github.com/cpitclaudel/alectryon/pull/56/commits/7c226b6f5944834579eb1a1a33ff5a2270e2dff3

I could not monkey patch all the way trough, so I'd like the --plugin option (or another one) to let me override the coq lexer as I do here.

gares commented 3 years ago

I close this one, since what I really need now is an "plugin mechanism" hence the other PR is more appropriate to discuss it.