# HG changeset patch
# User wenzelm
# Date 927280002 -7200
# Node ID 169e5b07ec06fa6050a7d4e2954decfc22929247
# Parent  f33c89103fb4153c44d3a6e56a9fe8910e351da3
tuned;
added prompt_state_fn hook;
added kill operation;
provide toplevel node history, nests with proof history;
toplevel prompt includes nest level;
more robust recovery from stale signatures;

diff -r f33c89103fb4 -r 169e5b07ec06 src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Fri May 21 11:43:34 1999 +0200
+++ b/src/Pure/Isar/toplevel.ML	Fri May 21 11:46:42 1999 +0200
@@ -9,11 +9,14 @@
 sig
   datatype node = Theory of theory | Proof of ProofHistory.T
   type state
-  exception UNDEF
   val toplevel: state
+  val prompt_state_default: state -> string
+  val prompt_state_fn: (state -> string) ref
   val print_state_default: state -> unit
   val print_state_fn: (state -> unit) ref
   val print_state: state -> unit
+  exception UNDEF
+  val node_history_of: state -> node History.T
   val node_of: state -> node
   val node_case: (theory -> 'a) -> (Proof.state -> 'a) -> state -> 'a
   val theory_of: state -> theory
@@ -23,24 +26,29 @@
   exception TERMINATE
   exception RESTART
   exception BREAK of state
+  val undo_limit: bool -> int option
   val empty: transition
   val name: string -> transition -> transition
   val position: Position.T -> transition -> transition
   val interactive: bool -> transition -> transition
   val print: transition -> transition
   val reset: transition -> transition
-  val init: (state -> node) -> (node -> unit) -> transition -> transition
+  val init: (state -> node) -> (node -> unit) -> (node -> unit) -> transition -> transition
+  val exit: transition -> transition
+  val kill: transition -> transition
   val keep: (state -> unit) -> transition -> transition
-  val exit: transition -> transition
+  val history: (node History.T -> node History.T) -> transition -> transition
   val imperative: (unit -> unit) -> transition -> transition
-  val init_theory: (unit -> theory) -> (theory -> unit) -> transition -> transition
+  val init_theory: (unit -> theory) -> (theory -> unit) -> (theory -> unit)
+    -> transition -> transition
   val theory: (theory -> theory) -> transition -> transition
+  val theory_to_proof: (bool -> theory -> ProofHistory.T) -> transition -> transition
   val proof: (ProofHistory.T -> ProofHistory.T) -> transition -> transition
-  val theory_to_proof: (theory -> ProofHistory.T) -> transition -> transition
+  val proof': (bool -> ProofHistory.T -> ProofHistory.T) -> transition -> transition
   val proof_to_theory: (ProofHistory.T -> theory) -> transition -> transition
-  type isar
   val trace: bool ref
   val exn_message: exn -> string
+  type isar
   val apply: bool -> transition -> state -> (state * (exn * string) option) option
   val excursion: transition list -> unit
   val set_state: state -> unit
@@ -50,7 +58,7 @@
   val loop: isar -> unit
 end;
 
-structure Toplevel: TOPLEVEL =
+structure Toplevel(*: TOPLEVEL *)=
 struct
 
 
@@ -62,6 +70,9 @@
   Theory of theory |
   Proof of ProofHistory.T;
 
+fun str_of_node (Theory _) = "in theory mode"
+  | str_of_node (Proof _) = "in proof mode";
+
 fun print_node (Theory thy) = Pretty.writeln (Pretty.block
       [Pretty.str "Theory:", Pretty.brk 1, Pretty.str (PureThy.get_name thy),
         Pretty.str " =", Pretty.brk 1, Display.pretty_theory thy])
@@ -72,24 +83,29 @@
 
 (* datatype state *)
 
-datatype state = State of (node * (node -> unit)) list;
-
-exception UNDEF;
+datatype state = State of (node History.T * ((node -> unit) * (node -> unit))) list;
 
 val toplevel = State [];
 fun append_states (State ns) (State ms) = State (ns @ ms);
 
 fun str_of_state (State []) = "at top level"
