Stream: VsCoq devs & users

Topic: VSCoq Headline highlighting


view this post on Zulip Michael Soegtrop (Nov 11 2021 at 15:52):

I wonder if VSCoq has an option to highlight the old style coqdoc headline comments. (** * 1 *) (** ** 2 *)and so on. Or is there a new format? I get lost in my own files without this ;-)

view this post on Zulip Bas Spitters (Nov 10 2022 at 15:20):

I'm not sure if this is what @Michael Soegtrop meant, but I'm curious whether it is possible to show coqdoc in vscoq in the style of jscoq.
I don't know whether vscode has such functionality for other languages.

view this post on Zulip Michael Soegtrop (Nov 10 2022 at 15:50):

I don't care that much about the source format and the nature of the highlighting - I can adopt. But some highlighting would be helpful!

view this post on Zulip Bas Spitters (Nov 15 2022 at 12:31):

My students suggested that one may be able to obtain functionality such as for jscoq by using some of the technology that is used for the Jupyter notebooks:
https://code.visualstudio.com/docs/datascience/jupyter-notebooks


Last updated: Jan 30 2023 at 18:04 UTC