Michael Soegtrop (Nov 11 2021 at 15:52): 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 ;-)
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.
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!
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: Jun 04 2023 at 23:30 UTC