src/Pure/Syntax/syntax.ML
changeset 69589 e15f053a42d8
parent 69576 cfac69e7b962
child 69971 4e98239aa083
equal deleted inserted replaced
69588:2b85a9294b2a 69589:e15f053a42d8
   201       let
   201       let
   202         val source = input_source tree;
   202         val source = input_source tree;
   203         val syms = Input.source_explode source;
   203         val syms = Input.source_explode source;
   204         val pos = Input.pos_of source;
   204         val pos = Input.pos_of source;
   205         val _ = Context_Position.report ctxt pos (markup (Input.is_delimited source));
   205         val _ = Context_Position.report ctxt pos (markup (Input.is_delimited source));
       
   206         val _ =
       
   207           if Options.default_bool "update_inner_syntax_cartouches" then
       
   208             Context_Position.report_text ctxt
       
   209               pos Markup.update (cartouche (Symbol_Pos.content syms))
       
   210           else ();
   206       in parse (syms, pos) end;
   211       in parse (syms, pos) end;
   207   in
   212   in
   208     (case YXML.parse_body str handle Fail msg => error msg of
   213     (case YXML.parse_body str handle Fail msg => error msg of
   209       body as [tree as XML.Elem ((name, _), _)] =>
   214       body as [tree as XML.Elem ((name, _), _)] =>
   210         if name = Markup.inputN then parse_tree tree else decode body
   215         if name = Markup.inputN then parse_tree tree else decode body