[isabelle-dev] NEWS: antiquoted cartouches

Makarius makarius at sketis.net
Wed Dec 6 23:02:01 CET 2017

On 05/12/17 17:18, Makarius wrote:
> *** Prover IDE -- Isabelle/Scala/jEdit ***
> * Named control symbols (without special Unicode rendering) are shown as
> bold-italic keyword. This is particularly useful for the short form of
> antiquotations with control symbol: \<^name>\<open>argument\<close>. The
> action
> "isabelle.antiquoted_cartouche" turns an antiquotation with 0 or 1
> arguments into this format.
> This refers to Isabelle/540eeaf88a63.
> Still required: update of various ML antiquotations to allow cartouche
> arguments. Right now it already works e.g. for @{typ}, @{term}, @{prop}.

Isabelle/909dcdec2122 enables many more ML antiquotations for this fancy
notation. Note that @{thm}, @{thms}, @{lemma} do not work due to their
more complex syntax.

Using action "isabelle.antiquoted_cartouche" in Isabelle/jEdit, I have
already updated all of src/Pure (dea94b1aabc3) and some of src/Tools and
src/HOL/Tools (e61557884799). Since there are so many ML sources, it is
probably better to upgrade the "isabelle update_cartouches" command-line
tool for this task.


More information about the isabelle-dev mailing list