output for document commands like 'section', 'text' is defined in user-space, as part of the command transaction;

--- a/src/Pure/Isar/token.ML	Tue Nov 23 12:29:09 2021 +0100
+++ b/src/Pure/Isar/token.ML	Tue Nov 23 16:06:09 2021 +0100
@@ -31,7 +31,8 @@
     Fact of string option * thm list |
     Attribute of morphism -> attribute |
     Declaration of declaration |
-    Files of file Exn.result list
+    Files of file Exn.result list |
+    Output of XML.body option
   val pos_of: T -> Position.T
   val adjust_offsets: (int -> int option) -> T -> T
   val eof: T
@@ -73,6 +74,8 @@
   val file_source: file -> Input.source
   val get_files: T -> file Exn.result list
   val put_files: file Exn.result list -> T -> T
+  val get_output: T -> XML.body option
+  val put_output: XML.body -> T -> T
   val get_value: T -> value option
   val reports_of_value: T -> Position.report list
   val name_value: name_value -> value
@@ -197,7 +200,8 @@
   Fact of string option * thm list |  (*optional name for dynamic fact, i.e. fact "variable"*)
   Attribute of morphism -> attribute |
   Declaration of declaration |
-  Files of file Exn.result list;
+  Files of file Exn.result list |
+  Output of XML.body option;
 
 type src = T list;
 
@@ -411,6 +415,15 @@
   | put_files _ tok = raise Fail ("Cannot put inlined files here" ^ Position.here (pos_of tok));
 
 
+(* document output *)
+
+fun get_output (Token (_, _, Value (SOME (Output output)))) = output
+  | get_output _ = NONE;
+
+fun put_output output (Token (x, y, Slot)) = Token (x, y, Value (SOME (Output (SOME output))))
+  | put_output _ tok = raise Fail ("Cannot put document output here" ^ Position.here (pos_of tok));
+
+
 (* access values *)
 
 fun get_value (Token (_, _, Value v)) = v
@@ -491,7 +504,8 @@
     | Fact (a, ths) => Fact (a, Morphism.fact phi ths)
     | Attribute att => Attribute (Morphism.transform phi att)
     | Declaration decl => Declaration (Morphism.transform phi decl)
-    | Files _ => v));
+    | Files _ => v
+    | Output _ => v));
 
 
 (* static binding *)

--- a/src/Pure/Isar/toplevel.ML	Tue Nov 23 12:29:09 2021 +0100
+++ b/src/Pure/Isar/toplevel.ML	Tue Nov 23 16:06:09 2021 +0100
@@ -17,6 +17,7 @@
   val is_skipped_proof: state -> bool
   val level: state -> int
   val previous_theory_of: state -> theory option
+  val output_of: state -> Latex.text option
   val context_of: state -> Proof.context
   val generic_theory_of: state -> generic_theory
   val theory_of: state -> theory
@@ -139,20 +140,20 @@
 fun node_presentation node =
   (node, cases_node init_presentation Context.proof_of Proof.context_of node);
 
-
 datatype state =
-  State of node_presentation * theory option;
-    (*current node with presentation context, previous theory*)
+  State of node_presentation * (theory option * Latex.text option);
+    (*current node with presentation context, previous theory, document output*)
 
 fun node_of (State ((node, _), _)) = node;
-fun previous_theory_of (State (_, prev_thy)) = prev_thy;
+fun previous_theory_of (State (_, (prev_thy, _))) = prev_thy;
+fun output_of (State (_, (_, output))) = output;
 
-fun init_toplevel () = State (node_presentation Toplevel, NONE);
-fun theory_toplevel thy = State (node_presentation (Theory (Context.Theory thy)), NONE);
+fun init_toplevel () = State (node_presentation Toplevel, (NONE, NONE));
+fun theory_toplevel thy = State (node_presentation (Theory (Context.Theory thy)), (NONE, NONE));
 
 val prev_theory = Config.declare_int ("prev_theory", Position.none) (K 0);
 fun get_prev_theory thy = Config.get_global thy prev_theory;
