Skip to content

Add launch.json and prettify#1

Merged
fizruk merged 6 commits intorzk-lang:mainfrom
fredrik-bakke:main
May 29, 2023
Merged

Add launch.json and prettify#1
fizruk merged 6 commits intorzk-lang:mainfrom
fredrik-bakke:main

Conversation

@fredrik-bakke
Copy link
Copy Markdown
Contributor

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
Copy link
Copy Markdown
Contributor Author

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

@fredrik-bakke
Copy link
Copy Markdown
Contributor Author

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

@fredrik-bakke
Copy link
Copy Markdown
Contributor Author

fredrik-bakke commented May 27, 2023

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
Copy link
Copy Markdown
Member

fizruk commented May 27, 2023

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
Copy link
Copy Markdown
Contributor Author

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
Copy link
Copy Markdown
Member

fizruk commented May 27, 2023

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

@fredrik-bakke
Copy link
Copy Markdown
Contributor Author

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
Copy link
Copy Markdown
Contributor Author

Maybe we can talk a bit then?

@fizruk
Copy link
Copy Markdown
Member

fizruk commented May 29, 2023

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.

@fizruk fizruk changed the title Define "Literate rzk Markdown" format Add launch.json and prettify May 29, 2023
@fizruk fizruk merged commit e56299b into rzk-lang:main May 29, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants