[isabelle-dev] HTML output

[Haslbeck, Maximilian]

Hi,

In one of our recent papers we provided direct links to the corresponding Isabelle definitions, lemmas, etc (for example [1]). The anchors inside Isabelle’s HTML output were added with a very crude shell script with multiple invocations of sed.

So it would be great if the necessary id tags (and other semantic information) could be added by Isabelle itself. I’m willing to implement this myself but I would need some general pointers in the right direction. I’m guessing I can implement this with Isabelle/Scala, right?

Gruß
Max

[1] <http://cl-informatik.uibk.ac.at/isafor/experiments/lll/browser_info/AFP/LLL_Basis_Reduction/LLL_GSO_Impl.html#def:basis_reduction_main>