-fun set_prev_theory (State (_, SOME prev_thy)) (Theory gthy) =
+fun set_prev_theory (State (_, (SOME prev_thy, _))) (Theory gthy) =
       let
         val put = Config.put_global prev_theory (Context.theory_identifier prev_thy);
         val gthy' = gthy |> Context.mapping put (Local_Theory.raw_theory put);
@@ -204,10 +205,10 @@
     Proof (prf, _) => Proof_Node.position prf
   | _ => ~1);
 
-fun is_end_theory (State ((Toplevel, _), SOME _)) = true
+fun is_end_theory (State ((Toplevel, _), (SOME _, _))) = true
   | is_end_theory _ = false;
 
-fun end_theory _ (State ((Toplevel, _), SOME thy)) = thy
+fun end_theory _ (State ((Toplevel, _), (SOME thy, _))) = thy
   | end_theory pos _ = error ("Malformed theory" ^ Position.here pos);
 
 
@@ -223,11 +224,11 @@
 
 fun presentation_context (state as State (current, _)) =
   presentation_context0 state
-  |> Presentation_State.put (SOME (State (current, NONE)));
+  |> Presentation_State.put (SOME (State (current, (NONE, NONE))));
 
 fun presentation_state ctxt =
   (case Presentation_State.get ctxt of
-    NONE => State (node_presentation (Theory (Context.Proof ctxt)), NONE)
+    NONE => State (node_presentation (Theory (Context.Proof ctxt)), (NONE, NONE))
   | SOME state => state);
 
 
@@ -286,28 +287,29 @@
 
 exception FAILURE of state * exn;
 
+fun apply_presentation g (st as State (node, (prev_thy, _))) =
+  State (node, (prev_thy, g st));
+
 fun apply f g node =
   let
     val node_pr = node_presentation node;
     val context = cases_proper_node I (Context.Proof o Proof.context_of) node;
-    fun state_error e node_pr' = (State (node_pr', get_theory node), e);
+    fun make_state node_pr' = State (node_pr', (get_theory node, NONE));
 
