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