tuned signature: more explicit types for presentation;

--- a/src/Pure/Isar/toplevel.ML	Mon Nov 22 23:08:57 2021 +0100
+++ b/src/Pure/Isar/toplevel.ML	Tue Nov 23 12:04:01 2021 +0100
@@ -30,6 +30,7 @@
   val pretty_state: state -> Pretty.T list
   val string_of_state: state -> string
   val pretty_abstract: state -> Pretty.T
+  type presentation = state -> Latex.text option
   type transition
   val empty: transition
   val name_of: transition -> string
@@ -44,6 +45,7 @@
   val is_init: transition -> bool
   val modify_init: (unit -> theory) -> transition -> transition
   val exit: transition -> transition
+  val present: (state -> Latex.text) -> transition -> transition
   val keep: (state -> unit) -> transition -> transition
   val keep': (bool -> state -> unit) -> transition -> transition
   val keep_proof: (state -> unit) -> transition -> transition
@@ -62,7 +64,7 @@
     (bool -> local_theory -> local_theory) -> transition -> transition
   val local_theory: (bool * Position.T) option -> (xstring * Position.T) option ->
     (local_theory -> local_theory) -> transition -> transition
-  val present_local_theory: (xstring * Position.T) option -> (state -> unit) ->
+  val present_local_theory: (xstring * Position.T) option -> (state -> Latex.text) ->
     transition -> transition
   val local_theory_to_proof': (bool * Position.T) option -> (xstring * Position.T) option ->
     (bool -> local_theory -> Proof.state) -> transition -> transition
@@ -261,6 +263,13 @@
 
 (** toplevel transitions **)
 
+(* presentation *)
+
+type presentation = state -> Latex.text option;
+val no_presentation: presentation = K NONE;
+fun presentation g : presentation = SOME o g;
+
+
 (* primitive transitions *)
 
 datatype trans =
@@ -269,9 +278,9 @@
   (*formal exit of theory*)
   Exit |
   (*peek at state*)
-  Keep of bool -> state -> unit |
+  Keep of bool -> presentation |
   (*node transaction and presentation*)
-  Transaction of (bool -> node -> node_presentation) * (state -> unit);
+  Transaction of (bool -> node -> node_presentation) * presentation;
 
 local
 
@@ -403,13 +412,14 @@
 fun modify_init f tr = if is_init tr then init_theory f (reset_trans tr) else tr;
 
 val exit = add_trans Exit;
-val keep' = add_trans o Keep;
 
 fun present_transaction f g = add_trans (Transaction (f, g));
-fun transaction f = present_transaction f (K ());
-fun transaction0 f = present_transaction (node_presentation oo f) (K ());
+fun transaction f = present_transaction f no_presentation;
+fun transaction0 f = present_transaction (node_presentation oo f) no_presentation;
 
-fun keep f = add_trans (Keep (fn _ => f));
+fun present f = add_trans (Keep (K (presentation f)));
+fun keep f = add_trans (Keep (fn _ => fn st => let val () = f st in NONE end));
+fun keep' f = add_trans (Keep (fn int => fn st => let val () = f int st in NONE end));
 
 fun keep_proof f =
   keep (fn st =>
@@ -495,15 +505,16 @@
             |> Local_Theory.reset_group;
         in (Theory (finish lthy'), lthy') end
     | _ => raise UNDEF))
-  (K ());
+  no_presentation;
 
 fun local_theory restricted target f = local_theory' restricted target (K f);
 
-fun present_local_theory target = present_transaction (fn _ =>
+fun present_local_theory target g = present_transaction (fn _ =>
   (fn Theory gthy =>
         let val (finish, lthy) = Target_Context.switch_named_cmd target gthy;
         in (Theory (finish lthy), lthy) end
-    | _ => raise UNDEF));
+    | _ => raise UNDEF))
+  (presentation g);
 
 
 (* proof transitions *)

--- a/src/Pure/pure_syn.ML	Mon Nov 22 23:08:57 2021 +0100
+++ b/src/Pure/pure_syn.ML	Tue Nov 23 12:04:01 2021 +0100
@@ -24,13 +24,13 @@
   in Document_Output.output_document ctxt markdown txt end;
 
 fun document_command markdown (loc, txt) =
-  Toplevel.keep (fn state =>
+  Toplevel.present (fn state =>
     (case loc of
-      NONE => ignore (output_document state markdown txt)
+      NONE => 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 (output_document state markdown txt));
+    output_document state markdown txt);
 
 val _ =
   Outer_Syntax.command ("chapter", \<^here>) "chapter heading"