src/Pure/Isar/toplevel.ML

   val timing: bool ref
   val profiling: int ref
   val skip_proofs: bool ref
   exception TERMINATE
   exception RESTART
+  val exn_message: exn -> string
+  val program: (unit -> 'a) -> 'a
   val checkpoint: state -> state
   val copy: state -> state
   type transition
   val undo_limit: bool -> int option
   val empty: transition

   val no_timing: transition -> transition
   val reset: transition -> transition
   val init: (bool -> node) -> (node -> unit) -> (node -> unit) -> transition -> transition
   val exit: transition -> transition
   val kill: transition -> transition
+  val history: (node History.T -> node History.T) -> transition -> transition
   val keep: (state -> unit) -> transition -> transition
   val keep': (bool -> state -> unit) -> transition -> transition
-  val history: (node History.T -> node History.T) -> transition -> transition
   val imperative: (unit -> unit) -> transition -> transition
   val init_theory: (bool -> theory) -> (theory -> unit) -> (theory -> unit)
     -> transition -> transition
   val theory: (theory -> theory) -> transition -> transition
   val theory': (bool -> theory -> theory) -> transition -> transition

   val present_local_theory: xstring option -> (bool -> node -> unit) -> transition -> transition
   val present_proof: (bool -> node -> unit) -> transition -> transition
   val unknown_theory: transition -> transition
   val unknown_proof: transition -> transition
   val unknown_context: transition -> transition
-  val exn_message: exn -> string
   val apply: bool -> transition -> state -> (state * (exn * string) option) option
   val present_excursion: (transition * (state -> state -> 'a -> 'a)) list -> 'a -> 'a
   val excursion: transition list -> unit
-  val program: (unit -> 'a) -> 'a
   val set_state: state -> unit
   val get_state: unit -> state
   val exn: unit -> (exn * string) option
   val >> : transition -> bool
   val >>> : transition list -> unit

 exception TERMINATE;
 exception RESTART;
 exception EXCURSION_FAIL of exn * string;
 exception FAILURE of state * exn;
 
-fun debugging f x =
-  if ! debug then
-    setmp Library.do_transform_failure false
-      exception_trace (fn () => f x)
-  else f x;
-
-
-(* node transactions and recovery from stale theories *)
-
-(*NB: proof commands should be non-destructive!*)
-
-local
-
-fun is_stale state = Context.is_stale (theory_of state) handle UNDEF => false;
-
-val stale_theory = ERROR "Stale theory encountered after succesful execution!";
-
-fun checkpoint_node (Theory (thy, _)) = Theory (Theory.checkpoint thy, NONE)
-  | checkpoint_node node = node;
-
-fun copy_node (Theory (thy, _)) = Theory (Theory.copy thy, NONE)
-  | copy_node node = node;
-
-fun return (result, NONE) = result
-  | return (result, SOME exn) = raise FAILURE (result, exn);
-
-fun interruptible f x =
-  let val y = ref x
-  in raise_interrupt (fn () => y := f x) (); ! y end;
-
-in
-
-fun transaction _ _ (State NONE) = raise UNDEF
-  | transaction hist f (State (SOME (node, term))) =
-      let
-        val cont_node = History.map checkpoint_node node;
-        val back_node = History.map copy_node cont_node;
-        fun state nd = State (SOME (nd, term));
-        fun normal_state nd = (state nd, NONE);
-        fun error_state nd exn = (state nd, SOME exn);
-
-        val (result, err) =
-          cont_node
-          |> (f
-              |> (if hist then History.apply_copy copy_node else History.map)
-              |> debugging
-              |> interruptible
-              |> setmp Output.do_toplevel_errors false)
-          |> normal_state
-          handle exn => error_state cont_node exn;
-      in
-        if is_stale result
-        then return (error_state back_node (the_default stale_theory err))
-        else return (result, err)
-      end;
-
-fun mapping f (State (SOME (node, term))) = State (SOME (History.map f node, term))
-  | mapping _ state = state;
-
-val checkpoint = mapping checkpoint_node;
-val copy = mapping copy_node;
-
-end;
-
-
-(* primitive transitions *)
-
-(*Note: Recovery from stale theories is provided only for theory-level
-  operations via Transaction.  Other node or state operations should
-  not touch theories at all.  Interrupts are enabled only for Keep and
-  Transaction.*)
-
-datatype trans =
-  Reset |                                               (*empty toplevel*)
-  Init of (bool -> node) * ((node -> unit) * (node -> unit)) |
-                                                        (*init node; with exit/kill operation*)
-  Exit |                                                (*conclude node*)
-  Kill |                                                (*abort node*)
-  Keep of bool -> state -> unit |                       (*peek at state*)
-  History of node History.T -> node History.T |         (*history operation (undo etc.)*)
-  Transaction of bool * (bool -> node -> node);         (*node transaction*)
-
-fun undo_limit int = if int then NONE else SOME 0;
-
-local
-
-fun apply_tr _ Reset _ = toplevel
-  | apply_tr int (Init (f, term)) (State NONE) =
-      State (SOME (History.init (undo_limit int) (f int), term))
-  | apply_tr _ (Init _ ) (State (SOME _)) = raise UNDEF
-  | apply_tr _ Exit (State NONE) = raise UNDEF
-  | apply_tr _ Exit (State (SOME (node, (exit, _)))) =
-      (exit (History.current node); State NONE)
-  | apply_tr _ Kill (State NONE) = raise UNDEF
-  | apply_tr _ Kill (State (SOME (node, (_, kill)))) =
-      (kill (History.current node); State NONE)
-  | apply_tr int (Keep f) state =
-      (setmp Output.do_toplevel_errors false (raise_interrupt (f int)) state; state)
-  | apply_tr _ (History _) (State NONE) = raise UNDEF
-  | apply_tr _ (History f) (State (SOME (node, term))) = State (SOME (f node, term))
-  | apply_tr int (Transaction (hist, f)) state = transaction hist (fn x => f int x) state;
-
-fun apply_union _ [] state = raise FAILURE (state, UNDEF)
-  | apply_union int (tr :: trs) state =
-      apply_tr int tr state
-        handle UNDEF => apply_union int trs state
-          | FAILURE (alt_state, UNDEF) => apply_union int trs alt_state
-          | exn as FAILURE _ => raise exn
-          | exn => raise FAILURE (state, exn);
-
-in
-
-fun apply_trans int trs state = (apply_union int trs state, NONE)
-  handle FAILURE (alt_state, exn) => (alt_state, SOME exn) | exn => (state, SOME exn);
-
-end;
-
-
-(* datatype transition *)
-
-datatype transition = Transition of
- {name: string,                        (*command name*)
-  pos: Position.T,                     (*source position*)
-  source: OuterLex.token list option,  (*source text*)
-  int_only: bool,                      (*interactive-only*)
-  print: string list,                  (*print modes (union)*)
-  no_timing: bool,                     (*suppress timing*)
-  trans: trans list};                  (*primitive transitions (union)*)
-
-fun make_transition (name, pos, source, int_only, print, no_timing, trans) =
-  Transition {name = name, pos = pos, source = source,
-    int_only = int_only, print = print, no_timing = no_timing, trans = trans};
-
-fun map_transition f (Transition {name, pos, source, int_only, print, no_timing, trans}) =
-  make_transition (f (name, pos, source, int_only, print, no_timing, trans));
-
-val empty = make_transition ("<unknown>", Position.none, NONE, false, [], false, []);
-
-fun name_of (Transition {name, ...}) = name;
-fun source_of (Transition {source, ...}) = source;
-
-
-(* diagnostics *)
-
-fun str_of_transition (Transition {name, pos, ...}) = quote name ^ Position.str_of pos;
-
-fun command_msg msg tr = msg ^ "command " ^ str_of_transition tr;
-fun at_command tr = command_msg "At " tr ^ ".";
-
-fun type_error tr state =
-  ERROR (command_msg "Illegal application of " tr ^ " " ^ str_of_state state);
-
-
-(* modify transitions *)
-
-fun name nm = map_transition (fn (_, pos, source, int_only, print, no_timing, trans) =>
-  (nm, pos, source, int_only, print, no_timing, trans));
-
-fun position pos = map_transition (fn (name, _, source, int_only, print, no_timing, trans) =>
-  (name, pos, source, int_only, print, no_timing, trans));
-
-fun source src = map_transition (fn (name, pos, _, int_only, print, no_timing, trans) =>
-  (name, pos, SOME src, int_only, print, no_timing, trans));
-
-fun interactive int_only = map_transition (fn (name, pos, source, _, print, no_timing, trans) =>
-  (name, pos, source, int_only, print, no_timing, trans));
-
-val no_timing = map_transition (fn (name, pos, source, int_only, print, _, trans) =>
-  (name, pos, source, int_only, print, true, trans));
-
-fun add_trans tr = map_transition (fn (name, pos, source, int_only, print, no_timing, trans) =>
-  (name, pos, source, int_only, print, no_timing, trans @ [tr]));
-
-fun print' mode = map_transition (fn (name, pos, source, int_only, print, no_timing, trans) =>
-  (name, pos, source, int_only, insert (op =) mode print, no_timing, trans));
-
-val print = print' "";
-
-val three_buffersN = "three_buffers";
-val print3 = print' three_buffersN;
-
-
-(* build transitions *)
-
-val reset = add_trans Reset;
-fun init f exit kill = add_trans (Init (f, (exit, kill)));
-val exit = add_trans Exit;
-val kill = add_trans Kill;
-val keep' = add_trans o Keep;
-val history = add_trans o History;
-fun map_current f = add_trans (Transaction (false, f));
-fun app_current f = add_trans (Transaction (true, f));
-
-fun keep f = add_trans (Keep (fn _ => f));
-fun imperative f = keep (fn _ => f ());
-
-fun init_theory f exit kill =
-  init (fn int => Theory (f int, NONE))
-    (fn Theory (thy, _) => exit thy | _ => raise UNDEF)
-    (fn Theory (thy, _) => kill thy | _ => raise UNDEF);
-
-
-(* typed transitions *)
-
-fun theory f = app_current
-  (K (fn Theory (thy, _) => Theory (f thy, NONE) | _ => raise UNDEF));
-
-fun theory' f = app_current (fn int =>
-  (fn Theory (thy, _) => Theory (f int thy, NONE) | _ => raise UNDEF));
-
-fun theory_context f = app_current
-  (K (fn Theory (thy, _) => Theory (swap (apfst SOME (f thy))) | _ => raise UNDEF));
-
-fun local_theory loc f = theory_context (LocalTheory.mapping loc f);
-
-fun theory_to_proof f = app_current (fn int =>
-  (fn Theory (thy, _) =>
-    let
-      val prf = f thy;
-      val schematic = Proof.schematic_goal prf;
-    in
-      if ! skip_proofs andalso schematic then
-        warning "Cannot skip proof of schematic goal statement"
-      else ();
-      if ! skip_proofs andalso not schematic then
-        SkipProof ((History.init (undo_limit int) 0, #2 (Proof.global_skip_proof int prf)), thy)
-      else Proof (ProofHistory.init (undo_limit int) prf, thy)
-    end
-  | _ => raise UNDEF));
-
-fun proofs' f = map_current (fn int =>
-  (fn Proof (prf, orig_thy) => Proof (ProofHistory.applys (f int) prf, orig_thy)
-    | SkipProof ((h, thy), orig_thy) => SkipProof ((History.apply I h, thy), orig_thy)
-    | _ => raise UNDEF));
-
-fun proof' f = proofs' (Seq.single oo f);
-val proofs = proofs' o K;
-val proof = proof' o K;
-
-fun actual_proof f = map_current (fn _ =>
-  (fn Proof (prf, orig_thy) => Proof (f prf, orig_thy) | _ => raise UNDEF));
-
-fun skip_proof f = map_current (fn _ =>
-  (fn SkipProof ((h, thy), orig_thy) => SkipProof ((f h, thy), orig_thy) | _ => raise UNDEF));
-
-fun end_proof f = map_current (fn int =>
-  (fn Proof (prf, _) => Theory (f int (ProofHistory.current prf))
-    | SkipProof ((h, thy), _) => if History.current h = 0 then Theory (thy, NONE) else raise UNDEF
-    | _ => raise UNDEF));
-
-val forget_proof = map_current (fn _ =>
-  (fn Proof (_, orig_thy) => Theory (orig_thy, NONE)
-    | SkipProof (_, orig_thy) => Theory (orig_thy, NONE)
-    | _ => raise UNDEF));
-
-fun proof_to_theory' f = end_proof (rpair NONE oo f);
-fun proof_to_theory f = proof_to_theory' (K f);
-fun proof_to_theory_context f = end_proof ((swap o apfst SOME) oo f);
-
-fun skip_proof_to_theory p = map_current (fn _ =>
-  (fn SkipProof ((h, thy), _) =>
-    if p (History.current h) then Theory (thy, NONE)
-    else raise UNDEF
-  | _ => raise UNDEF));
-
-fun present_local_theory loc f = app_current (fn int =>
-  (fn Theory (thy, _) => Theory (swap (apfst SOME (LocalTheory.mapping loc I thy)))
-    | _ => raise UNDEF) #> tap (f int));
-
-fun present_proof f = map_current (fn int =>
-  (fn node as Proof _ => node | _ => raise UNDEF) #> tap (f int));
-
-val unknown_theory = imperative (fn () => warning "Unknown theory context");
-val unknown_proof = imperative (fn () => warning "Unknown proof context");
-val unknown_context = imperative (fn () => warning "Unknown context");
-
-
-
-(** toplevel transactions **)
 
 (* print exceptions *)
 
 local
 

   | print_exn (SOME (exn, s)) = Output.error_msg (cat_lines [exn_message exn, s]);
 
 end;
 
 
+(* controlled execution *)
+
+local
+
+fun debugging f x =
+  if ! debug then
+    setmp Library.do_transform_failure false
+      exception_trace (fn () => f x)
+  else f x;
+
+fun interruptible f x =
+  let val y = ref x
+  in raise_interrupt (fn () => y := f x) (); ! y end;
+
+in
+
+fun controlled_execution f =
+  f
+  |> debugging
+  |> interruptible
+  |> setmp Output.do_toplevel_errors false;
+
+fun program f =
+  Output.ML_errors (fn () => debugging f () handle exn => error (exn_message exn)) ();
+
+end;
+
+
+(* node transactions and recovery from stale theories *)
+
+(*NB: proof commands should be non-destructive!*)
+
+local
+
+fun is_stale state = Context.is_stale (theory_of state) handle UNDEF => false;
+
+val stale_theory = ERROR "Stale theory encountered after succesful execution!";
+
+fun checkpoint_node (Theory (thy, _)) = Theory (Theory.checkpoint thy, NONE)
+  | checkpoint_node node = node;
+
+fun copy_node (Theory (thy, _)) = Theory (Theory.copy thy, NONE)
+  | copy_node node = node;
+
+fun return (result, NONE) = result
+  | return (result, SOME exn) = raise FAILURE (result, exn);
+
+in
+
+fun transaction hist f (node, term) =
+  let
+    val cont_node = History.map checkpoint_node node;
+    val back_node = History.map copy_node cont_node;
+    fun state nd = State (SOME (nd, term));
+    fun normal_state nd = (state nd, NONE);
+    fun error_state nd exn = (state nd, SOME exn);
+
+    val (result, err) =
+      cont_node
+      |> (f
+          |> (if hist then History.apply_copy copy_node else History.map)
+          |> controlled_execution)
+      |> normal_state
+      handle exn => error_state cont_node exn;
+  in
+    if is_stale result
+    then return (error_state back_node (the_default stale_theory err))
+    else return (result, err)
+  end;
+
+fun mapping f (State (SOME (node, term))) = State (SOME (History.map f node, term))
+  | mapping _ state = state;
+
+val checkpoint = mapping checkpoint_node;
+val copy = mapping copy_node;
+
+end;
+
+
+(* primitive transitions *)
+
+(*Note: Recovery from stale theories is provided only for theory-level
+  operations via Transaction.  Other node or state operations should
+  not touch theories at all.  Interrupts are enabled only for Keep and
+  Transaction.*)
+
+datatype trans =
+  Reset |                                               (*empty toplevel*)
+  Init of (bool -> node) * ((node -> unit) * (node -> unit)) |
+                                                        (*init node; with exit/kill operation*)
+  Exit |                                                (*conclude node*)
+  Kill |                                                (*abort node*)
+  History of node History.T -> node History.T |         (*history operation (undo etc.)*)
+  Keep of bool -> state -> unit |                       (*peek at state*)
+  Transaction of bool * (bool -> node -> node);         (*node transaction*)
+
+fun undo_limit int = if int then NONE else SOME 0;
+
+local
+
+fun apply_tr _ Reset _ = toplevel
+  | apply_tr int (Init (f, term)) (State NONE) =
+      State (SOME (History.init (undo_limit int) (f int), term))
+  | apply_tr _ (Init _ ) (State (SOME _)) = raise UNDEF
+  | apply_tr _ Exit (State NONE) = raise UNDEF
+  | apply_tr _ Exit (State (SOME (node, (exit, _)))) =
+      (exit (History.current node); State NONE)
+  | apply_tr _ Kill (State NONE) = raise UNDEF
+  | apply_tr _ Kill (State (SOME (node, (_, kill)))) =
+      (kill (History.current node); State NONE)
+  | apply_tr _ (History _) (State NONE) = raise UNDEF
+  | apply_tr _ (History f) (State (SOME (node, term))) = State (SOME (f node, term))
+  | apply_tr int (Keep f) state =
+      controlled_execution (fn x => tap (f int) x) state
+  | apply_tr _ (Transaction _) (State NONE) = raise UNDEF
+  | apply_tr int (Transaction (hist, f)) (State (SOME state)) =
+      transaction hist (fn x => f int x) state;
+
+fun apply_union _ [] state = raise FAILURE (state, UNDEF)
+  | apply_union int (tr :: trs) state =
+      apply_tr int tr state
+        handle UNDEF => apply_union int trs state
+          | FAILURE (alt_state, UNDEF) => apply_union int trs alt_state
+          | exn as FAILURE _ => raise exn
+          | exn => raise FAILURE (state, exn);
+
+in
+
+fun apply_trans int trs state = (apply_union int trs state, NONE)
+  handle FAILURE (alt_state, exn) => (alt_state, SOME exn) | exn => (state, SOME exn);
+
+end;
+
+
+(* datatype transition *)
+
+datatype transition = Transition of
+ {name: string,                        (*command name*)
+  pos: Position.T,                     (*source position*)
+  source: OuterLex.token list option,  (*source text*)
+  int_only: bool,                      (*interactive-only*)
+  print: string list,                  (*print modes (union)*)
+  no_timing: bool,                     (*suppress timing*)
+  trans: trans list};                  (*primitive transitions (union)*)
+
+fun make_transition (name, pos, source, int_only, print, no_timing, trans) =
+  Transition {name = name, pos = pos, source = source,
+    int_only = int_only, print = print, no_timing = no_timing, trans = trans};
+
+fun map_transition f (Transition {name, pos, source, int_only, print, no_timing, trans}) =
+  make_transition (f (name, pos, source, int_only, print, no_timing, trans));
+
+val empty = make_transition ("<unknown>", Position.none, NONE, false, [], false, []);
+
+fun name_of (Transition {name, ...}) = name;
+fun source_of (Transition {source, ...}) = source;
+
+
+(* diagnostics *)
+
+fun str_of_transition (Transition {name, pos, ...}) = quote name ^ Position.str_of pos;
+
+fun command_msg msg tr = msg ^ "command " ^ str_of_transition tr;
+fun at_command tr = command_msg "At " tr ^ ".";
+
+fun type_error tr state =
+  ERROR (command_msg "Illegal application of " tr ^ " " ^ str_of_state state);
+
+
+(* modify transitions *)
+
+fun name nm = map_transition (fn (_, pos, source, int_only, print, no_timing, trans) =>
+  (nm, pos, source, int_only, print, no_timing, trans));
+
+fun position pos = map_transition (fn (name, _, source, int_only, print, no_timing, trans) =>
+  (name, pos, source, int_only, print, no_timing, trans));
+
+fun source src = map_transition (fn (name, pos, _, int_only, print, no_timing, trans) =>
+  (name, pos, SOME src, int_only, print, no_timing, trans));
+
+fun interactive int_only = map_transition (fn (name, pos, source, _, print, no_timing, trans) =>
+  (name, pos, source, int_only, print, no_timing, trans));
+
+val no_timing = map_transition (fn (name, pos, source, int_only, print, _, trans) =>
+  (name, pos, source, int_only, print, true, trans));
+
+fun add_trans tr = map_transition (fn (name, pos, source, int_only, print, no_timing, trans) =>
+  (name, pos, source, int_only, print, no_timing, trans @ [tr]));
+
+fun print' mode = map_transition (fn (name, pos, source, int_only, print, no_timing, trans) =>
+  (name, pos, source, int_only, insert (op =) mode print, no_timing, trans));
+
+val print = print' "";
+
+val three_buffersN = "three_buffers";
+val print3 = print' three_buffersN;
+
+
+(* build transitions *)
+
+val reset = add_trans Reset;
+fun init f exit kill = add_trans (Init (f, (exit, kill)));
+val exit = add_trans Exit;
+val kill = add_trans Kill;
+val history = add_trans o History;
+val keep' = add_trans o Keep;
+fun map_current f = add_trans (Transaction (false, f));
+fun app_current f = add_trans (Transaction (true, f));
+
+fun keep f = add_trans (Keep (fn _ => f));
+fun imperative f = keep (fn _ => f ());
+
+fun init_theory f exit kill =
+  init (fn int => Theory (f int, NONE))
+    (fn Theory (thy, _) => exit thy | _ => raise UNDEF)
+    (fn Theory (thy, _) => kill thy | _ => raise UNDEF);
+
+
+(* typed transitions *)
+
+fun theory f = app_current
+  (K (fn Theory (thy, _) => Theory (f thy, NONE) | _ => raise UNDEF));
+
+fun theory' f = app_current (fn int =>
+  (fn Theory (thy, _) => Theory (f int thy, NONE) | _ => raise UNDEF));
+
+fun theory_context f = app_current
+  (K (fn Theory (thy, _) => Theory (swap (apfst SOME (f thy))) | _ => raise UNDEF));
+
+fun local_theory loc f = theory_context (LocalTheory.mapping loc f);
+
+fun theory_to_proof f = app_current (fn int =>
+  (fn Theory (thy, _) =>
+    let
+      val prf = f thy;
+      val schematic = Proof.schematic_goal prf;
+    in
+      if ! skip_proofs andalso schematic then
+        warning "Cannot skip proof of schematic goal statement"
+      else ();
+      if ! skip_proofs andalso not schematic then
+        SkipProof ((History.init (undo_limit int) 0, #2 (Proof.global_skip_proof int prf)), thy)
+      else Proof (ProofHistory.init (undo_limit int) prf, thy)
+    end
+  | _ => raise UNDEF));
+
+fun proofs' f = map_current (fn int =>
+  (fn Proof (prf, orig_thy) => Proof (ProofHistory.applys (f int) prf, orig_thy)
+    | SkipProof ((h, thy), orig_thy) => SkipProof ((History.apply I h, thy), orig_thy)
+    | _ => raise UNDEF));
+
+fun proof' f = proofs' (Seq.single oo f);
+val proofs = proofs' o K;
+val proof = proof' o K;
+
+fun actual_proof f = map_current (fn _ =>
+  (fn Proof (prf, orig_thy) => Proof (f prf, orig_thy) | _ => raise UNDEF));
+
+fun skip_proof f = map_current (fn _ =>
+  (fn SkipProof ((h, thy), orig_thy) => SkipProof ((f h, thy), orig_thy) | _ => raise UNDEF));
+
+fun end_proof f = map_current (fn int =>
+  (fn Proof (prf, _) => Theory (f int (ProofHistory.current prf))
+    | SkipProof ((h, thy), _) => if History.current h = 0 then Theory (thy, NONE) else raise UNDEF
+    | _ => raise UNDEF));
+
+val forget_proof = map_current (fn _ =>
+  (fn Proof (_, orig_thy) => Theory (orig_thy, NONE)
+    | SkipProof (_, orig_thy) => Theory (orig_thy, NONE)
+    | _ => raise UNDEF));
+
+fun proof_to_theory' f = end_proof (rpair NONE oo f);
+fun proof_to_theory f = proof_to_theory' (K f);
+fun proof_to_theory_context f = end_proof ((swap o apfst SOME) oo f);
+
+fun skip_proof_to_theory p = map_current (fn _ =>
+  (fn SkipProof ((h, thy), _) =>
+    if p (History.current h) then Theory (thy, NONE)
+    else raise UNDEF
+  | _ => raise UNDEF));
+
+fun present_local_theory loc f = app_current (fn int =>
+  (fn Theory (thy, _) => Theory (swap (apfst SOME (LocalTheory.mapping loc I thy)))
+    | _ => raise UNDEF) #> tap (f int));
+
+fun present_proof f = map_current (fn int =>
+  (fn node as Proof _ => node | _ => raise UNDEF) #> tap (f int));
+
+val unknown_theory = imperative (fn () => warning "Unknown theory context");
+val unknown_proof = imperative (fn () => warning "Unknown proof context");
+val unknown_context = imperative (fn () => warning "Unknown context");
+
+
+
+(** toplevel transactions **)
+
 (* apply transitions *)
 
 local
 
 fun app int (tr as Transition {trans, int_only, print, no_timing, ...}) state =

 fun excursion trs = present_excursion (map (rpair no_pr) trs) ();
 
 end;
 
 
-(* toplevel program: independent of state *)
-
-fun program f =
-  Output.ML_errors (fn () => debugging f () handle exn => error (exn_message exn)) ();
-
-
 
 (** interactive transformations **)
 
 (* the global state reference *)