src/Pure/Syntax/lexicon.ML

   val scan_var: Symbol_Pos.T list -> Symbol_Pos.T list * Symbol_Pos.T list
   val scan_tvar: Symbol_Pos.T list -> Symbol_Pos.T list * Symbol_Pos.T list
   val is_tid: string -> bool
   datatype token_kind =
     Literal | IdentSy | LongIdentSy | VarSy | TFreeSy | TVarSy |
-    NumSy | FloatSy | XNumSy | StrSy | Space | Comment | EOF
+    NumSy | FloatSy | XNumSy | StrSy | Cartouche | Space | Comment | EOF
   datatype token = Token of token_kind * string * Position.range
   val str_of_token: token -> string
   val pos_of_token: token -> Position.T
   val is_proper: token -> bool
   val mk_eof: Position.T -> token

 
 (** datatype token **)
 
 datatype token_kind =
   Literal | IdentSy | LongIdentSy | VarSy | TFreeSy | TVarSy |
-  NumSy | FloatSy | XNumSy | StrSy | Space | Comment | EOF;
+  NumSy | FloatSy | XNumSy | StrSy | Cartouche | Space | Comment | EOF;
 
 datatype token = Token of token_kind * string * Position.range;
 
 fun str_of_token (Token (_, s, _)) = s;
 fun pos_of_token (Token (_, _, (pos, _))) = pos;

   ("tid", TFreeSy),
   ("tvar", TVarSy),
   ("num_token", NumSy),
   ("float_token", FloatSy),
   ("xnum_token", XNumSy),
-  ("str_token", StrSy)];
+  ("str_token", StrSy),
+  ("cartouche", Cartouche)];
 
 val terminals = map #1 terminal_kinds;
 val is_terminal = member (op =) terminals;
 
 

   then Markup.literal
   else Markup.delimiter;
 
 val token_kind_markup =
  fn TFreeSy => Markup.tfree
-  | TVarSy  => Markup.tvar
-  | NumSy   => Markup.numeral
+  | TVarSy => Markup.tvar
+  | NumSy => Markup.numeral
   | FloatSy => Markup.numeral
-  | XNumSy  => Markup.numeral
-  | StrSy   => Markup.inner_string
+  | XNumSy => Markup.numeral
+  | StrSy => Markup.inner_string
+  | Cartouche => Markup.inner_cartouche
   | Comment => Markup.inner_comment
-  | _       => Markup.empty;
+  | _ => Markup.empty;
 
 fun report_of_token (Token (kind, s, (pos, _))) =
   let val markup = if kind = Literal then literal_markup s else token_kind_markup kind
   in (pos, markup) end;
 

       scan_xid >> token IdentSy;
 
     val scan_lit = Scan.literal lex >> token Literal;
 
     val scan_token =
+      Symbol_Pos.scan_cartouche !!! >> token Cartouche ||
       Symbol_Pos.scan_comment !!! >> token Comment ||
       Scan.max token_leq scan_lit scan_val ||
       scan_str >> token StrSy ||
       Scan.many1 (Symbol.is_blank o Symbol_Pos.symbol) >> token Space;
   in