Email Gateway (Aug 18 2022 at 15:58): Email Gateway (Aug 18 2022 at 15:58):From: John Wickerson <jpw48@cam.ac.uk>
Dear Isabelle Users,
I have produced an html version of a proof script:
http://www.cl.cam.ac.uk/~jpw48/traces/Traces_Composition.html
I would like to replace all occurrences of "\<sharp>" in the file with the hash symbol "#", because I think it makes it easier to read. I have tried to achieve this by writing
notation (html) tdisj (infix "#" 55)
but that didn't work. I don't want to use the hash symbol in the script itself, because it is already too overloaded. In a similar vein, I should like to replace all the "\<ast>" symbols with proper "*" symbols.
Any suggestions welcomed! Thanks very much,
John
Email Gateway (Aug 18 2022 at 15:59):From: Makarius <makarius@sketis.net>
The 'notation' command only affects printed output (terms that go through
the "inner syntax pretty printing engine"), but the HTML presentation is
only a crude superficial rendering of the source as given. It is based on
a hard-wired interpretation of some of the infinitely many Isabelle
symbols as HTML entities (see Isabelle/src/Pure/Thy/html.ML).
If you really care much about the HTML output, you can try some
post-processing with perl and regular expressions.
BTW, the (* source comments *) in your text are not part of the formal
document. Once the HTML rendering becomes more serious (closer to the
Isabelle LaTeX document preparation system), such raw comments will be
suppressed in the same way as LaTeX igores text after % comments.
The proper way to include informal text into theory sources is like this:
text {* blah blah *}
or
-- {* blah blah *}
The former is a command on its own, the latter can be attached to other
commands in arbitrary places.
Makarius
Last updated: Apr 26 2024 at 08:19 UTC