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 *)