outer syntax: support for control-cartouche tokens;

--- a/src/Pure/General/antiquote.ML	Tue Sep 28 10:47:18 2021 +0200
+++ b/src/Pure/General/antiquote.ML	Tue Sep 28 16:01:13 2021 +0200
@@ -7,6 +7,8 @@
 signature ANTIQUOTE =
 sig
   type control = {range: Position.range, name: string * Position.T, body: Symbol_Pos.T list}
+  val no_control: control
+  val control_symbols: control -> Symbol_Pos.T list
   type antiq = {start: Position.T, stop: Position.T, range: Position.range, body: Symbol_Pos.T list}
   datatype 'a antiquote = Text of 'a | Control of control | Antiq of antiq
   val is_text: 'a antiquote -> bool
@@ -17,7 +19,8 @@
   val split_lines: text_antiquote list -> text_antiquote list list
   val antiq_reports: 'a antiquote list -> Position.report list
   val update_reports: bool -> Position.T -> string list -> Position.report_text list
-  val scan_control: control scanner
+  val err_prefix: string
+  val scan_control: string -> control scanner
   val scan_antiq: antiq scanner
   val scan_antiquote: text_antiquote scanner
   val scan_antiquote_comments: text_antiquote scanner
@@ -31,6 +34,10 @@
 (* datatype antiquote *)
 
 type control = {range: Position.range, name: string * Position.T, body: Symbol_Pos.T list};
+val no_control = {range = Position.no_range, name = ("", Position.none), body = []};
+fun control_symbols ({name = (name, pos), body, ...}: control) =
+  (Symbol.encode (Symbol.Control name), pos) :: body;
+
 type antiq = {start: Position.T, stop: Position.T, range: Position.range, body: Symbol_Pos.T list};
 datatype 'a antiquote = Text of 'a | Control of control | Antiq of antiq;
 
@@ -112,9 +119,9 @@
 
 open Basic_Symbol_Pos;
 
-local
+val err_prefix = "Antiquotation lexical error: ";
 
-val err_prefix = "Antiquotation lexical error: ";
+local
 
 val scan_nl = Scan.one (fn (s, _) => s = "\n") >> single;
 val scan_nl_opt = Scan.optional scan_nl [];
@@ -148,9 +155,9 @@
 
 in
 
-val scan_control =
+fun scan_control err =
   Scan.option (Scan.one (Symbol.is_control o Symbol_Pos.symbol)) --
-  Symbol_Pos.scan_cartouche err_prefix >>
+  Symbol_Pos.scan_cartouche err >>
     (fn (opt_control, body) =>
       let
         val (name, range) =
@@ -173,10 +180,10 @@
        body = body});
 
 val scan_antiquote =
-  scan_text >> Text || scan_control >> Control || scan_antiq >> Antiq;
+  scan_text >> Text || scan_control err_prefix >> Control || scan_antiq >> Antiq;
 
 val scan_antiquote_comments =
-  scan_text_comments >> Text || scan_control >> Control || scan_antiq >> Antiq;
+  scan_text_comments >> Text || scan_control err_prefix >> Control || scan_antiq >> Antiq;
 
 end;
 

--- a/src/Pure/General/scan.scala	Tue Sep 28 10:47:18 2021 +0200
+++ b/src/Pure/General/scan.scala	Tue Sep 28 16:01:13 2021 +0200
@@ -290,6 +290,13 @@
     }
 
 
+    /* control cartouches */
+
+    val control_symbol: Parser[String] = one(Symbol.is_control)
+
+    val control_cartouche: Parser[String] = control_symbol ~ cartouche ^^ { case a ~ b => a + b }
+
+
     /* keyword */
 
     def literal(lexicon: Lexicon): Parser[String] = new Parser[String]

--- a/src/Pure/Isar/parse.ML	Tue Sep 28 10:47:18 2021 +0200
+++ b/src/Pure/Isar/parse.ML	Tue Sep 28 16:01:13 2021 +0200
@@ -32,6 +32,7 @@
   val alt_string: string parser
   val verbatim: string parser
   val cartouche: string parser
+  val control: Antiquote.control parser
   val eof: string parser
   val command_name: string -> string parser
   val keyword_with: (string -> bool) -> string parser
@@ -195,6 +196,7 @@
 val alt_string = kind Token.Alt_String;
 val verbatim = kind Token.Verbatim;
 val cartouche = kind Token.Cartouche;
+val control = token (kind Token.control_kind) >> (the o Token.get_control);
 val eof = kind Token.EOF;
 
 fun command_name x =

--- a/src/Pure/Isar/token.ML	Tue Sep 28 10:47:18 2021 +0200
+++ b/src/Pure/Isar/token.ML	Tue Sep 28 16:01:13 2021 +0200
@@ -11,9 +11,12 @@
     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
@@ -37,6 +40,7 @@
   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
@@ -118,10 +122,20 @@
   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"
@@ -138,6 +152,7 @@
   | 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"
@@ -152,6 +167,7 @@
     | Alt_String => true
     | Verbatim => true
     | Cartouche => true
+    | Control _ => true
     | Comment _ => true
     | _ => false);
 
@@ -214,7 +230,10 @@
 (* 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;
 
@@ -304,6 +323,7 @@
   | Alt_String => (Markup.alt_string, "")
   | Verbatim => (Markup.verbatim, "")
   | Cartouche => (Markup.cartouche, "")
+  | Control _ => (Markup.cartouche, "")
   | Comment _ => (Markup.comment, "")
   | Error msg => (Markup.bad (), msg)
   | _ => (Markup.empty, "");
@@ -354,6 +374,7 @@
   | 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);
