Email Gateway (Aug 19 2022 at 09:46): Email Gateway (Aug 19 2022 at 09:46):From: John Wickerson <jpw48@cam.ac.uk>
Dear Isabelle,
My theory imports various theories not made by me, such as Quotient_Set, Quotient_Syntax, and so on. When I do "isabelle build" (on Isabelle2013-RC1), the generated pdf includes only those theories for which I did not specify [document = false] in my ROOT file.
However, the generated html pages include all the theories together. I would like to have just my theories listed on the index.html page, and any references to third-party theories linking to their respective pages at http://isabelle.in.tum.de/library/HOL/. Could somebody kindly explain how to achieve this?
Best wishes,
john
Email Gateway (Aug 19 2022 at 09:46):From: John Wickerson <jpw48@cam.ac.uk>
On a related topic, I find some symbols are not pretty-printed in the html output. For instance, each occurrence of \<oplus> comes out nicely as ⊕ in both the pdf output and the html output, but \<rightharpoonup> comes out as ⇀ in the pdf output and as \<rightharpoonup> in the html output. How can I this and other symbols print nicely in the html output?
Best wishes,
john
Email Gateway (Aug 19 2022 at 09:47):From: Makarius <makarius@sketis.net>
You can make a separate session for the imports, and take it as a parent
to your own stuff. The new isabelle build system makes it very easy to
specify sessions, as explained in the "system" manual.
Makarius
Email Gateway (Aug 19 2022 at 09:47):From: Makarius <makarius@sketis.net>
On the spot, I would say via perl on the generated HTML files.
HTML output is still awaiting substantial renovations. Hardly anything of
what is there in the pipeline system comming from the Ural made it
into Isabelle2013.
Makarius
Last updated: Nov 21 2024 at 12:39 UTC