Syntax highlighting constants in a term

[aqjune]

I am thinking about a syntax highlighting feature that adds a font color for constants in HOL Light terms.

I can imagine are two possible approaches for this:
(1) adding 'get the term structure' query to the HOL Light server letting the VSCode plugin send & receiving the result to highlight it
(2) writing a simple term parser in the VSCode plugin & analyzing it, without updating the server

It seems there are pros and cons here: (1) makes the server more complex, whereas (2) will return less accurate result.
Which feature do you think is better?

[maggesi]

Which feature do you think is better?

I use HOL Light in my courses at the university.
I think (1) is much better for students, since (2) can generate confusion.

[monadius]

Do you want to get something like this (SUC is highlighted with a different color):

It is possible to implement this feature using a semantic token provider. The main issue is how to parse HOL Light terms and build semantic tokens. Writing a simple parser in the extension itself is not a good option because it is not possible to parse user-defined constants or user-defined parser extension (such as custom operators).

One approach is to write a parser in OCaml and then invoke this parser for all terms which need to be highlighted (this is your approach (1)). Another option is to use a hybrid approach: parse everything in the extension but get all information which is required for parsing terms from the server (all defined constants, custom operators, etc.).

I prefer to parse everything in OCaml because it seems to be easier to extend an OCaml parser with new features (it can invoke HOL Light functions directly). Do you plan to write a prototype parser? Initially, it could be something very simple: Highlight all words which match some defined constants (it will not parse terms like !SUC. SUC correctly).