@@ -646,9 +667,11 @@
   (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

--- a/src/Pure/Isar/token.scala	Tue Sep 28 10:47:18 2021 +0200
+++ b/src/Pure/Isar/token.scala	Tue Sep 28 16:01:13 2021 +0200
@@ -34,6 +34,7 @@
     val ALT_STRING = Value("back-quoted string")
     val VERBATIM = Value("verbatim text")
     val CARTOUCHE = Value("text cartouche")
+    val CONTROL = Value("control cartouche")
     val INFORMAL_COMMENT = Value("informal comment")
     val FORMAL_COMMENT = Value("formal comment")
     /*special content*/
@@ -53,11 +54,12 @@
       val string = quoted("\"") ^^ (x => Token(Token.Kind.STRING, x))
       val alt_string = quoted("`") ^^ (x => Token(Token.Kind.ALT_STRING, x))
       val verb = verbatim ^^ (x => Token(Token.Kind.VERBATIM, x))
-      val cart = cartouche ^^ (x => Token(Token.Kind.CARTOUCHE, x))
       val cmt = comment ^^ (x => Token(Token.Kind.INFORMAL_COMMENT, x))
       val formal_cmt = comment_cartouche ^^ (x => Token(Token.Kind.FORMAL_COMMENT, x))
+      val cart = cartouche ^^ (x => Token(Token.Kind.CARTOUCHE, x))
+      val ctrl = control_cartouche ^^ (x => Token(Token.Kind.CONTROL, x))
 
-      string | (alt_string | (verb | (cart | (cmt | formal_cmt))))
+      string | (alt_string | (verb | (cmt | (formal_cmt | (cart | ctrl)))))
     }
 
     private def other_token(keywords: Keyword.Keywords): Parser[Token] =

--- a/src/Pure/ML/ml_lex.ML	Tue Sep 28 10:47:18 2021 +0200
+++ b/src/Pure/ML/ml_lex.ML	Tue Sep 28 16:01:13 2021 +0200
@@ -36,6 +36,7 @@
     token Antiquote.antiquote Symbol_Pos.scanner -> Input.source -> token Antiquote.antiquote list
   val read_source: Input.source -> token Antiquote.antiquote list
   val read_source_sml: Input.source -> token Antiquote.antiquote list
+  val read_symbols: Symbol_Pos.T list -> token Antiquote.antiquote list
   val read_symbols_sml: Symbol_Pos.T list -> token Antiquote.antiquote list
 end;
 
@@ -315,7 +316,7 @@
 
 val scan_ml_antiq =
   Comment.scan_inner >> (fn (kind, ss) => Antiquote.Text (token (Comment (SOME kind)) ss)) ||
-  Antiquote.scan_control >> Antiquote.Control ||
+  Antiquote.scan_control Antiquote.err_prefix >> Antiquote.Control ||
   Antiquote.scan_antiq >> Antiquote.Antiq ||
   scan_rat_antiq >> Antiquote.Antiq ||
   scan_sml_antiq;
@@ -389,6 +390,7 @@
   read_source' {language = Markup.language_SML, symbols = false, opaque_warning = false}
     scan_sml_antiq;
 
+val read_symbols = reader {opaque_warning = true} scan_ml_antiq;
 val read_symbols_sml = reader {opaque_warning = false} scan_sml_antiq;
 
 end;

--- a/src/Pure/Thy/document_output.ML	Tue Sep 28 10:47:18 2021 +0200
+++ b/src/Pure/Thy/document_output.ML	Tue Sep 28 16:01:13 2021 +0200
@@ -156,6 +156,7 @@
     | Token.Alt_String => output false "{\\isacharbackquoteopen}" "{\\isacharbackquoteclose}"
     | Token.Verbatim => output true "{\\isacharverbatimopen}" "{\\isacharverbatimclose}"
     | Token.Cartouche => output false "{\\isacartoucheopen}" "{\\isacartoucheclose}"
+    | Token.Control control => output_body ctxt false "" "" (Antiquote.control_symbols control)
     | _ => output false "" "")
   end handle ERROR msg => error (msg ^ Position.here (Token.pos_of tok));
 

--- a/src/Pure/Tools/generated_files.ML	Tue Sep 28 10:47:18 2021 +0200
+++ b/src/Pure/Tools/generated_files.ML	Tue Sep 28 16:01:13 2021 +0200
@@ -201,7 +201,7 @@
   end;
 
 val scan_antiq =
-  Antiquote.scan_control >> Antiquote.Control ||
+  Antiquote.scan_control Antiquote.err_prefix >> Antiquote.Control ||
   Scan.one (Symbol.not_eof o Symbol_Pos.symbol) >> (Antiquote.Text o Symbol_Pos.symbol);
 
 fun read_source ctxt (file_type: file_type) source =

--- a/src/Tools/jEdit/src/jedit_rendering.scala	Tue Sep 28 10:47:18 2021 +0200
+++ b/src/Tools/jEdit/src/jedit_rendering.scala	Tue Sep 28 16:01:13 2021 +0200
@@ -72,6 +72,7 @@
       Token.Kind.ALT_STRING -> LITERAL2,
       Token.Kind.VERBATIM -> COMMENT3,
       Token.Kind.CARTOUCHE -> COMMENT3,
+      Token.Kind.CONTROL -> COMMENT3,
       Token.Kind.INFORMAL_COMMENT -> COMMENT1,
       Token.Kind.FORMAL_COMMENT -> COMMENT1,
       Token.Kind.ERROR -> INVALID