clarified markup;
authorwenzelm
Sun Mar 24 19:17:42 2019 +0100 (3 weeks ago)
changeset 699714e98239aa083
parent 69970 b5a47478897a
child 69972 5e82015fa879
clarified markup;
src/Pure/Syntax/syntax.ML
     1.1 --- a/src/Pure/Syntax/syntax.ML	Sun Mar 24 18:38:42 2019 +0100
     1.2 +++ b/src/Pure/Syntax/syntax.ML	Sun Mar 24 19:17:42 2019 +0100
     1.3 @@ -202,7 +202,9 @@
     1.4          val source = input_source tree;
     1.5          val syms = Input.source_explode source;
     1.6          val pos = Input.pos_of source;
     1.7 -        val _ = Context_Position.report ctxt pos (markup (Input.is_delimited source));
     1.8 +        val _ =
     1.9 +          Context_Position.reports ctxt
    1.10 +            [(pos, Markup.cartouche), (pos, markup (Input.is_delimited source))];
    1.11          val _ =
    1.12            if Options.default_bool "update_inner_syntax_cartouches" then
    1.13              Context_Position.report_text ctxt