src/Pure/Syntax/syntax.ML

       let
         val source = input_source tree;
         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
       body as [tree as XML.Elem ((name, _), _)] =>
         if name = Markup.inputN then parse_tree tree else decode body