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