Stream: Proof General users

Topic: Pictures in Proof General/emacs

view this post on Zulip 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 ?

view this post on Zulip 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.

view this post on Zulip Bas Spitters (Apr 11 2021 at 16:12):

Yes, please!

view this post on Zulip 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: Feb 06 2023 at 05:03 UTC