src/Pure/pure_syn.ML
changeset 73752 eeb076fc569f
parent 73751 fefb5ccb1e5e
child 73761 ef1a18e20ace
--- 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 =>