# HG changeset patch
# User wenzelm
# Date 1390161177 -3600
# Node ID 99056d23e05bdc5f4f0cc25814c1f045aeb4ed5d
# Parent  5f4d5f6876f120cbebe62e646f51435caa14eb71
cartouche within nested args (attributes, methods, etc.);

diff -r 5f4d5f6876f1 -r 99056d23e05b src/Doc/IsarRef/Outer_Syntax.thy
--- a/src/Doc/IsarRef/Outer_Syntax.thy	Sun Jan 19 20:39:48 2014 +0100
+++ b/src/Doc/IsarRef/Outer_Syntax.thy	Sun Jan 19 20:52:57 2014 +0100
@@ -401,7 +401,7 @@
   @{rail "
     @{syntax_def atom}: @{syntax nameref} | @{syntax typefree} |
       @{syntax typevar} | @{syntax var} | @{syntax nat} | @{syntax float} |
-      @{syntax keyword}
+      @{syntax keyword} | @{syntax cartouche}
     ;
     arg: @{syntax atom} | '(' @{syntax args} ')' | '[' @{syntax args} ']'
     ;
diff -r 5f4d5f6876f1 -r 99056d23e05b src/Pure/Isar/args.ML
--- a/src/Pure/Isar/args.ML	Sun Jan 19 20:39:48 2014 +0100
+++ b/src/Pure/Isar/args.ML	Sun Jan 19 20:52:57 2014 +0100
@@ -29,6 +29,8 @@
   val bracks: 'a parser -> 'a parser
   val mode: string -> bool parser
   val maybe: 'a parser -> 'a option parser
+  val cartouche_source: string parser
+  val cartouche_source_position: (Symbol_Pos.text * Position.T) parser
   val name_source: string parser
   val name_source_position: (Symbol_Pos.text * Position.T) parser
   val name: string parser
@@ -148,6 +150,10 @@
 fun mode s = Scan.optional (parens ($$$ s) >> K true) false;
 fun maybe scan = $$$ "_" >> K NONE || scan >> SOME;
 
+val cartouche = token Parse.cartouche;
+val cartouche_source = cartouche >> Token.source_of;
+val cartouche_source_position = cartouche >> Token.source_position_of;
+
 val name_source = named >> Token.source_of;
 val name_source_position = named >> Token.source_position_of;