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. Makarius _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev