more accurate markup;
authorwenzelm
Sun Mar 24 17:45:00 2019 +0100 (2 months ago)
changeset 699678a9d0d894ec0
parent 69966 cba5b866c633
child 69968 1a400b14fd3a
more accurate markup;
src/Pure/Thy/document_marker.ML
     1.1 --- a/src/Pure/Thy/document_marker.ML	Sun Mar 24 17:33:11 2019 +0100
     1.2 +++ b/src/Pure/Thy/document_marker.ML	Sun Mar 24 17:45:00 2019 +0100
     1.3 @@ -49,14 +49,17 @@
     1.4  
     1.5  fun evaluate input ctxt =
     1.6    let
     1.7 -    val body =
     1.8 -      Input.source_explode input
     1.9 -      |> drop_prefix (fn (s, _) => s = Symbol.marker)
    1.10 -      |> Symbol_Pos.cartouche_content;
    1.11 +    val syms = Input.source_explode input
    1.12 +      |> drop_prefix (fn (s, _) => s = Symbol.marker);
    1.13 +    val pos = #1 (Symbol_Pos.range syms);
    1.14 +
    1.15 +    val _ = Context_Position.reports ctxt (map (pair pos) (Comment.kind_markups Comment.Marker));
    1.16 +
    1.17 +    val body = Symbol_Pos.cartouche_content syms;
    1.18      val markers =
    1.19        (case Token.read_body (Thy_Header.get_keywords' ctxt) (Parse.list parse_marker) body of
    1.20          SOME res => res
    1.21 -      | NONE => error ("Bad input" ^ Position.here (Input.pos_of input)));
    1.22 +      | NONE => error ("Bad input" ^ Position.here pos));
    1.23    in fold (fn src => #2 (check ctxt (Token.name_of_src src)) src) markers ctxt end;
    1.24  
    1.25