# HG changeset patch
# User wenzelm
# Date 1553445900 -3600
# Node ID 8a9d0d894ec0339a20d098a9c63052f170f74124
# Parent  cba5b866c633f76f9c3eaa30aa87d9f2a30c6cb4
more accurate markup;

diff -r cba5b866c633 -r 8a9d0d894ec0 src/Pure/Thy/document_marker.ML
--- a/src/Pure/Thy/document_marker.ML	Sun Mar 24 17:33:11 2019 +0100
+++ b/src/Pure/Thy/document_marker.ML	Sun Mar 24 17:45:00 2019 +0100
@@ -49,14 +49,17 @@
 
 fun evaluate input ctxt =
   let
-    val body =
-      Input.source_explode input
-      |> drop_prefix (fn (s, _) => s = Symbol.marker)
-      |> Symbol_Pos.cartouche_content;
+    val syms = Input.source_explode input
+      |> drop_prefix (fn (s, _) => s = Symbol.marker);
+    val pos = #1 (Symbol_Pos.range syms);
+
+    val _ = Context_Position.reports ctxt (map (pair pos) (Comment.kind_markups Comment.Marker));
+
+    val body = Symbol_Pos.cartouche_content syms;
     val markers =
       (case Token.read_body (Thy_Header.get_keywords' ctxt) (Parse.list parse_marker) body of
         SOME res => res
-      | NONE => error ("Bad input" ^ Position.here (Input.pos_of input)));
+      | NONE => error ("Bad input" ^ Position.here pos));
   in fold (fn src => #2 (check ctxt (Token.name_of_src src)) src) markers ctxt end;