src/Pure/Syntax/syntax.ML

--- a/src/Pure/Syntax/syntax.ML	Thu Jan 03 21:36:58 2019 +0100
+++ b/src/Pure/Syntax/syntax.ML	Thu Jan 03 21:48:05 2019 +0100
@@ -203,6 +203,11 @@
         val syms = Input.source_explode source;
         val pos = Input.pos_of source;
         val _ = Context_Position.report ctxt pos (markup (Input.is_delimited source));
+        val _ =
+          if Options.default_bool "update_inner_syntax_cartouches" then
+            Context_Position.report_text ctxt
+              pos Markup.update (cartouche (Symbol_Pos.content syms))
+          else ();
       in parse (syms, pos) end;
   in
     (case YXML.parse_body str handle Fail msg => error msg of