Bas Spitters (Apr 11 2021 at 16:05): Bas Spitters (Apr 11 2021 at 16:05):Proof General is great, and emacs is quite capable of showing images.
Would there be any way of including images in literate Coq code?
Company-coq already replaces coq's ascii art by math-symbols.
Perhaps a similar thing is possible with symbol strings in comments. E.g.
(** Coq is great.
PNG: Rooster.png
*)
I don't know what the syntax should be. @Clément Pit-Claudel ?
Clément Pit-Claudel (Apr 11 2021 at 16:07):Yup, it's very easy to include images in an Emacs buffer. You can do what you suggest with a font-lock rule. I can write an example if you want.
Bas Spitters (Apr 11 2021 at 16:12):Yes, please!
Notification Bot (Oct 24 2021 at 21:35):This topic was moved here from #User interfaces devs & users > Pictures in Proof General/emacs by Karl Palmskog
Last updated: Apr 20 2024 at 10:02 UTC