[isabelle-dev] NEWS: document preparation refinements

Makarius makarius at sketis.net
Fri Oct 23 23:16:50 CEST 2015

Some more NEWS items (Isabelle/436b7fe89cdc):

*** Document preparation ***

* There is a new short form for antiquotations with a single argument
that is a cartouche: \<^name>‹...› is equivalent to @{name ‹...›} and
‹...› without control symbol is equivalent to @{cartouche ‹...›}. The
standard Isabelle fonts provide glyphs to render important control
symbols, e.g. "▩", "∗", "❙".

* Antiquotation @{cartouche} in Isabelle/Pure is the same as @{text}.
Consequently, ‹...› without any decoration prints literal quasi-formal
text. Command-line tool "isabelle update_cartouches -t" helps to update
old sources, by approximative patching of the content of string and
cartouche tokens seen in theory sources.

* The @{text} antiquotation now ignores the antiquotation option
"source". The given text content is output unconditionally, without any
surrounding quotes etc. Subtle INCOMPATIBILITY, put quotes into the
argument where they are really intended, e.g. @{text ‹"foo"›}. Initial
or terminal spaces are ignored.


More information about the isabelle-dev mailing list