# HG changeset patch
# User wenzelm
# Date 1517665157 -3600
# Node ID 5d71b114e7a3dfc576f6fe2145f684c1c50c797d
# Parent  fc2b303070dafbc30eff4fec8a14d50dff4baad1
avoid proliferation of language_document reports;
clarified signature;

diff -r fc2b303070da -r 5d71b114e7a3 src/Pure/PIDE/command.ML
--- a/src/Pure/PIDE/command.ML	Sat Feb 03 14:32:12 2018 +0100
+++ b/src/Pure/PIDE/command.ML	Sat Feb 03 14:39:17 2018 +0100
@@ -207,7 +207,8 @@
         check_error (fn () => Thy_Output.check_token_comments ctxt tok))) @
       (span |> maps (fn tok =>
         if Token.kind_of tok = Token.Comment (SOME Comment.Comment) then
-          check_error (fn () => Thy_Output.output_text ctxt {markdown = false} (Token.input_of tok))
+          check_error (fn () =>
+            Thy_Output.output_document ctxt {markdown = false} (Token.input_of tok))
         else [])))
     ();
 
diff -r fc2b303070da -r 5d71b114e7a3 src/Pure/Thy/document_antiquotations.ML
--- a/src/Pure/Thy/document_antiquotations.ML	Sat Feb 03 14:32:12 2018 +0100
+++ b/src/Pure/Thy/document_antiquotations.ML	Sat Feb 03 14:39:17 2018 +0100
@@ -133,7 +133,7 @@
 
 fun control_antiquotation name s1 s2 =
   Thy_Output.antiquotation_raw name (Scan.lift Args.cartouche_input)
-    (fn ctxt => Latex.enclose_block s1 s2 o Thy_Output.output_text ctxt {markdown = false});
+    (fn ctxt => Latex.enclose_block s1 s2 o Thy_Output.output_document ctxt {markdown = false});
 
 in
 
diff -r fc2b303070da -r 5d71b114e7a3 src/Pure/Thy/thy_output.ML
--- a/src/Pure/Thy/thy_output.ML	Sat Feb 03 14:32:12 2018 +0100
+++ b/src/Pure/Thy/thy_output.ML	Sat Feb 03 14:39:17 2018 +0100
@@ -6,7 +6,7 @@
 
 signature THY_OUTPUT =
 sig
-  val output_text: Proof.context -> {markdown: bool} -> Input.source -> Latex.text list
+  val output_document: Proof.context -> {markdown: bool} -> Input.source -> Latex.text list
   val check_comments: Proof.context -> Symbol_Pos.T list -> unit
   val check_token_comments: Proof.context -> Token.T -> unit
   val output_token: Proof.context -> Token.T -> Latex.text list
@@ -39,15 +39,13 @@
 structure Thy_Output: THY_OUTPUT =
 struct
 
-(* output text *)
+(* output document source *)
 
-fun output_text ctxt {markdown} source =
+fun output_document ctxt {markdown} source =
   let
     val pos = Input.pos_of source;
     val syms = Input.source_explode source;
 
-    val _ = Context_Position.report ctxt pos (Markup.language_document (Input.is_delimited source));
-
     val output_antiquotes = maps (Document_Antiquotation.evaluate ctxt);
 
     fun output_line line =
@@ -104,7 +102,7 @@
         val ctxt' = ctxt
           |> Config.put Document_Antiquotation.thy_output_display false;
       in
-        output_text ctxt' {markdown = false} source
+        output_document ctxt' {markdown = false} source
         |> Latex.enclose_body "%\n\\isamarkupcmt{" "%\n}"
       end
   | (SOME Comment.Cancel, _) =>
@@ -192,11 +190,11 @@
   | Basic_Token tok => output_token ctxt tok
   | Markup_Token (cmd, source) =>
       Latex.enclose_body ("%\n\\isamarkup" ^ cmd ^ "{") "%\n}\n"
-        (output_text ctxt {markdown = false} source)
+        (output_document ctxt {markdown = false} source)
   | Markup_Env_Token (cmd, source) =>
-      [Latex.environment_block ("isamarkup" ^ cmd) (output_text ctxt {markdown = true} source)]
+      [Latex.environment_block ("isamarkup" ^ cmd) (output_document ctxt {markdown = true} source)]
   | Raw_Token source =>
-      Latex.string "%\n" :: output_text ctxt {markdown = true} source @ [Latex.string "\n"]);
+      Latex.string "%\n" :: output_document ctxt {markdown = true} source @ [Latex.string "\n"]);
 
 
 (* command spans *)
diff -r fc2b303070da -r 5d71b114e7a3 src/Pure/pure_syn.ML
--- a/src/Pure/pure_syn.ML	Sat Feb 03 14:32:12 2018 +0100
+++ b/src/Pure/pure_syn.ML	Sat Feb 03 14:39:17 2018 +0100
@@ -17,16 +17,22 @@
 
 val semi = Scan.option (Parse.$$$ ";");
 
-fun document_command {markdown} (loc, txt) =
+fun output_document state markdown txt =
+  let
+    val ctxt = Toplevel.presentation_context state;
+    val _ =
+      Context_Position.report ctxt
+        (Input.pos_of txt) (Markup.language_document (Input.is_delimited txt));
+  in Thy_Output.output_document ctxt markdown txt end;
+
+fun document_command markdown (loc, txt) =
   Toplevel.keep (fn state =>
     (case loc of
-      NONE =>
-        ignore (Thy_Output.output_text
-          (Toplevel.presentation_context state) {markdown = markdown} txt)
+      NONE => ignore (output_document state markdown txt)
     | SOME (_, pos) =>
         error ("Illegal target specification -- not a theory context" ^ Position.here pos))) o
   Toplevel.present_local_theory loc (fn state =>
-    ignore (Thy_Output.output_text (Toplevel.presentation_context state) {markdown = markdown} txt));
+    ignore (output_document state markdown txt));
 
 val _ =
   Outer_Syntax.command ("chapter", \<^here>) "chapter heading"