Re: [isabelle] html syntax

On Tue, 28 Sep 2010, John Wickerson wrote:

Dear Isabelle Users,

I have produced an html version of a proof script:

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.

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 *}


  -- {* blah blah *}

The former is a command on its own, the latter can be attached to other commands in arbitrary places.


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.