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