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;