-  | str_of_state (State ((Theory _, _) :: _)) = "in theory mode"
-  | str_of_state (State ((Proof _, _) :: _)) = "in proof mode";
+  | str_of_state (State ((node, _) :: _)) = str_of_node (History.current node);
+
+
+(* prompt_state hook *)
+
+fun prompt_state_default (State nodes) =
+  let val len = length nodes
+  in (if len < 2 then "" else string_of_int len) ^ Source.default_prompt end;
+
+val prompt_state_fn = ref prompt_state_default;
+fun prompt_state state = ! prompt_state_fn state;
 
 
 (* print_state hook *)
 
 fun print_topnode (State []) = ()
-  | print_topnode (State [(node, _)]) = print_node node
-  | print_topnode (State ((node, _) :: nodes)) =
-      (writeln ("Stack size: " ^ string_of_int (length nodes)); print_node node);
+  | print_topnode (State ((node, _) :: _)) = print_node (History.current node);
 
 fun print_state_default state =
   let val ref (begin_state, end_state, _) = Goals.current_goals_markers in
@@ -104,8 +120,12 @@
 
 (* top node *)
 
-fun node_of (State []) = raise UNDEF
-  | node_of (State ((node, _) :: _)) = node;
+exception UNDEF;
+
+fun node_history_of (State []) = raise UNDEF
+  | node_history_of (State ((node, _) :: _)) = node;
+
+val node_of = History.current o node_history_of;
 
 fun node_case f g state =
   (case node_of state of
@@ -116,13 +136,6 @@
 val sign_of = Theory.sign_of o theory_of;
 val proof_of = node_case (fn _ => raise UNDEF) I;
 
-fun is_stale state =
-  Sign.is_stale (node_case Theory.sign_of Proof.sign_of state) handle UNDEF => false;
-
-fun backup (State ((Theory thy, exit) :: nodes)) =
-      State ((Theory (PureThy.backup thy), exit) :: nodes)
-  | backup state = state;
-
 
 
 (** toplevel transitions **)
@@ -131,28 +144,97 @@
 exception RESTART;
 exception BREAK of state;
 exception FAIL of exn * string;
+exception ROLLBACK of state * exn option;
+exception FAILURE of state * exn;
 
 
-(* datatype trans *)
+(* recovery from stale signatures *)
+
+local
+
+fun is_stale state = Sign.is_stale (sign_of state) handle UNDEF => false;
+
+fun checkpoint_node true (Theory thy) = Theory (PureThy.checkpoint thy)
+  | checkpoint_node _ node = node;
+
+fun copy_node true (Theory thy) = Theory (Theory.copy thy)
+  | copy_node _ node = node;
+
+in
+
+fun node_trans _ _ _ (State []) = raise UNDEF
+  | node_trans int hist f (State ((node, term) :: nodes)) =
+      let
+        fun mk_state nd = State ((nd, term) :: nodes);
+
+        val cont_node = History.map (checkpoint_node int) node;
+        val back_node = History.map (copy_node int) cont_node;
+
+        val trans = if hist then History.apply_copy (copy_node int) else History.map;
+        val (result, opt_exn) = (mk_state (transform_error (trans (f int)) cont_node), None)
+          handle exn => (mk_state cont_node, Some exn);
+      in
+        if is_stale result then raise ROLLBACK (mk_state back_node, opt_exn)
+        else (case opt_exn of None => result | Some exn => raise FAILURE (result, exn))
+      end;
+
+fun check_stale state =
+  if not (is_stale state) then ()
+  else warning "Stale signature encountered!  Should redo current theory from start.";
+
+end;
+
+
+(* primitive transitions *)
+
+(*Important note: recovery from stale signatures is provided only for
+  theory-level operations via MapCurrent and AppCurrent.  Other node
+  or state operations should not touch signatures at all.*)
 
 datatype trans =
-  Reset |
-  Init of (state -> node) * (node -> unit) |
-  Keep of (state -> unit) |
-  Exit |
-  MapCurrent of node -> node;
+  Reset |                                       (*empty toplevel*)
+  Init of (state -> node) * ((node -> unit) * (node -> unit)) |
+    (*push node; provide exit/kill operation*)
+  Exit |                                        (*pop node*)
+  Kill |                                        (*abort node*)
+  Keep of state -> unit |                       (*peek at state*)
+  History of node History.T -> node History.T | (*history operation (undo etc.)*)
+  MapCurrent of bool -> node -> node |          (*change node, bypassing history*)
+  AppCurrent of bool -> node -> node;           (*change node, recording history*)
+
+fun undo_limit int = if int then None else Some 0;
+
+local
 
-fun apply_trans Reset _ = State []
-  | apply_trans (Init (f, g)) (state as State nodes) = State ((f state, g) :: nodes)
-  | apply_trans (Keep f) state = (f state; state)
-  | apply_trans Exit (State []) = raise UNDEF
-  | apply_trans Exit (State ((node, g) :: nodes)) = (g node; State nodes)
-  | apply_trans (MapCurrent _) (State []) = raise UNDEF
-  | apply_trans (MapCurrent f) (State ((node, g) :: nodes)) = State ((f node, g) :: nodes);
+fun apply_tr _ Reset _ = toplevel
+  | apply_tr int (Init (f, term)) (state as State nodes) =
+      State ((History.init (undo_limit int) (f state), term) :: nodes)
+  | apply_tr _ Exit (State []) = raise UNDEF
+  | apply_tr _ Exit (State ((node, (exit, _)):: nodes)) =
+      (exit (History.current node); State nodes)
+  | apply_tr _ Kill (State []) = raise UNDEF
+  | apply_tr _ Kill (State ((node, (_, kill)) :: nodes)) =
+      (kill (History.current node); State nodes)
+  | apply_tr _ (Keep f) state = (f state; state)
+  | apply_tr _ (History _) (State []) = raise UNDEF
+  | apply_tr _ (History f) (State ((node, term) :: nodes)) = State ((f node, term) :: nodes)
+  | apply_tr int (MapCurrent f) state = node_trans int false f state
+  | apply_tr int (AppCurrent f) state = node_trans int true f state;
 
-fun apply_union [] _ = raise UNDEF
-  | apply_union (tr :: trs) state =
-      apply_trans tr state handle UNDEF => apply_union trs state;
+fun apply_union _ [] state = raise FAILURE (state, UNDEF)
+  | apply_union int (tr :: trs) state =
+      transform_error (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 *)
@@ -181,7 +263,7 @@
 fun at_command tr = command_msg "At " tr ^ ".";
 
 fun type_error tr state =
-  error (command_msg "Illegal application of " tr ^ " " ^ str_of_state state);
+  ERROR_MESSAGE (command_msg "Illegal application of " tr ^ " " ^ str_of_state state);
 
 
 (* modify transitions *)
@@ -205,30 +287,27 @@
 (* build transitions *)
 
 val reset = add_trans Reset;
-fun init f g = add_trans (Init (f, g));
+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 exit = add_trans Exit;
+val history = add_trans o History;
 val map_current = add_trans o MapCurrent;
+val app_current = add_trans o AppCurrent;
 
 fun imperative f = keep (fn _ => f ());
 
-fun init_theory f g =
-  init (fn _ => Theory (f ())) (fn Theory thy => g thy | _ => raise UNDEF);
-
-fun theory f = map_current (fn Theory thy => Theory (f thy) | _ => raise UNDEF);
-fun proof f = map_current (fn Proof prf => Proof (f prf) | _ => raise UNDEF);
-
-fun theory_to_proof f = map_current (fn Theory thy => Proof (f thy) | _ => raise UNDEF);
-fun proof_to_theory f = map_current (fn Proof prf => Theory (f prf) | _ => raise UNDEF);
+fun init_theory f exit kill =
+  init (fn _ => Theory (f ()))
+    (fn Theory thy => exit thy | _ => raise UNDEF)
+    (fn Theory thy => kill thy | _ => raise UNDEF);
 
-
-(* the Isar source of transitions *)
-
-type isar =
-  (transition, (transition option,
-    (OuterLex.token, (OuterLex.token,
-      Position.T * (Symbol.symbol, (string, unit) Source.source) Source.source)
-          Source.source) Source.source) Source.source) Source.source;
+fun theory f = app_current (fn _ => (fn Theory thy => Theory (f thy) | _ => raise UNDEF));
+fun theory_to_proof f =
+  app_current (fn int => (fn Theory thy => Proof (f int thy) | _ => raise UNDEF));
+fun proof' f = map_current (fn int => (fn Proof prf => Proof (f int prf) | _ => raise UNDEF));
+val proof = proof' o K;
+fun proof_to_theory f = map_current (fn _ => (fn Proof prf => Theory (f prf) | _ => raise UNDEF));
 
 
 
@@ -269,10 +348,19 @@
   | print_exn (Some (exn, s)) = error_msg (cat_lines [exn_message exn, s]);
 
 
+(* the Isar source of transitions *)
+
+type isar =
+  (transition, (transition option,
+    (OuterLex.token, (OuterLex.token,
+      Position.T * (Symbol.symbol, (string, unit) Source.source) Source.source)
+          Source.source) Source.source) Source.source) Source.source;
+
+
 (* transform interrupt (non-polymorphic) *)
 
 fun transform_interrupt_state f x =
-  let val y = ref (None: state option);
+  let val y = ref (None: (state * exn option) option);
   in exhibit_interrupt (fn () => y := Some (f x)) (); the (! y) end;
 
 fun transform_interrupt_isar f x =
@@ -280,51 +368,34 @@
   in exhibit_interrupt (fn () => y := Some (f x)) (); the (! y) end;
 
 
-(* the dreaded stale signatures *)
-
-fun check_stale state =
-  if not (is_stale state) then ()
-  else warning "Stale signature encountered!  Should redo current theory from start.";
-
-
 (* apply transitions *)
 
 local
 
-fun ap int (tr as Transition {trans, int_only, print, ...}) state =
+fun app int (tr as Transition {trans, int_only, print, ...}) state =
   let
     val _ =
       if int orelse not int_only then ()
       else warning (command_msg "Executing interactive-only " tr);
-    val state' =
-      (if ! trace then (writeln (command_msg "" tr); timeap (apply_union trans) state)
-        else apply_union trans state)
-      handle UNDEF => type_error tr state;
-    val _ = if int andalso print then print_state state' else ();
-  in state' end;
-
-fun app int tr state =
-  let
-    val back_state = backup state;
-    fun rollback st =
-      if not (is_stale st) then st
-      else (warning (command_msg "Rollback after " tr); back_state);
-  in
-    (rollback (transform_interrupt_state (transform_error (ap int tr)) state), None)
-      handle exn => (rollback state, Some exn)
-  end;
+    val (result, opt_exn) =
+      (if ! trace then (writeln (command_msg "" tr); timeap) else I) (apply_trans int trans) state;
+    val _ = if int andalso print then print_state result else ();
+  in (result, apsome (fn UNDEF => type_error tr state | exn => exn) opt_exn) end;
 
 in
 
-fun apply int tr state =
-  (case app int tr state of
-    (state', None) => Some (state', None)
-  | (_, Some TERMINATE) => None
+fun apply int tr st =
+  (case transform_interrupt_state (app int tr) st of
+    (_, Some TERMINATE) => None
   | (_, Some RESTART) => Some (toplevel, None)
   | (state', Some (FAIL (exn_info as (BREAK break_state, _)))) =>
       Some (append_states break_state state', Some exn_info)
   | (state', Some (FAIL exn_info)) => Some (state', Some exn_info)
-  | (state', Some exn) => Some (state', Some (exn, at_command tr)));
+  | (_, Some (ROLLBACK (back_state, opt_exn))) =>
+      (warning (command_msg "Rollback after " tr);
+        Some (back_state, apsome (fn exn => (exn, at_command tr)) opt_exn))
+  | (state', Some exn) => Some (state', Some (exn, at_command tr))
+  | (state', None) => Some (state', None));
 
 end;
 
@@ -355,7 +426,7 @@
 
 (* the global state reference *)
 
-val global_state = ref (State [], None: (exn * string) option);
+val global_state = ref (toplevel, None: (exn * string) option);
 
 fun set_state state = global_state := (state, None);
 fun get_state () = fst (! global_state);
@@ -379,7 +450,7 @@
     handle Interrupt => None;
 
 fun raw_loop src =
-  (case get_interruptible src of
+  (case get_interruptible (Source.set_prompt (prompt_state (get_state ())) src) of
     None => (writeln "\nInterrupt (read)."; raw_loop src)
   | Some None => ()
   | Some (Some (tr, src')) => if >> tr then raw_loop src' else ());