Syntax Highlighting

[banacorn]

• General Syntax Highlighting (by language-agda)
• Custom Syntax Highlighting (generated dynamically by Agda per source)

[ajrouvoet]

+1 How is this supposed to work? I don't have syntax highlighting after type checking on a fresh atom 1.0.0 installation with agda-mode.

[banacorn]

Please install language-agda for general syntax highlighting, I suppose this is what you are looking for : )

Syntax highlighting is usually handled by language-blahblah in Atom

[ajrouvoet]

No I understood that part; sorry for not being clear. I actually wanted to know about the agda type-driven syntax highlight that requires agda to compile the source.

[banacorn]

Agda sends syntax highlighting informations every time when the file is loaded, which looks something like this:

(agda2-highlight-add-annotations '(59 65 (keyword) nil) '(66 70 (module) nil ("/Users/banacorn/agda/test/Test.agda" . 1)) '(71 76 (keyword) nil))

But currently only terminationproblem and unsolvedmeta are highlighted, and other tokens are ignored, mostly for performance concerns (okay maybe it's just because I'm too lazy XD)

I'm not sure if there's any other way (other than Markers) to do the highlighting, but recently they've optimized the markers a bit, maybe it worths trying.

[ajrouvoet]

I'm not sure how it's done in Emacs, but it's not uncommon for the syntax highlight to be slightly off while editing before you compile again (e.g. a function name colored in 2 colors); so I'm not sure that emacs really does a big effort to track highlighted regions when the file changes.

[banacorn]

I believe that Emacs simply erase all highlightings and repaint them again with the annotations sent from Agda, the same can be done in Atom, too.