Hacking the Agda HTML back end - part 2

Last night I had the thought that I should just modify the Interface data structure and add a map from declaration names to highlighting info.

I’ve just modified the Interface data structure and done all the necessary plumbing so that now we have a field called iDeclHighlighting :: Map QName [Aspects].

I add to this data structure inside function Agda.Interaction.Highlighting.Generate.generateAndPrintSyntaxInfo.

I am just about to test it on Permutations.agda and traceShow the output. I’m getting excited.

It basically worked! Along the way I discovered that the HighlightingInfo data structure doesn’t actually contain any of the text of the program, just character ranges and “aspects”.

So I have completed a new implementation where I store iDeclRanges :: Map QName Range in the Interface data structure instead.

For a given declaration I can then find the (min, max) of the range using a function called coveringRange. Inside the HTML backend the Agda source file is transformed into a token stream of type [TokenInfo]. We can easily filter out the tokens that are outside the “covering range”.

Thus, we highlight the Agda source file once and then cut snippets out of it and then render these to HTML.

A commit of this proof of concept can be found here.