[isabelle-dev] HTML output

[Bisping, Benjamin]

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-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev