src/Pure/Isar/token.ML

   datatype kind =
     (*immediate source*)
     Command | Keyword | Ident | Long_Ident | Sym_Ident | Var | Type_Ident | Type_Var | Nat |
     Float | Space |
     (*delimited content*)
-    String | Alt_String | Verbatim | Cartouche | Comment of Comment.kind option |
+    String | Alt_String | Verbatim | Cartouche |
+    Control of Antiquote.control |
+    Comment of Comment.kind option |
     (*special content*)
     Error of string | EOF
+  val control_kind: kind
   val str_of_kind: kind -> string
   type file = {src_path: Path.T, lines: string list, digest: SHA1.digest, pos: Position.T}
   type T
   type src = T list
   type name_value = {name: string, kind: string, print: Proof.context -> Markup.T * xstring}

   val is_eof: T -> bool
   val not_eof: T -> bool
   val stopper: T Scan.stopper
   val kind_of: T -> kind
   val is_kind: kind -> T -> bool
+  val get_control: T -> Antiquote.control option
   val is_command: T -> bool
   val keyword_with: (string -> bool) -> T -> bool
   val is_command_modifier: T -> bool
   val ident_with: (string -> bool) -> T -> bool
   val is_proper: T -> bool

 datatype kind =
   (*immediate source*)
   Command | Keyword | Ident | Long_Ident | Sym_Ident | Var | Type_Ident | Type_Var | Nat |
   Float | Space |
   (*delimited content*)
-  String | Alt_String | Verbatim | Cartouche | Comment of Comment.kind option |
+  String | Alt_String | Verbatim | Cartouche |
+  Control of Antiquote.control |
+  Comment of Comment.kind option |
   (*special content*)
   Error of string | EOF;
+
+val control_kind = Control Antiquote.no_control;
+
+fun equiv_kind kind kind' =
+  (case (kind, kind') of
+    (Control _, Control _) => true
+  | (Error _, Error _) => true
+  | _ => kind = kind');
 
 val str_of_kind =
  fn Command => "command"
   | Keyword => "keyword"
   | Ident => "identifier"

   | Space => "white space"
   | String => "quoted string"
   | Alt_String => "back-quoted string"
   | Verbatim => "verbatim text"
   | Cartouche => "text cartouche"
+  | Control _ => "control cartouche"
   | Comment NONE => "informal comment"
   | Comment (SOME _) => "formal comment"
   | Error _ => "bad input"
   | EOF => "end-of-input";
 

 val delimited_kind =
   (fn String => true
     | Alt_String => true
     | Verbatim => true
     | Cartouche => true
+    | Control _ => true
     | Comment _ => true
     | _ => false);
 
 
 (* datatype token *)

 
 
 (* kind of token *)
 
 fun kind_of (Token (_, (k, _), _)) = k;
-fun is_kind k (Token (_, (k', _), _)) = k = k';
+fun is_kind k (Token (_, (k', _), _)) = equiv_kind k k';
+
+fun get_control tok =
+  (case kind_of tok of Control control => SOME control | _ => NONE);
 
 val is_command = is_kind Command;
 
 fun keyword_with pred (Token (_, (Keyword, x), _)) = pred x
   | keyword_with _ _ = false;

   | Type_Var => (Markup.tvar, "")
   | String => (Markup.string, "")
   | Alt_String => (Markup.alt_string, "")
   | Verbatim => (Markup.verbatim, "")
   | Cartouche => (Markup.cartouche, "")
+  | Control _ => (Markup.cartouche, "")
   | Comment _ => (Markup.comment, "")
   | Error msg => (Markup.bad (), msg)
   | _ => (Markup.empty, "");
 
 fun keyword_reports tok = map (fn markup => ((pos_of tok, markup), ""));

   (case kind of
     String => Symbol_Pos.quote_string_qq x
   | Alt_String => Symbol_Pos.quote_string_bq x
   | Verbatim => enclose "{*" "*}" x
   | Cartouche => cartouche x
+  | Control control => Symbol_Pos.content (Antiquote.control_symbols control)
   | Comment NONE => enclose "(*" "*)" x
   | EOF => ""
   | _ => x);
 
 fun print tok = Markup.markups (markups Keyword.empty_keywords tok) (unparse tok);

 
 fun scan_token keywords = !!! "bad input"
   (Symbol_Pos.scan_string_qq err_prefix >> token_range String ||
     Symbol_Pos.scan_string_bq err_prefix >> token_range Alt_String ||
     scan_verbatim >> token_range Verbatim ||
-    scan_cartouche >> token_range Cartouche ||
     scan_comment >> token_range (Comment NONE) ||
     Comment.scan_outer >> (fn (k, ss) => token (Comment (SOME k)) ss) ||
+    scan_cartouche >> token_range Cartouche ||
+    Antiquote.scan_control err_prefix >> (fn control =>
+      token (Control control) (Antiquote.control_symbols control)) ||
     scan_space >> token Space ||
     (Scan.max token_leq
       (Scan.max token_leq
         (Scan.literal (Keyword.major_keywords keywords) >> pair Command)
         (Scan.literal (Keyword.minor_keywords keywords) >> pair Keyword))