Hi! I ran into the same problem (solved it with a crude Python script here...) and would also greatly appreciate such a feature and other improvements to the HTML output!
By the way, seeing your solution, I would suggest to rather attach the id-attributes to the tags surrounding the defined names, which enables CSS :target highlighting. (To see what it looks like in our solution: https://coupledsim.bbisping.de/isabelle/Coupled_Simulation.html#coupled_sim_by_eq_coupled_delay_simulation ) Kind Regards, Ben Am Montag, den 18.03.2019, 12:25 +0000 schrieb 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 > > > _______________________________________________ > isabelle-dev mailing list > isabelle-...@in.tum.de > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
