# HG changeset patch
# User wenzelm
# Date 1546634946 -3600
# Node ID a80d8ec6c998449221f50352106a7d84f14d3aff
# Parent  cc6a21413f8a8bb65830a94f852fa7e883d23de5
support for isabelle update -u control_cartouches;

diff -r cc6a21413f8a -r a80d8ec6c998 NEWS
--- a/NEWS	Thu Jan 03 22:30:41 2019 +0100
+++ b/NEWS	Fri Jan 04 21:49:06 2019 +0100
@@ -171,6 +171,10 @@
 section "Theory update". Theory sessions are specified as in "isabelle
 dump".
 
+* The command-line tool "isabelle update -u control_cartouches" changes
+antiquotations into control-symbol format (where possible): @{NAME}
+becomes \<^NAME> and @{NAME ARG} becomes \<^NAME>\<open>ARG\<close>.
+
 * Support for Isabelle command-line tools defined in Isabelle/Scala.
 Instances of class Isabelle_Scala_Tools may be configured via the shell
 function "isabelle_scala_tools" in etc/settings (e.g. of an Isabelle
diff -r cc6a21413f8a -r a80d8ec6c998 etc/options
--- a/etc/options	Thu Jan 03 22:30:41 2019 +0100
+++ b/etc/options	Fri Jan 04 21:49:06 2019 +0100
@@ -285,6 +285,9 @@
 option update_mixfix_cartouches : bool = false
   -- "update mixfix templates to use cartouches instead of double quotes"
 
+option update_control_cartouches : bool = false
+  -- "update antiquotations to use control symbol with cartouche argument"
+
 
 section "Build Database"
 
diff -r cc6a21413f8a -r a80d8ec6c998 src/HOL/Library/LaTeXsugar.thy
--- a/src/HOL/Library/LaTeXsugar.thy	Thu Jan 03 22:30:41 2019 +0100
+++ b/src/HOL/Library/LaTeXsugar.thy	Fri Jan 04 21:49:06 2019 +0100
@@ -97,7 +97,8 @@
   "_asm" :: "prop \<Rightarrow> asms" ("_")
 
 setup \<open>
-  Thy_Output.antiquotation_pretty_source \<^binding>\<open>const_typ\<close> (Scan.lift Args.embedded_inner_syntax)
+  Thy_Output.antiquotation_pretty_source_embedded \<^binding>\<open>const_typ\<close>
+    (Scan.lift Args.embedded_inner_syntax)
     (fn ctxt => fn c =>
       let val tc = Proof_Context.read_const {proper = false, strict = false} ctxt c in
         Pretty.block [Thy_Output.pretty_term ctxt tc, Pretty.str " ::",
diff -r cc6a21413f8a -r a80d8ec6c998 src/HOL/Tools/BNF/bnf_fp_util.ML
--- a/src/HOL/Tools/BNF/bnf_fp_util.ML	Thu Jan 03 22:30:41 2019 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_util.ML	Fri Jan 04 21:49:06 2019 +0100
@@ -983,7 +983,8 @@
   end;
 
 fun fp_antiquote_setup binding =
-  Thy_Output.antiquotation_pretty_source binding (Args.type_name {proper = true, strict = true})
+  Thy_Output.antiquotation_pretty_source_embedded binding
+    (Args.type_name {proper = true, strict = true})
     (fn ctxt => fn fcT_name =>
        (case Ctr_Sugar.ctr_sugar_of ctxt fcT_name of
          NONE => error ("Not a known freely generated type name: " ^ quote fcT_name)
diff -r cc6a21413f8a -r a80d8ec6c998 src/HOL/Tools/value_command.ML
--- a/src/HOL/Tools/value_command.ML	Thu Jan 03 22:30:41 2019 +0100
+++ b/src/HOL/Tools/value_command.ML	Fri Jan 04 21:49:06 2019 +0100
@@ -73,7 +73,7 @@
       >> (fn ((name, modes), t) => Toplevel.keep (value_cmd name modes t)));
 
 val _ = Theory.setup
-  (Thy_Output.antiquotation_pretty_source \<^binding>\<open>value\<close>
+  (Thy_Output.antiquotation_pretty_source_embedded \<^binding>\<open>value\<close>
     (Scan.lift opt_evaluator -- Term_Style.parse -- Args.term)
     (fn ctxt => fn ((name, style), t) =>
       Thy_Output.pretty_term ctxt (style (value_select name ctxt t)))
diff -r cc6a21413f8a -r a80d8ec6c998 src/Pure/General/antiquote.ML
--- a/src/Pure/General/antiquote.ML	Thu Jan 03 22:30:41 2019 +0100
+++ b/src/Pure/General/antiquote.ML	Fri Jan 04 21:49:06 2019 +0100
@@ -14,6 +14,7 @@
   val text_range: text_antiquote list -> Position.range
   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 scan_antiq: antiq scanner
   val scan_antiquote: text_antiquote scanner
@@ -71,6 +72,30 @@
          (pos, Markup.language_antiquotation)]);
 
 
+(* update *)
+
+fun update_reports embedded pos src =
+  let
+    val n = length src;
+    val no_arg = n = 1;
+    val embedded_arg = n = 2 andalso embedded;
+    val control =
+      (case src of
+        name :: _ =>
+          if Symbol.is_ascii_identifier name andalso name <> "cartouche" andalso
+            (no_arg orelse embedded_arg)
+          then SOME (Symbol.control_prefix ^ name ^ Symbol.control_suffix)
+          else NONE
+      | [] => NONE);
+    val arg = if embedded_arg then cartouche (nth src 1) else "";
+  in
+    (case control of
+      SOME sym => [((pos, Markup.update), sym ^ arg)]
+    | NONE => [])
+  end;
+
+
+
 (* scan *)
 
 open Basic_Symbol_Pos;
diff -r cc6a21413f8a -r a80d8ec6c998 src/Pure/General/symbol.ML
--- a/src/Pure/General/symbol.ML	Thu Jan 03 22:30:41 2019 +0100
+++ b/src/Pure/General/symbol.ML	Fri Jan 04 21:49:06 2019 +0100
@@ -23,6 +23,8 @@
   val is_symbolic: symbol -> bool
   val is_symbolic_char: symbol -> bool
   val is_printable: symbol -> bool
+  val control_prefix: string
+  val control_suffix: string
   val is_control: symbol -> bool
   val eof: symbol
   val is_eof: symbol -> bool
@@ -135,8 +137,11 @@
   if is_char s then 32 <= ord s andalso ord s <= Char.ord #"~"
   else is_utf8 s orelse raw_symbolic s;
 
+val control_prefix = "\092<^";
+val control_suffix = ">";
+
 fun is_control s =
-  String.isPrefix "\092<^" s andalso String.isSuffix ">" s;
+  String.isPrefix control_prefix s andalso String.isSuffix control_suffix s;
 
 
 (* input source control *)
diff -r cc6a21413f8a -r a80d8ec6c998 src/Pure/ML/ml_antiquotation.ML
--- a/src/Pure/ML/ml_antiquotation.ML	Thu Jan 03 22:30:41 2019 +0100
+++ b/src/Pure/ML/ml_antiquotation.ML	Fri Jan 04 21:49:06 2019 +0100
@@ -9,8 +9,13 @@
   val declaration: binding -> 'a context_parser ->
     (Token.src -> 'a -> Proof.context -> ML_Context.decl * Proof.context) ->
     theory -> theory
+  val declaration_embedded: binding -> 'a context_parser ->
+    (Token.src -> 'a -> Proof.context -> ML_Context.decl * Proof.context) ->
+    theory -> theory
   val inline: binding -> string context_parser -> theory -> theory
+  val inline_embedded: binding -> string context_parser -> theory -> theory
   val value: binding -> string context_parser -> theory -> theory
+  val value_embedded: binding -> string context_parser -> theory -> theory
 end;
 
 structure ML_Antiquotation: ML_ANTIQUOTATION =
@@ -18,17 +23,32 @@
 
 (* define antiquotations *)
 
-fun declaration name scan body =
-  ML_Context.add_antiquotation name
+local
+
+fun gen_declaration name embedded scan body =
+  ML_Context.add_antiquotation name embedded
     (fn src => fn orig_ctxt =>
       let val (x, _) = Token.syntax scan src orig_ctxt
       in body src x orig_ctxt end);
 
-fun inline name scan =
-  declaration name scan (fn _ => fn s => fn ctxt => (K ("", s), ctxt));
+fun gen_inline name embedded scan =
+  gen_declaration name embedded scan (fn _ => fn s => fn ctxt => (K ("", s), ctxt));
+
+fun gen_value name embedded scan =
+  gen_declaration name embedded scan (fn _ => ML_Context.value_decl (Binding.name_of name));
+
+in
 
-fun value name scan =
-  declaration name scan (fn _ => ML_Context.value_decl (Binding.name_of name));
+fun declaration name = gen_declaration name false;
+fun declaration_embedded name = gen_declaration name true;
+
+fun inline name = gen_inline name false;
+fun inline_embedded name = gen_inline name true;
+
+fun value name = gen_value name false;
+fun value_embedded name = gen_value name true;
+
+end;
 
 
 (* basic antiquotations *)
@@ -40,15 +60,15 @@
 
   inline (Binding.make ("make_string", \<^here>)) (Args.context >> K ML_Pretty.make_string_fn) #>
 
-  value (Binding.make ("binding", \<^here>))
+  value_embedded (Binding.make ("binding", \<^here>))
     (Scan.lift (Parse.input Args.embedded) >> (ML_Syntax.make_binding o Input.source_content)) #>
 
-  value (Binding.make ("cartouche", \<^here>))
+  value_embedded (Binding.make ("cartouche", \<^here>))
     (Scan.lift Args.cartouche_input >> (fn source =>
       "Input.source true " ^ ML_Syntax.print_string (Input.text_of source) ^ " " ^
         ML_Syntax.atomic (ML_Syntax.print_range (Input.range_of source)))) #>
 
-  inline (Binding.make ("verbatim", \<^here>))
+  inline_embedded (Binding.make ("verbatim", \<^here>))
     (Scan.lift Args.embedded >> ML_Syntax.print_string));
 
 end;
diff -r cc6a21413f8a -r a80d8ec6c998 src/Pure/ML/ml_antiquotations.ML
--- a/src/Pure/ML/ml_antiquotations.ML	Thu Jan 03 22:30:41 2019 +0100
+++ b/src/Pure/ML/ml_antiquotations.ML	Fri Jan 04 21:49:06 2019 +0100
@@ -16,7 +16,7 @@
   ML_Antiquotation.inline \<^binding>\<open>assert\<close>
     (Scan.succeed "(fn b => if b then () else raise General.Fail \"Assertion failed\")") #>
 
-  ML_Antiquotation.declaration \<^binding>\<open>print\<close>
+  ML_Antiquotation.declaration_embedded \<^binding>\<open>print\<close>
     (Scan.lift (Scan.optional Args.embedded "Output.writeln"))
       (fn src => fn output => fn ctxt =>
         let
@@ -40,18 +40,18 @@
 (* formal entities *)
 
 val _ = Theory.setup
- (ML_Antiquotation.value \<^binding>\<open>system_option\<close>
+ (ML_Antiquotation.value_embedded \<^binding>\<open>system_option\<close>
     (Args.context -- Scan.lift Args.embedded_position >> (fn (ctxt, (name, pos)) =>
       (Completion.check_option (Options.default ()) ctxt (name, pos) |> ML_Syntax.print_string))) #>
 
-  ML_Antiquotation.value \<^binding>\<open>theory\<close>
+  ML_Antiquotation.value_embedded \<^binding>\<open>theory\<close>
     (Args.context -- Scan.lift Args.embedded_position >> (fn (ctxt, (name, pos)) =>
       (Theory.check {long = false} ctxt (name, pos);
        "Context.get_theory {long = false} (Proof_Context.theory_of ML_context) " ^
         ML_Syntax.print_string name))
     || Scan.succeed "Proof_Context.theory_of ML_context") #>
 
-  ML_Antiquotation.value \<^binding>\<open>theory_context\<close>
+  ML_Antiquotation.value_embedded \<^binding>\<open>theory_context\<close>
     (Args.context -- Scan.lift Args.embedded_position >> (fn (ctxt, (name, pos)) =>
       (Theory.check {long = false} ctxt (name, pos);
        "Proof_Context.get_global (Proof_Context.theory_of ML_context) " ^
@@ -60,20 +60,25 @@
   ML_Antiquotation.inline \<^binding>\<open>context\<close>
     (Args.context >> (fn ctxt => ML_Context.struct_name ctxt ^ ".ML_context")) #>
 
-  ML_Antiquotation.inline \<^binding>\<open>typ\<close> (Args.typ >> (ML_Syntax.atomic o ML_Syntax.print_typ)) #>
-  ML_Antiquotation.inline \<^binding>\<open>term\<close> (Args.term >> (ML_Syntax.atomic o ML_Syntax.print_term)) #>
-  ML_Antiquotation.inline \<^binding>\<open>prop\<close> (Args.prop >> (ML_Syntax.atomic o ML_Syntax.print_term)) #>
+  ML_Antiquotation.inline_embedded \<^binding>\<open>typ\<close>
+    (Args.typ >> (ML_Syntax.atomic o ML_Syntax.print_typ)) #>
 
-  ML_Antiquotation.value \<^binding>\<open>ctyp\<close> (Args.typ >> (fn T =>
+  ML_Antiquotation.inline_embedded \<^binding>\<open>term\<close>
+    (Args.term >> (ML_Syntax.atomic o ML_Syntax.print_term)) #>
+
+  ML_Antiquotation.inline_embedded \<^binding>\<open>prop\<close>
+    (Args.prop >> (ML_Syntax.atomic o ML_Syntax.print_term)) #>
+
+  ML_Antiquotation.value_embedded \<^binding>\<open>ctyp\<close> (Args.typ >> (fn T =>
     "Thm.ctyp_of ML_context " ^ ML_Syntax.atomic (ML_Syntax.print_typ T))) #>
 
-  ML_Antiquotation.value \<^binding>\<open>cterm\<close> (Args.term >> (fn t =>
+  ML_Antiquotation.value_embedded \<^binding>\<open>cterm\<close> (Args.term >> (fn t =>
     "Thm.cterm_of ML_context " ^ ML_Syntax.atomic (ML_Syntax.print_term t))) #>
 
-  ML_Antiquotation.value \<^binding>\<open>cprop\<close> (Args.prop >> (fn t =>
+  ML_Antiquotation.value_embedded \<^binding>\<open>cprop\<close> (Args.prop >> (fn t =>
     "Thm.cterm_of ML_context " ^ ML_Syntax.atomic (ML_Syntax.print_term t))) #>
 
-  ML_Antiquotation.inline \<^binding>\<open>method\<close>
+  ML_Antiquotation.inline_embedded \<^binding>\<open>method\<close>
     (Args.context -- Scan.lift Args.embedded_position >> (fn (ctxt, (name, pos)) =>
       ML_Syntax.print_string (Method.check_name ctxt (name, pos)))));
 
@@ -81,7 +86,7 @@
 (* locales *)
 
 val _ = Theory.setup
- (ML_Antiquotation.inline \<^binding>\<open>locale\<close>
+ (ML_Antiquotation.inline_embedded \<^binding>\<open>locale\<close>
    (Args.context -- Scan.lift Args.embedded_position >> (fn (ctxt, (name, pos)) =>
       Locale.check (Proof_Context.theory_of ctxt) (name, pos)
       |> ML_Syntax.print_string)));
@@ -95,10 +100,10 @@
   |> ML_Syntax.print_string);
 
 val _ = Theory.setup
- (ML_Antiquotation.inline \<^binding>\<open>class\<close> (class false) #>
-  ML_Antiquotation.inline \<^binding>\<open>class_syntax\<close> (class true) #>
+ (ML_Antiquotation.inline_embedded \<^binding>\<open>class\<close> (class false) #>
+  ML_Antiquotation.inline_embedded \<^binding>\<open>class_syntax\<close> (class true) #>
 
-  ML_Antiquotation.inline \<^binding>\<open>sort\<close>
+  ML_Antiquotation.inline_embedded \<^binding>\<open>sort\<close>
     (Args.context -- Scan.lift Args.embedded_inner_syntax >> (fn (ctxt, s) =>
       ML_Syntax.atomic (ML_Syntax.print_sort (Syntax.read_sort ctxt s)))));
 
@@ -119,13 +124,13 @@
     in ML_Syntax.print_string res end);
 
 val _ = Theory.setup
- (ML_Antiquotation.inline \<^binding>\<open>type_name\<close>
+ (ML_Antiquotation.inline_embedded \<^binding>\<open>type_name\<close>
     (type_name "logical type" (fn (c, Type.LogicalType _) => c)) #>
-  ML_Antiquotation.inline \<^binding>\<open>type_abbrev\<close>
+  ML_Antiquotation.inline_embedded \<^binding>\<open>type_abbrev\<close>
     (type_name "type abbreviation" (fn (c, Type.Abbreviation _) => c)) #>
-  ML_Antiquotation.inline \<^binding>\<open>nonterminal\<close>
+  ML_Antiquotation.inline_embedded \<^binding>\<open>nonterminal\<close>
     (type_name "nonterminal" (fn (c, Type.Nonterminal) => c)) #>
-  ML_Antiquotation.inline \<^binding>\<open>type_syntax\<close>
+  ML_Antiquotation.inline_embedded \<^binding>\<open>type_syntax\<close>
     (type_name "type" (fn (c, _) => Lexicon.mark_type c)));
 
 
@@ -142,14 +147,14 @@
     in ML_Syntax.print_string res end);
 
 val _ = Theory.setup
- (ML_Antiquotation.inline \<^binding>\<open>const_name\<close>
+ (ML_Antiquotation.inline_embedded \<^binding>\<open>const_name\<close>
     (const_name (fn (consts, c) => (Consts.the_const consts c; c))) #>
-  ML_Antiquotation.inline \<^binding>\<open>const_abbrev\<close>
+  ML_Antiquotation.inline_embedded \<^binding>\<open>const_abbrev\<close>
     (const_name (fn (consts, c) => (Consts.the_abbreviation consts c; c))) #>
-  ML_Antiquotation.inline \<^binding>\<open>const_syntax\<close>
+  ML_Antiquotation.inline_embedded \<^binding>\<open>const_syntax\<close>
     (const_name (fn (_, c) => Lexicon.mark_const c)) #>
 
-  ML_Antiquotation.inline \<^binding>\<open>syntax_const\<close>
+  ML_Antiquotation.inline_embedded \<^binding>\<open>syntax_const\<close>
     (Args.context -- Scan.lift Args.embedded_position >> (fn (ctxt, (c, pos)) =>
       if is_some (Syntax.lookup_const (Proof_Context.syn_of ctxt) c)
       then ML_Syntax.print_string c
@@ -252,7 +257,7 @@
 (* outer syntax *)
 
 val _ = Theory.setup
- (ML_Antiquotation.value \<^binding>\<open>keyword\<close>
+ (ML_Antiquotation.value_embedded \<^binding>\<open>keyword\<close>
     (Args.context --
       Scan.lift (Parse.embedded_position || Parse.position (Parse.keyword_with (K true)))
       >> (fn (ctxt, (name, pos)) =>
@@ -260,7 +265,7 @@
           (Context_Position.report ctxt pos (Token.keyword_markup (true, Markup.keyword2) name);
            "Parse.$$$ " ^ ML_Syntax.print_string name)
         else error ("Bad outer syntax keyword " ^ quote name ^ Position.here pos))) #>
-  ML_Antiquotation.value \<^binding>\<open>command_keyword\<close>
+  ML_Antiquotation.value_embedded \<^binding>\<open>command_keyword\<close>
     (Args.context -- Scan.lift Parse.embedded_position >> (fn (ctxt, (name, pos)) =>
       (case Keyword.command_markup (Thy_Header.get_keywords' ctxt) name of
         SOME markup =>
diff -r cc6a21413f8a -r a80d8ec6c998 src/Pure/ML/ml_context.ML
--- a/src/Pure/ML/ml_context.ML	Thu Jan 03 22:30:41 2019 +0100
+++ b/src/Pure/ML/ml_context.ML	Fri Jan 04 21:49:06 2019 +0100
@@ -11,7 +11,7 @@
   val variant: string -> Proof.context -> string * Proof.context
   type decl = Proof.context -> string * string
   val value_decl: string -> string -> Proof.context -> decl * Proof.context
-  val add_antiquotation: binding -> (Token.src -> Proof.context -> decl * Proof.context) ->
+  val add_antiquotation: binding -> bool -> (Token.src -> Proof.context -> decl * Proof.context) ->
     theory -> theory
   val print_antiquotations: bool -> Proof.context -> unit
   val eval: ML_Compiler.flags -> Position.T -> ML_Lex.token Antiquote.antiquote list -> unit
@@ -67,7 +67,7 @@
 
 structure Antiquotations = Theory_Data
 (
-  type T = (Token.src -> Proof.context -> decl * Proof.context) Name_Space.table;
+  type T = (bool * (Token.src -> Proof.context -> decl * Proof.context)) Name_Space.table;
   val empty : T = Name_Space.empty_table Markup.ML_antiquotationN;
   val extend = I;
   fun merge data : T = Name_Space.merge_tables data;
@@ -78,17 +78,23 @@
 fun check_antiquotation ctxt =
   #1 o Name_Space.check (Context.Proof ctxt) (get_antiquotations ctxt);
 
-fun add_antiquotation name f thy = thy
-  |> Antiquotations.map (Name_Space.define (Context.Theory thy) true (name, f) #> snd);
+fun add_antiquotation name embedded scan thy = thy
+  |> Antiquotations.map (Name_Space.define (Context.Theory thy) true (name, (embedded, scan)) #> snd);
 
 fun print_antiquotations verbose ctxt =
   Pretty.big_list "ML antiquotations:"
     (map (Pretty.mark_str o #1) (Name_Space.markup_table verbose ctxt (get_antiquotations ctxt)))
   |> Pretty.writeln;
 
-fun apply_antiquotation src ctxt =
-  let val (src', f) = Token.check_src ctxt get_antiquotations src
-  in f src' ctxt end;
+fun apply_antiquotation pos src ctxt =
+  let
+    val (src', (embedded, scan)) = Token.check_src ctxt get_antiquotations src;
+    val _ =
+      if Options.default_bool "update_control_cartouches" then
+        Context_Position.reports_text ctxt
+          (Antiquote.update_reports embedded pos (map Token.content_of src'))
+      else ();
+  in scan src' ctxt end;
 
 
 (* parsing and evaluation *)
@@ -123,7 +129,7 @@
           fun tokenize range = apply2 (ML_Lex.tokenize #> map (ML_Lex.set_range range));
 
           fun expand_src range src ctxt =
-            let val (decl, ctxt') = apply_antiquotation src ctxt
+            let val (decl, ctxt') = apply_antiquotation (#1 range) src ctxt;
             in (decl #> tokenize range, ctxt') end;
 
           fun expand (Antiquote.Text tok) ctxt = (K ([], [tok]), ctxt)
diff -r cc6a21413f8a -r a80d8ec6c998 src/Pure/PIDE/resources.ML
--- a/src/Pure/PIDE/resources.ML	Thu Jan 03 22:30:41 2019 +0100
+++ b/src/Pure/PIDE/resources.ML	Fri Jan 04 21:49:06 2019 +0100
@@ -277,16 +277,16 @@
 in
 
 val _ = Theory.setup
- (Thy_Output.antiquotation_verbatim \<^binding>\<open>session\<close>
+ (Thy_Output.antiquotation_verbatim_embedded \<^binding>\<open>session\<close>
     (Scan.lift Parse.embedded_position) check_session #>
-  Thy_Output.antiquotation_verbatim \<^binding>\<open>doc\<close>
+  Thy_Output.antiquotation_verbatim_embedded \<^binding>\<open>doc\<close>
     (Scan.lift Parse.embedded_position) check_doc #>
-  Thy_Output.antiquotation_raw \<^binding>\<open>path\<close> (document_antiq check_path) (K I) #>
-  Thy_Output.antiquotation_raw \<^binding>\<open>file\<close> (document_antiq check_file) (K I) #>
-  Thy_Output.antiquotation_raw \<^binding>\<open>dir\<close> (document_antiq check_dir) (K I) #>
-  ML_Antiquotation.value \<^binding>\<open>path\<close> (ML_antiq check_path) #>
-  ML_Antiquotation.value \<^binding>\<open>file\<close> (ML_antiq check_file) #>
-  ML_Antiquotation.value \<^binding>\<open>dir\<close> (ML_antiq check_dir) #>
+  Thy_Output.antiquotation_raw_embedded \<^binding>\<open>path\<close> (document_antiq check_path) (K I) #>
+  Thy_Output.antiquotation_raw_embedded \<^binding>\<open>file\<close> (document_antiq check_file) (K I) #>
+  Thy_Output.antiquotation_raw_embedded \<^binding>\<open>dir\<close> (document_antiq check_dir) (K I) #>
+  ML_Antiquotation.value_embedded \<^binding>\<open>path\<close> (ML_antiq check_path) #>
+  ML_Antiquotation.value_embedded \<^binding>\<open>file\<close> (ML_antiq check_file) #>
+  ML_Antiquotation.value_embedded \<^binding>\<open>dir\<close> (ML_antiq check_dir) #>
   ML_Antiquotation.value \<^binding>\<open>master_dir\<close>
     (Args.theory >> (ML_Syntax.print_path o master_directory)));
 
diff -r cc6a21413f8a -r a80d8ec6c998 src/Pure/Thy/document_antiquotation.ML
--- a/src/Pure/Thy/document_antiquotation.ML	Thu Jan 03 22:30:41 2019 +0100
+++ b/src/Pure/Thy/document_antiquotation.ML	Fri Jan 04 21:49:06 2019 +0100
@@ -26,6 +26,8 @@
   val check_option: Proof.context -> xstring * Position.T -> string
   val setup: binding -> 'a context_parser ->
     ({context: Proof.context, source: Token.src, argument: 'a} -> Latex.text) -> theory -> theory
+  val setup_embedded: binding -> 'a context_parser ->
+    ({context: Proof.context, source: Token.src, argument: 'a} -> Latex.text) -> theory -> theory
   val setup_option: binding -> (string -> Proof.context -> Proof.context) -> theory -> theory
   val boolean: string -> bool
   val integer: string -> int
@@ -86,7 +88,7 @@
 structure Data = Theory_Data
 (
   type T =
-    (Token.src -> Proof.context -> Latex.text) Name_Space.table *
+    (bool * (Token.src -> Proof.context -> Latex.text)) Name_Space.table *
       (string -> Proof.context -> Proof.context) Name_Space.table;
   val empty : T =
     (Name_Space.empty_table Markup.document_antiquotationN,
@@ -112,12 +114,16 @@
 fun check ctxt = #1 o Name_Space.check (Context.Proof ctxt) (#1 (get_antiquotations ctxt));
 fun check_option ctxt = #1 o Name_Space.check (Context.Proof ctxt) (#2 (get_antiquotations ctxt));
 
-fun setup name scan body thy =
+fun gen_setup name embedded scan body thy =
   let
     fun cmd src ctxt =
       let val (x, ctxt') = Token.syntax scan src ctxt
       in body {context = ctxt', source = src, argument = x} end;
-  in thy |> Data.map (apfst (Name_Space.define (Context.Theory thy) true (name, cmd) #> #2)) end;
+    val entry = (name, (embedded, cmd));
+  in thy |> Data.map (apfst (Name_Space.define (Context.Theory thy) true entry #> #2)) end;
+
+fun setup name = gen_setup name false;
+fun setup_embedded name = gen_setup name true;
 
 fun setup_option name opt thy = thy
   |> Data.map (apsnd (Name_Space.define (Context.Theory thy) true (name, opt) #> #2));
@@ -138,7 +144,7 @@
 val parse_antiq =
   Parse.!!!
     (Parse.token Parse.liberal_name -- properties -- Parse.args --| Scan.ahead Parse.eof)
-  >> (fn ((name, props), args) => (props, name :: args));
+  >> (fn ((name, opts), args) => (opts, name :: args));
 
 end;
 
@@ -147,9 +153,15 @@
 
 local
 
-fun command src ctxt =
-  let val (src', f) = Token.check_src ctxt (#1 o get_antiquotations) src
-  in f src' ctxt end;
+fun command pos (opts, src) ctxt =
+  let
+    val (src', (embedded, scan)) = Token.check_src ctxt (#1 o get_antiquotations) src;
+    val _ =
+      if null opts andalso Options.default_bool "update_control_cartouches" then
+        Context_Position.reports_text ctxt
+          (Antiquote.update_reports embedded pos (map Token.content_of src'))
+      else ();
+  in scan src' ctxt end;
 
 fun option ((xname, pos), s) ctxt =
   let
@@ -157,14 +169,14 @@
       Name_Space.check (Context.Proof ctxt) (#2 (get_antiquotations ctxt)) (xname, pos);
   in opt s ctxt end;
 
-fun eval ctxt (opts, src) =
+fun eval ctxt pos (opts, src) =
   let
     val preview_ctxt = fold option opts (Config.put show_markup false ctxt);
-    val _ = command src preview_ctxt;
+    val _ = command pos (opts, src) preview_ctxt;
 
     val print_ctxt = Context_Position.set_visible false preview_ctxt;
     val print_modes = space_explode "," (Config.get print_ctxt thy_output_modes) @ [Latex.latexN];
-  in [Print_Mode.with_modes print_modes (fn () => command src print_ctxt) ()] end;
+  in [Print_Mode.with_modes print_modes (fn () => command pos (opts, src) print_ctxt) ()] end;
 
 in
 
@@ -172,10 +184,11 @@
   (case antiq of
     Antiquote.Text ss => eval_text ss
   | Antiquote.Control {name, body, ...} =>
-      eval ctxt ([], Token.make_src name (if null body then [] else [Token.read_cartouche body]))
+      eval ctxt Position.none
+        ([], Token.make_src name (if null body then [] else [Token.read_cartouche body]))
   | Antiquote.Antiq {range = (pos, _), body, ...} =>
       let val keywords = Thy_Header.get_keywords' ctxt;
-      in eval ctxt (Token.read_antiq keywords parse_antiq (body, pos)) end);
+      in eval ctxt pos (Token.read_antiq keywords parse_antiq (body, pos)) end);
 
 end;
 
diff -r cc6a21413f8a -r a80d8ec6c998 src/Pure/Thy/document_antiquotations.ML
--- a/src/Pure/Thy/document_antiquotations.ML	Thu Jan 03 22:30:41 2019 +0100
+++ b/src/Pure/Thy/document_antiquotations.ML	Fri Jan 04 21:49:06 2019 +0100
@@ -62,7 +62,7 @@
 fun pretty_theory ctxt (name, pos) =
   (Theory.check {long = true} ctxt (name, pos); Pretty.str name);
 
-val basic_entity = Thy_Output.antiquotation_pretty_source;
+val basic_entity = Thy_Output.antiquotation_pretty_source_embedded;
 
 fun basic_entities name scan pretty =
   Document_Antiquotation.setup name scan
@@ -132,7 +132,7 @@
 local
 
 fun control_antiquotation name s1 s2 =
-  Thy_Output.antiquotation_raw name (Scan.lift Args.cartouche_input)
+  Thy_Output.antiquotation_raw_embedded name (Scan.lift Args.cartouche_input)
     (fn ctxt => Latex.enclose_block s1 s2 o Thy_Output.output_document ctxt {markdown = false});
 
 in
@@ -158,7 +158,7 @@
   Input.source_content #> #1 #> Document_Antiquotation.prepare_lines ctxt;
 
 fun text_antiquotation name =
-  Thy_Output.antiquotation_raw name (Scan.lift Args.text_input)
+  Thy_Output.antiquotation_raw_embedded name (Scan.lift Args.text_input)
     (fn ctxt => fn text =>
       let
         val _ = report_text ctxt text;
@@ -169,7 +169,7 @@
       end);
 
 val theory_text_antiquotation =
-  Thy_Output.antiquotation_raw \<^binding>\<open>theory_text\<close> (Scan.lift Args.text_input)
+  Thy_Output.antiquotation_raw_embedded \<^binding>\<open>theory_text\<close> (Scan.lift Args.text_input)
     (fn ctxt => fn text =>
       let
         val keywords = Thy_Header.get_keywords' ctxt;
@@ -243,7 +243,7 @@
 (* verbatim text *)
 
 val _ = Theory.setup
-  (Thy_Output.antiquotation_verbatim \<^binding>\<open>verbatim\<close> (Scan.lift Args.text_input)
+  (Thy_Output.antiquotation_verbatim_embedded \<^binding>\<open>verbatim\<close> (Scan.lift Args.text_input)
     (fn ctxt => fn text =>
       let
         val _ =
@@ -257,7 +257,7 @@
 local
 
 fun ml_text name ml =
-  Thy_Output.antiquotation_verbatim name (Scan.lift Args.text_input)
+  Thy_Output.antiquotation_verbatim_embedded name (Scan.lift Args.text_input)
     (fn ctxt => fn text =>
       let val _ = ML_Context.eval_in (SOME ctxt) ML_Compiler.flags (Input.pos_of text) (ml text)
       in #1 (Input.source_content text) end);
@@ -287,7 +287,7 @@
 (* URLs *)
 
 val _ = Theory.setup
-  (Thy_Output.antiquotation_raw \<^binding>\<open>url\<close> (Scan.lift Args.embedded_position)
+  (Thy_Output.antiquotation_raw_embedded \<^binding>\<open>url\<close> (Scan.lift Args.embedded_position)
     (fn ctxt => fn (url, pos) =>
       let val _ = Context_Position.reports ctxt [(pos, Markup.language_path), (pos, Markup.url url)]
       in Latex.enclose_block "\\url{" "}" [Latex.string url] end));
diff -r cc6a21413f8a -r a80d8ec6c998 src/Pure/Thy/thy_output.ML
--- a/src/Pure/Thy/thy_output.ML	Thu Jan 03 22:30:41 2019 +0100
+++ b/src/Pure/Thy/thy_output.ML	Fri Jan 04 21:49:06 2019 +0100
@@ -27,12 +27,20 @@
   val pretty_items_source: Proof.context -> Token.src -> Pretty.T list -> Latex.text
   val antiquotation_pretty:
     binding -> 'a context_parser -> (Proof.context -> 'a -> Pretty.T) -> theory -> theory
+  val antiquotation_pretty_embedded:
+    binding -> 'a context_parser -> (Proof.context -> 'a -> Pretty.T) -> theory -> theory
   val antiquotation_pretty_source:
     binding -> 'a context_parser -> (Proof.context -> 'a -> Pretty.T) -> theory -> theory
+  val antiquotation_pretty_source_embedded:
+    binding -> 'a context_parser -> (Proof.context -> 'a -> Pretty.T) -> theory -> theory
   val antiquotation_raw:
     binding -> 'a context_parser -> (Proof.context -> 'a -> Latex.text) -> theory -> theory
+  val antiquotation_raw_embedded:
+    binding -> 'a context_parser -> (Proof.context -> 'a -> Latex.text) -> theory -> theory
   val antiquotation_verbatim:
     binding -> 'a context_parser -> (Proof.context -> 'a -> string) -> theory -> theory
+  val antiquotation_verbatim_embedded:
+    binding -> 'a context_parser -> (Proof.context -> 'a -> string) -> theory -> theory
 end;
 
 structure Thy_Output: THY_OUTPUT =
@@ -525,19 +533,40 @@
 
 (* antiquotation variants *)
 
-fun antiquotation_pretty name scan f =
-  Document_Antiquotation.setup name scan
-    (fn {context = ctxt, argument = x, ...} => pretty ctxt (f ctxt x));
+local
 
-fun antiquotation_pretty_source name scan f =
-  Document_Antiquotation.setup name scan
+fun gen_setup name embedded =
+  if embedded
+  then Document_Antiquotation.setup_embedded name
+  else Document_Antiquotation.setup name;
+
+fun gen_antiquotation_pretty name embedded scan f =
+  gen_setup name embedded scan (fn {context = ctxt, argument = x, ...} => pretty ctxt (f ctxt x));
+
+fun gen_antiquotation_pretty_source name embedded scan f =
+  gen_setup name embedded scan
     (fn {context = ctxt, source = src, argument = x} => pretty_source ctxt src (f ctxt x));
 
-fun antiquotation_raw name scan f =
-  Document_Antiquotation.setup name scan
-    (fn {context = ctxt, argument = x, ...} => f ctxt x);
+fun gen_antiquotation_raw name embedded scan f =
+  gen_setup name embedded scan (fn {context = ctxt, argument = x, ...} => f ctxt x);
+
+fun gen_antiquotation_verbatim name embedded scan f =
+  gen_antiquotation_raw name embedded scan (fn ctxt => verbatim ctxt o f ctxt);
+
+in
 
-fun antiquotation_verbatim name scan f =
-  antiquotation_raw name scan (fn ctxt => verbatim ctxt o f ctxt);
+fun antiquotation_pretty name = gen_antiquotation_pretty name false;
+fun antiquotation_pretty_embedded name = gen_antiquotation_pretty name true;
+
+fun antiquotation_pretty_source name = gen_antiquotation_pretty_source name false;
+fun antiquotation_pretty_source_embedded name = gen_antiquotation_pretty_source name true;
+
+fun antiquotation_raw name = gen_antiquotation_raw name false;
+fun antiquotation_raw_embedded name = gen_antiquotation_raw name true;
+
+fun antiquotation_verbatim name = gen_antiquotation_verbatim name false;
+fun antiquotation_verbatim_embedded name = gen_antiquotation_verbatim name true;
 
 end;
+
+end;
diff -r cc6a21413f8a -r a80d8ec6c998 src/Pure/Tools/jedit.ML
--- a/src/Pure/Tools/jedit.ML	Thu Jan 03 22:30:41 2019 +0100
+++ b/src/Pure/Tools/jedit.ML	Fri Jan 04 21:49:06 2019 +0100
@@ -74,7 +74,7 @@
 
 val _ =
   Theory.setup
-    (Thy_Output.antiquotation_verbatim \<^binding>\<open>action\<close> (Scan.lift Args.embedded_position)
+    (Thy_Output.antiquotation_verbatim_embedded \<^binding>\<open>action\<close> (Scan.lift Args.embedded_position)
       (fn ctxt => fn (name, pos) =>
         let
           val _ =
diff -r cc6a21413f8a -r a80d8ec6c998 src/Pure/Tools/named_theorems.ML
--- a/src/Pure/Tools/named_theorems.ML	Thu Jan 03 22:30:41 2019 +0100
+++ b/src/Pure/Tools/named_theorems.ML	Fri Jan 04 21:49:06 2019 +0100
@@ -103,7 +103,7 @@
 (* ML antiquotation *)
 
 val _ = Theory.setup
-  (ML_Antiquotation.inline \<^binding>\<open>named_theorems\<close>
+  (ML_Antiquotation.inline_embedded \<^binding>\<open>named_theorems\<close>
     (Args.context -- Scan.lift Args.embedded_position >>
       (fn (ctxt, name) => ML_Syntax.print_string (check ctxt name))));
 
diff -r cc6a21413f8a -r a80d8ec6c998 src/Pure/Tools/plugin.ML
--- a/src/Pure/Tools/plugin.ML	Thu Jan 03 22:30:41 2019 +0100
+++ b/src/Pure/Tools/plugin.ML	Fri Jan 04 21:49:06 2019 +0100
@@ -40,7 +40,7 @@
   #1 o Name_Space.check (Context.Proof ctxt) (Data.get (Proof_Context.theory_of ctxt));
 
 val _ = Theory.setup
-  (ML_Antiquotation.inline \<^binding>\<open>plugin\<close>
+  (ML_Antiquotation.inline_embedded \<^binding>\<open>plugin\<close>
     (Args.context -- Scan.lift Args.embedded_position >> (ML_Syntax.print_string o uncurry check)));
 
 
diff -r cc6a21413f8a -r a80d8ec6c998 src/Pure/Tools/rail.ML
--- a/src/Pure/Tools/rail.ML	Thu Jan 03 22:30:41 2019 +0100
+++ b/src/Pure/Tools/rail.ML	Fri Jan 04 21:49:06 2019 +0100
@@ -384,7 +384,7 @@
   in Latex.string (Latex.environment "railoutput" (implode (map output_rule rules))) end;
 
 val _ = Theory.setup
-  (Thy_Output.antiquotation_raw \<^binding>\<open>rail\<close> (Scan.lift Args.text_input)
+  (Thy_Output.antiquotation_raw_embedded \<^binding>\<open>rail\<close> (Scan.lift Args.text_input)
     (fn ctxt => output_rules ctxt o read ctxt));
 
 end;
diff -r cc6a21413f8a -r a80d8ec6c998 src/Pure/simplifier.ML
--- a/src/Pure/simplifier.ML	Thu Jan 03 22:30:41 2019 +0100
+++ b/src/Pure/simplifier.ML	Fri Jan 04 21:49:06 2019 +0100
@@ -114,7 +114,7 @@
 val the_simproc = Name_Space.get o get_simprocs;
 
 val _ = Theory.setup
-  (ML_Antiquotation.value \<^binding>\<open>simproc\<close>
+  (ML_Antiquotation.value_embedded \<^binding>\<open>simproc\<close>
     (Args.context -- Scan.lift Args.embedded_position
       >> (fn (ctxt, name) =>
         "Simplifier.the_simproc ML_context " ^ ML_Syntax.print_string (check_simproc ctxt name))));