[isabelle] \<^locale> antiquotation does not work

[Peter Lammich]

Hi

Although jedit offers me a shortcut and a template with a 
cartouche for \<^locale><...>, it does not work, while @{locale <...>}
works perfectly.

What is the correct/intended way to use \<^locale> ?

--
  Peter



Example:

theory Scratch 
  imports Main
begin

locale Test

text ‹
  @{locale Test}
›

text ‹
  \<^locale>‹Test›
›
(* 
Bad arguments for document antiquotation "locale"⌂:
  ‹Test›
*)

[Makarius]

Post by Peter Lammich
Although jedit offers me a shortcut and a template with a 
works perfectly.
What is the correct/intended way to use \<^locale> ?

E.g. as ML antiquotation.

The document antiquotations is still lagging behind in supporting
cartouche syntax, but it will be supported in the next release.


Makarius