# HG changeset patch
# User wenzelm
# Date 1459261248 -7200
# Node ID eba34ff9671c647582ac79e8d588a83ed81e1fbf
# Parent  aa0084adce1f024171788f808503a28b2a0f65a9
clarified reports;
tuned signature;

diff -r aa0084adce1f -r eba34ff9671c src/Pure/General/antiquote.ML
--- a/src/Pure/General/antiquote.ML	Tue Mar 29 14:03:26 2016 +0200
+++ b/src/Pure/General/antiquote.ML	Tue Mar 29 16:20:48 2016 +0200
@@ -16,7 +16,7 @@
   val scan_control: Symbol_Pos.T list -> control * Symbol_Pos.T list
   val scan_antiq: Symbol_Pos.T list -> antiq * Symbol_Pos.T list
   val scan_antiquote: Symbol_Pos.T list -> text_antiquote * Symbol_Pos.T list
-  val read': Position.T -> Symbol_Pos.T list -> text_antiquote list
+  val parse: Position.T -> Symbol_Pos.T list -> text_antiquote list
   val read: Input.source -> text_antiquote list
 end;
 
@@ -123,11 +123,15 @@
 
 (* read *)
 
-fun read' pos syms =
+fun parse pos syms =
   (case Scan.read Symbol_Pos.stopper (Scan.repeat scan_antiquote) syms of
-    SOME ants => (Position.reports (antiq_reports ants); ants)
+    SOME ants => ants
   | NONE => error ("Malformed quotation/antiquotation source" ^ Position.here pos));
 
-fun read source = read' (Input.pos_of source) (Input.source_explode source);
+fun read source =
+  let
+    val ants = parse (Input.pos_of source) (Input.source_explode source);
+    val _ = Position.reports (antiq_reports ants);
+  in ants end;
 
 end;
diff -r aa0084adce1f -r eba34ff9671c src/Pure/Thy/thy_output.ML
--- a/src/Pure/Thy/thy_output.ML	Tue Mar 29 14:03:26 2016 +0200
+++ b/src/Pure/Thy/thy_output.ML	Tue Mar 29 16:20:48 2016 +0200
@@ -195,10 +195,19 @@
 
 fun output_text state {markdown} source =
   let
+    val is_reported =
+      (case try Toplevel.context_of state of
+        SOME ctxt => Context_Position.is_visible ctxt
+      | NONE => true);
+
     val pos = Input.pos_of source;
-    val _ = Position.report pos (Markup.language_document (Input.is_delimited source));
     val syms = Input.source_explode source;
 
+    val _ =
+      if is_reported then
+        Position.report pos (Markup.language_document (Input.is_delimited source))
+      else ();
+
     val output_antiquotes = map (eval_antiquote state) #> implode;
 
     fun output_line line =
@@ -214,14 +223,16 @@
     else if markdown andalso exists (Markdown.is_control o Symbol_Pos.symbol) syms
     then
       let
-        val ants = Antiquote.read' pos syms;
+        val ants = Antiquote.parse pos syms;
+        val reports = Antiquote.antiq_reports ants;
         val blocks = Markdown.read_antiquotes ants;
-        val _ = Position.reports (Markdown.reports blocks);
+        val _ = if is_reported then Position.reports (reports @ Markdown.reports blocks) else ();
       in output_blocks blocks end
     else
       let
-        val ants = Antiquote.read' pos (Symbol_Pos.trim_blanks syms);
-        val _ = Position.reports (Markdown.text_reports ants);
+        val ants = Antiquote.parse pos (Symbol_Pos.trim_blanks syms);
+        val reports = Antiquote.antiq_reports ants;
+        val _ = if is_reported then Position.reports (reports @ Markdown.text_reports ants) else ();
       in output_antiquotes ants end
   end;