# HG changeset patch
# User wenzelm
# Date 1621511420 -7200
# Node ID eeb076fc569f7b91c9bcdd98b6f0bd545f4ecf05
# Parent  fefb5ccb1e5ed86c1e7e4b62a186933d0f8e2d25
tuned signature;

diff -r fefb5ccb1e5e -r eeb076fc569f src/Pure/Thy/document_antiquotations.ML
--- a/src/Pure/Thy/document_antiquotations.ML	Wed May 19 21:42:45 2021 +0200
+++ b/src/Pure/Thy/document_antiquotations.ML	Thu May 20 13:50:20 2021 +0200
@@ -133,7 +133,9 @@
 
 fun control_antiquotation name s1 s2 =
   Thy_Output.antiquotation_raw_embedded name (Scan.lift Args.cartouche_input)
-    (fn ctxt => Latex.enclose_block s1 s2 o Thy_Output.output_document ctxt {markdown = false});
+    (fn ctxt => fn txt =>
+      (Context_Position.reports ctxt (Thy_Output.document_reports txt);
+        Latex.enclose_block s1 s2 (Thy_Output.output_document ctxt {markdown = false} txt)));
 
 in
 
diff -r fefb5ccb1e5e -r eeb076fc569f src/Pure/Thy/thy_output.ML
--- a/src/Pure/Thy/thy_output.ML	Wed May 19 21:42:45 2021 +0200
+++ b/src/Pure/Thy/thy_output.ML	Thu May 20 13:50:20 2021 +0200
@@ -6,8 +6,8 @@
 
 signature THY_OUTPUT =
 sig
+  val document_reports: Input.source -> Position.report list
   val output_document: Proof.context -> {markdown: bool} -> Input.source -> Latex.text list
-  val output_document_report: Proof.context -> {markdown: bool} -> Input.source -> Latex.text list
   val check_comments: Proof.context -> Symbol_Pos.T list -> unit
   val output_token: Proof.context -> Token.T -> Latex.text list
   val output_source: Proof.context -> string -> Latex.text list
@@ -52,6 +52,12 @@
 
 (* output document source *)
 
+fun document_reports txt =
+  let val pos = Input.pos_of txt in
+    [(pos, Markup.language_document (Input.is_delimited txt)),
+     (pos, Markup.plain_text)]
+  end;
+
 val output_symbols = single o Latex.symbols_output;
 
 fun output_comment ctxt (kind, syms) =
@@ -108,16 +114,6 @@
       in output_antiquotes ants end
   end;
 
-fun output_document_report ctxt markdown txt =
-  let
-    val pos = Input.pos_of txt;
-    val _ =
-      Context_Position.reports ctxt
-        [(pos, Markup.language_document (Input.is_delimited txt)),
-         (pos, Markup.plain_text)];
-  in output_document ctxt markdown txt end;
-
-
 
 (* output tokens with formal comments *)
 
diff -r fefb5ccb1e5e -r eeb076fc569f src/Pure/pure_syn.ML
--- a/src/Pure/pure_syn.ML	Wed May 19 21:42:45 2021 +0200
+++ b/src/Pure/pure_syn.ML	Thu May 20 13:50:20 2021 +0200
@@ -17,8 +17,11 @@
 
 val semi = Scan.option (Parse.$$$ ";");
 
-val output_document =
-  Thy_Output.output_document_report o Toplevel.presentation_context;
+fun output_document state markdown txt =
+  let
+    val ctxt = Toplevel.presentation_context state;
+    val _ = Context_Position.reports ctxt (Thy_Output.document_reports txt);
+  in Thy_Output.output_document ctxt markdown txt end;
 
 fun document_command markdown (loc, txt) =
   Toplevel.keep (fn state =>