Re: [isabelle] @{command and "fixes"



On Mon, 15 Feb 2016, Buday Gergely wrote:

writes that the @{command antiquotation can be used via

ML_file "$ISABELLE_HOME/src/Doc/antiquote_setup.ML"

However, \item @{command "fixes"} is not accepted by Isabelle2015.

Is "fixes" not a command in this sense, or just the above file is not ready for handling this case?

No it is a minor keyword, not a command keyword.


Isabelle2016 has various improvements to typeset Isar theory text, see NEWS:

* Antiquotation @{theory_text} prints uninterpreted theory source text
(Isar outer syntax with command keywords etc.). This may be used in the
short form \<^theory_text>\<open>...\<close>. @{theory_text [display]} supports option "indent".

* Antiquotations @{command}, @{method}, @{attribute} print checked entities of the Isar language.


Which means the Isar antiquotations are there by default, but not needed for quick informal snippets that should like like formal text.


	Makarius




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