Add launch.json and prettify

rzk-lang / vscode-rzk

Visual Studio Code Extension(s) for Rzk proof assistant.

https://marketplace.visualstudio.com/items?itemName=NikolaiKudasovfizruk.rzk-1-experimental-highlighting

Other

8 stars 1 forks source link

Add launch.json and prettify #1

Closed fredrik-bakke closed 1 year ago

fredrik-bakke commented 1 year ago

Summary

Define the "Literate rzk Markdown" format for .rzk.md files. This is useful, as having a separate "Literate rzk Markdown" format allows users to define settings for .rzk.md files apart from their .md settings.
Add a .vscode/launch.json file for convenient debugging.
Some scope changes

fredrik-bakke commented 1 year ago

Ah, shoot! I see you've just pushed this yourself 🤦‍♂️

fredrik-bakke commented 1 year ago

There are some other additions in this PR as well, however. Maybe have a look and see if you find anything useful?

fredrik-bakke commented 1 year ago

Also, while I'm here: in my VSCode Agda syntax highlighting extension, I found using YAML instead of JSON grammar files to be most helpful, as they require about half as many lines of code, and also you can usually get away with fewer escaped characters in your regexes. Moreover, I use Jinja2 templates to reduce code duplication. I would be happy to submit a PR adding this functionality to your extension as well if you want.

fizruk commented 1 year ago

Thank you and sorry for being slightly faster, I did not think someone else would try to do it :)

I will check current version of your PR and merge it.

There is one thing that I don't know yet how to fix: *.md files have Markdown Preview, but *.rzk.md do not anymore. Markdown Preview is useful when I insert SVG diagrams in the markdown files (e.g. see Associativity section for Segal Types). If you have ideas or you would like to submit a PR — it would be most welcome! :)

Also, it would be nice to have literate Rzk LaTeX support. Although rzk does not support literate *.rzk.tex files yet (but it's not difficult to add), I've used it already with the minted package (see here).

Regarding YAML — I do not have a strong opinion here, I will get back to you about it a bit later.

fredrik-bakke commented 1 year ago

Ah, I have some code for literate latex that I can copy over! Also, regarding YAML+Jinja2 vs. JSON, it may be instructive to compare these two files: agda.tmLanguage.j2.yml and agda.tmLanguage.json. Regarding Markdown preview, I don't know how to make this work with the built-in preview function. There is however a "Markdown Preview Enhanced" extension that works just fine. Though this isn't the cleanest solution...

fizruk commented 1 year ago

I have installed Markdown Preview Enhanced (this one), but it does not seem to work for .rzk.md files on my machine.

fredrik-bakke commented 1 year ago

Sorry, I'll be on vacation for the next week. But I'll be back the week after that and pull the latex highlighting code! (And hopefully learn a bit of rzk)

fredrik-bakke commented 1 year ago

Maybe we can talk a bit then?

fizruk commented 1 year ago

Absolutely! I haven't merged this PR yet, because I get a weird error locally, but I'm unsure if it's actually related to the PR. I will double check soon and merge.