-    val (result, err) =
-      node
-      |> Runtime.controlled_execution (SOME context) f
-      |> state_error NONE
-      handle exn => state_error (SOME exn) node_pr;
+    val (st', err) =
+      (Runtime.controlled_execution (SOME context) (f #> make_state #> apply_presentation g) node,
+        NONE) handle exn => (make_state node_pr, SOME exn);
   in
     (case err of
-      NONE => tap g result
-    | SOME exn => raise FAILURE (result, exn))
+      NONE => st'
+    | SOME exn => raise FAILURE (st', exn))
   end;
 
 fun apply_tr int trans state =
   (case (trans, node_of state) of
     (Init f, Toplevel) =>
       Runtime.controlled_execution NONE (fn () =>
-        State (node_presentation (Theory (Context.Theory (f ()))), NONE)) ()
+        State (node_presentation (Theory (Context.Theory (f ()))), (NONE, NONE))) ()
   | (Exit, node as Theory (Context.Theory thy)) =>
       let
         val State ((node', pr_ctxt), _) =
@@ -315,11 +317,15 @@
             (fn _ =>
               node_presentation
                 (Theory (Context.Theory (tap Thm.expose_theory (Theory.end_theory thy)))))
-            (K ());
-      in State ((Toplevel, pr_ctxt), get_theory node') end
+            no_presentation;
+      in State ((Toplevel, pr_ctxt), (get_theory node', NONE)) end
   | (Keep f, node) =>
       Runtime.controlled_execution (try generic_theory_of state)
-        (fn () => (f int state; State (node_presentation node, previous_theory_of state))) ()
+        (fn () =>
+          let
+            val prev_thy = previous_theory_of state;
+            val state' = State (node_presentation node, (prev_thy, NONE));
+          in apply_presentation (fn st => f int st) state' end) ()
   | (Transaction _, Toplevel) => raise UNDEF
   | (Transaction (f, g), node) => apply (fn x => f int x) g (set_prev_theory state node)
   | _ => raise UNDEF);

--- a/src/Pure/Thy/document_output.ML	Tue Nov 23 12:29:09 2021 +0100
+++ b/src/Pure/Thy/document_output.ML	Tue Nov 23 16:06:09 2021 +0100
@@ -207,9 +207,8 @@
 datatype token =
     Ignore
   | Token of Token.T
-  | Heading of Markup.T * Input.source
-  | Body of Markup.T * Input.source
-  | Raw of Input.source;
+  | Markup of Markup.T * Latex.text
+  | Raw of Latex.text;
 
 fun token_with pred (Token tok) = pred tok
   | token_with _ _ = false;
@@ -223,16 +222,14 @@
   (case tok of
     Ignore => []
   | Token tok => output_token ctxt tok
-  | Heading (markup, source) => [XML.Elem (markup, output_document ctxt {markdown = false} source)]
-  | Body (markup, source) => [XML.Elem (markup, output_document ctxt {markdown = true} source)]
-  | Raw source =>
-      Latex.string "%\n" @ output_document ctxt {markdown = true} source @ Latex.string "\n");
+  | Markup (markup, output) => [XML.Elem (markup, output)]
+  | Raw output => Latex.enclose_text "%\n" "\n" output);
 
 fun mk_heading (kind, pos) source =
-  Heading (Markup.latex_heading kind |> Position.markup pos, source);
+  Markup (Markup.latex_heading kind |> Position.markup pos, source);
 
 fun mk_body (kind, pos) source =
-  Body (Markup.latex_body kind |> Position.markup pos, source);
+  Markup (Markup.latex_body kind |> Position.markup pos, source);
 
 
 (* command spans *)
@@ -374,8 +371,30 @@
 
 (* present_thy *)
 
+type segment =
+  {span: Command_Span.span, command: Toplevel.transition,
+   prev_state: Toplevel.state, state: Toplevel.state};
+
 local
 
+fun command_output output tok =
+  if Token.is_command tok then SOME (Token.put_output output tok) else NONE;
+
+fun segment_content (segment: segment) =
+  let val toks = Command_Span.content (#span segment) in
+    (case Toplevel.output_of (#state segment) of
+      NONE => toks
+    | SOME output => map_filter (command_output output) toks)
+  end;
+
+fun output_command is_kind =
+  Scan.some (fn tok =>
+    let val kind = Token.content_of tok in
+      if Token.is_command tok andalso is_kind kind andalso is_some (Token.get_output tok)
+      then SOME ((kind, Token.pos_of tok), the (Token.get_output tok))
+      else NONE
+    end);
+
 val markup_true = "\\isamarkuptrue%\n";
 val markup_false = "\\isamarkupfalse%\n";
 
@@ -395,10 +414,6 @@
 
 in
 
-type segment =
-  {span: Command_Span.span, command: Toplevel.transition,
-   prev_state: Toplevel.state, state: Toplevel.state};
-
 fun present_thy options thy (segments: segment list) =
   let
     val keywords = Thy_Header.get_keywords thy;
@@ -410,16 +425,8 @@
       >> (fn d => (NONE, (Ignore, ("", d))));
 
     fun markup pred mk flag = Scan.peek (fn d =>
-      Document_Source.improper |--
-        Scan.one (fn tok => Token.is_command tok andalso pred keywords (Token.content_of tok)) --
-      (Document_Source.annotation |--
-        Parse.!!!! ((Document_Source.improper -- locale -- Document_Source.improper) |--
-          Parse.document_source --| Document_Source.improper_end))
-            >> (fn (tok, source) =>
-              let
-                val kind = Token.content_of tok;
-                val pos' = Token.pos_of tok;
-              in (SOME (kind, pos'), (mk (kind, pos') source, (flag, d))) end));
+      Document_Source.improper |-- output_command (pred keywords) --| Document_Source.improper_end
+        >> (fn (kind, body) => (SOME kind, (mk kind body, (flag, d)))));
 
     val command = Scan.peek (fn d =>
       Scan.optional (Scan.one Token.is_command_modifier ::: Document_Source.improper) [] --
@@ -468,7 +475,7 @@
           make_span (the cmd) (toks1 @ (tok2 :: (toks3 @ the_default [] tok4))));
 
     val spans = segments
-      |> maps (Command_Span.content o #span)
+      |> maps segment_content
       |> drop_suffix Token.is_space
       |> Source.of_list
       |> Source.source' 0 Token.stopper (Scan.error (Scan.bulk tokens >> flat))