# HG changeset patch
# User wenzelm
# Date 1640121070 -3600
# Node ID 77a96ed74340d5685ecab27ead848b4e959b5398
# Parent  29dfe75c058be5b2283ebcf2bc081b5b3de2425f
allow general command transactions with presentation;

diff -r 29dfe75c058b -r 77a96ed74340 src/Pure/Isar/outer_syntax.ML
--- a/src/Pure/Isar/outer_syntax.ML	Tue Dec 21 21:27:26 2021 +0100
+++ b/src/Pure/Isar/outer_syntax.ML	Tue Dec 21 22:11:10 2021 +0100
@@ -162,7 +162,9 @@
     (Restricted_Parser (fn restricted =>
       Parse.opt_target -- parse >> (fn (target, f) => trans restricted target f)));
 
-val local_theory' = local_theory_command Toplevel.local_theory';
+val local_theory' =
+  local_theory_command
+    (fn a => fn b => fn c => Toplevel.local_theory' a b c Toplevel.no_presentation);
 val local_theory = local_theory_command Toplevel.local_theory;
 val local_theory_to_proof' = local_theory_command Toplevel.local_theory_to_proof';
 val local_theory_to_proof = local_theory_command Toplevel.local_theory_to_proof;
diff -r 29dfe75c058b -r 77a96ed74340 src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Tue Dec 21 21:27:26 2021 +0100
+++ b/src/Pure/Isar/toplevel.ML	Tue Dec 21 22:11:10 2021 +0100
@@ -32,6 +32,8 @@
   val string_of_state: state -> string
   val pretty_abstract: state -> Pretty.T
   type presentation = state -> Latex.text option
+  val presentation: (state -> Latex.text) -> presentation
+  val no_presentation: presentation
   type transition
   val empty: transition
   val name_of: transition -> string
@@ -55,14 +57,14 @@
   val ignored: Position.T -> transition
   val malformed: Position.T -> string -> transition
   val generic_theory: (generic_theory -> generic_theory) -> transition -> transition
-  val theory': (bool -> theory -> theory) -> transition -> transition
+  val theory': (bool -> theory -> theory) -> presentation -> transition -> transition
   val theory: (theory -> theory) -> transition -> transition
   val begin_main_target: bool -> (theory -> local_theory) -> transition -> transition
   val end_main_target: transition -> transition
   val begin_nested_target: (Context.generic -> local_theory) -> transition -> transition
   val end_nested_target: transition -> transition
   val local_theory': (bool * Position.T) option -> (xstring * Position.T) option ->
-    (bool -> local_theory -> local_theory) -> transition -> transition
+    (bool -> local_theory -> local_theory) -> presentation -> 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 -> Latex.text) ->
@@ -267,8 +269,8 @@
 (* presentation *)
 
 type presentation = state -> Latex.text option;
+fun presentation g : presentation = SOME o g;
 val no_presentation: presentation = K NONE;
-fun presentation g : presentation = SOME o g;
 
 
 (* primitive transitions *)
@@ -452,7 +454,7 @@
   (fn Theory gthy => node_presentation (Theory (f gthy))
     | _ => raise UNDEF));
 
-fun theory' f = transaction (fn int =>
+fun theory' f = present_transaction (fn int =>
   (fn Theory (Context.Theory thy) =>
       let val thy' = thy
         |> Sign.new_group
@@ -461,7 +463,7 @@
       in node_presentation (Theory (Context.Theory thy')) end
     | _ => raise UNDEF));
 
-fun theory f = theory' (K f);
+fun theory f = theory' (K f) no_presentation;
 
 fun begin_main_target begin f = transaction (fn _ =>
   (fn Theory (Context.Theory thy) =>
@@ -510,10 +512,10 @@
             |> f int
             |> Local_Theory.reset_group;
         in (Theory (finish lthy'), lthy') end
-    | _ => raise UNDEF))
-  no_presentation;
+    | _ => raise UNDEF));
 
-fun local_theory restricted target f = local_theory' restricted target (K f);
+fun local_theory restricted target f =
+  local_theory' restricted target (K f) no_presentation;
 
 fun present_local_theory target g = present_transaction (fn _ =>
   (fn Theory gthy =>