# HG changeset patch
# User wenzelm
# Date 1621453365 -7200
# Node ID fefb5ccb1e5ed86c1e7e4b62a186933d0f8e2d25
# Parent  c7a57fc472207f34aaf6fedabf1497c9af96d6a4
clarified modules;

diff -r c7a57fc47220 -r fefb5ccb1e5e src/Pure/Thy/thy_output.ML
--- a/src/Pure/Thy/thy_output.ML	Wed May 19 18:22:56 2021 +0200
+++ b/src/Pure/Thy/thy_output.ML	Wed May 19 21:42:45 2021 +0200
@@ -7,6 +7,7 @@
 signature THY_OUTPUT =
 sig
   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
@@ -107,6 +108,16 @@
       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 c7a57fc47220 -r fefb5ccb1e5e src/Pure/pure_syn.ML
--- a/src/Pure/pure_syn.ML	Wed May 19 18:22:56 2021 +0200
+++ b/src/Pure/pure_syn.ML	Wed May 19 21:42:45 2021 +0200
@@ -17,15 +17,8 @@
 
 val semi = Scan.option (Parse.$$$ ";");
 
-fun output_document state markdown txt =
-  let
-    val ctxt = Toplevel.presentation_context state;
-    val pos = Input.pos_of txt;
-    val _ =
-      Context_Position.reports ctxt
-        [(pos, Markup.language_document (Input.is_delimited txt)),
-         (pos, Markup.plain_text)];
-  in Thy_Output.output_document ctxt markdown txt end;
+val output_document =
+  Thy_Output.output_document_report o Toplevel.presentation_context;
 
 fun document_command markdown (loc, txt) =
   Toplevel.keep (fn state =>