src/Pure/Isar/parse.ML

   val number: string parser
   val float_number: string parser
   val string: string parser
   val alt_string: string parser
   val verbatim: string parser
+  val cartouche: string parser
   val sync: string parser
   val eof: string parser
   val command_name: string -> string parser
   val keyword_with: (string -> bool) -> string parser
   val keyword_ident_or_symbolic: string parser

 val number = kind Token.Nat;
 val float_number = kind Token.Float;
 val string = kind Token.String;
 val alt_string = kind Token.AltString;
 val verbatim = kind Token.Verbatim;
+val cartouche = kind Token.Cartouche;
 val sync = kind Token.Sync;
 val eof = kind Token.EOF;
 
 fun keyword_with pred = RESET_VALUE (Scan.one (Token.keyword_with pred) >> Token.content_of);
 val keyword_ident_or_symbolic = keyword_with Token.ident_or_symbolic;