--- a/src/Pure/Thy/document_output.ML Tue Nov 23 21:43:45 2021 +0100
+++ b/src/Pure/Thy/document_output.ML Wed Nov 24 15:33:43 2021 +0100
@@ -8,7 +8,7 @@
sig
val document_reports: Input.source -> Position.report list
val output_document: Proof.context -> {markdown: bool} -> Input.source -> Latex.text
- val document_output: {markdown: bool, markup: Position.T -> Latex.text -> Latex.text} ->
+ val document_output: {markdown: bool, markup: Latex.text -> Latex.text} ->
(xstring * Position.T) option * Input.source -> Toplevel.transition -> Toplevel.transition
val check_comments: Proof.context -> Symbol_Pos.T list -> unit
val output_token: Proof.context -> Token.T -> Latex.text
@@ -119,7 +119,7 @@
let
val ctxt = Toplevel.presentation_context st;
val _ = Context_Position.reports ctxt (document_reports txt);
- in txt |> output_document ctxt {markdown = markdown} |> markup (Position.thread_data ()) end;
+ in txt |> output_document ctxt {markdown = markdown} |> markup end;
in
Toplevel.present (fn st =>
(case loc of