cartouche within nested args (attributes, methods, etc.);

--- 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} ']'
     ;

--- 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;