Syntax highlighting for HOL

[digama0]

We need at least the following syntax highlighters:

• Github (TextMate grammar via linguist)
• Zulip (Pygments)
• Vim
• Emacs

hol4-vscode has a TextMate grammar which can be reused for github.

[mn200]

The existing code for emacs highlights “outer syntax” but does not attempt to deal with inner/logical syntax at all. The emacs mode makes an effort to understand inner syntax to support automatic indentation but doesn't have access to the HOL parser/grammar so it will only be an approximation if users do a lot of violence to the "default".

[RedCMD]

here's my VSCode extension to help with authoring TextMate grammars https://marketplace.visualstudio.com/items?itemName=RedCMD.tmlanguage-syntax-highlighter

[dnezam]

For Emacs and Vim, I think a tree-sitter grammar could be useful, as my understanding is that it can also help with navigation and indentation.

In my last (misguided) attempt, I tried to model the inner syntax, but I think it would be much more useful to only deal with antiquotes for that. Matthew Fluet already has a tree-sitter grammar for Standard ML at tree-sitter-sml, so one could take that as a basis and add all the HOL features to it. The HOLParser.sml and HOLAst.sml files that are currently living on the holyml-parser branch may be useful.

The "existing" tree-sitter files in the repo are based on tree-sitter-sml and my early (mis)understandings of HOL; from my point of view, those files can be thrown out and someone can start fresh (perhaps me in the future once we get holyml-parser merged :))