improved undo / kill operations;

--- a/src/Pure/Isar/isar_cmd.ML	Thu May 27 11:39:44 1999 +0200
+++ b/src/Pure/Isar/isar_cmd.ML	Thu May 27 20:45:20 1999 +0200
@@ -13,9 +13,12 @@
   val quit: Toplevel.transition -> Toplevel.transition
   val cannot_undo: string -> Toplevel.transition -> Toplevel.transition
   val clear_undo: Toplevel.transition -> Toplevel.transition
+  val redo: Toplevel.transition -> Toplevel.transition
+  val undos_proof: int -> Toplevel.transition -> Toplevel.transition
+  val kill_proof: Toplevel.transition -> Toplevel.transition
+  val undo_theory: Toplevel.transition -> Toplevel.transition
+  val kill_theory: Toplevel.transition -> Toplevel.transition
   val undo: Toplevel.transition -> Toplevel.transition
-  val redo: Toplevel.transition -> Toplevel.transition
-  val undos: int -> Toplevel.transition -> Toplevel.transition
   val use: string -> Toplevel.transition -> Toplevel.transition
   val use_mltext_theory: string -> Toplevel.transition -> Toplevel.transition
   val use_mltext: string -> Toplevel.transition -> Toplevel.transition
@@ -58,20 +61,22 @@
 (* history commands *)
 
 fun cannot_undo txt = Toplevel.imperative (fn () => error ("Cannot undo " ^ quote txt));
-
 val clear_undo = Toplevel.history History.clear o Toplevel.proof ProofHistory.clear;
 val redo = Toplevel.history History.redo o Toplevel.proof ProofHistory.redo;
 
-fun undo_proof prf =
-  if ProofHistory.is_initial prf then raise Toplevel.UNDEF else ProofHistory.undo prf;
+fun undos_proof n = Toplevel.proof (fn prf =>
+  if ProofHistory.is_initial prf then raise Toplevel.UNDEF else funpow n ProofHistory.undo prf);
 
-fun undo_node hist =
-  if History.is_initial hist then raise Toplevel.UNDEF else History.undo hist;
+val kill_proof = Toplevel.history (fn hist =>
+  (case History.current hist of
+    Toplevel.Theory _ => raise Toplevel.UNDEF
+  | Toplevel.Proof _ => History.undo hist));
 
-val undo = Toplevel.kill o Toplevel.history undo_node o Toplevel.proof undo_proof;
+val undo_theory = Toplevel.history (fn hist =>
+  if History.is_initial hist then raise Toplevel.UNDEF else History.undo hist);
 
-(* FIXME fix *)
-fun undos n = Toplevel.history (funpow n History.undo) o Toplevel.proof (funpow n undo_proof);
+val kill_theory = Toplevel.imperative (fn () => warning "Nothing to kill.") o Toplevel.kill;
+val undo = kill_theory o undo_theory o undos_proof 1;
 
 
 (* use ML text *)

--- a/src/Pure/Isar/isar_syn.ML	Thu May 27 11:39:44 1999 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Thu May 27 20:45:20 1999 +0200
@@ -29,7 +29,7 @@
 
 val kill_excursionP =
   OuterSyntax.command "kill" "kill current excursion" K.control
-    (Scan.succeed (Toplevel.print o Toplevel.kill));
+    (Scan.succeed (Toplevel.print o IsarCmd.kill_theory));
 
 val contextP =
   OuterSyntax.improper_command "context" "switch theory context" K.thy_begin
@@ -320,10 +320,6 @@
 
 (* end proof *)
 
-val kill_proofP =
-  OuterSyntax.improper_command "kill_proof" "abort current proof" K.control
-    (Scan.succeed (Toplevel.print o Toplevel.proof_to_theory IsarThy.kill_proof));
-
 val qed_withP =
   OuterSyntax.improper_command "qed_with" "conclude proof, may patch name and attributes"
     K.qed_block
@@ -363,27 +359,7 @@
       >> (Toplevel.print oo (Toplevel.proof o IsarThy.proof)));
 
 
-(* proof history *)
-
-val cannot_undoP =
-  OuterSyntax.improper_command "cannot_undo" "report 'cannot undo' error message" K.control
-    (P.name >> (Toplevel.print oo IsarCmd.cannot_undo));
-
-val clear_undoP =
-  OuterSyntax.improper_command "clear_undo" "clear undo information" K.control
-    (Scan.succeed (Toplevel.print o IsarCmd.clear_undo));
-
-val undoP =
-  OuterSyntax.improper_command "undo" "undo last command" K.control
-    (Scan.succeed (Toplevel.print o IsarCmd.undo));
-
-val redoP =
-  OuterSyntax.improper_command "redo" "redo last command" K.control
-    (Scan.succeed (Toplevel.print o IsarCmd.redo));
-
-val undosP =
-  OuterSyntax.improper_command "undos" "undo last commands" K.control
-    (P.nat >> (fn n => Toplevel.print o IsarCmd.undos n));
+(* proof navigation *)
 
 val backP =
   OuterSyntax.improper_command "back" "backtracking of proof command" K.prf_script
@@ -402,6 +378,33 @@
     (Scan.succeed (Toplevel.print o Toplevel.proof ProofHistory.top));
 
 
+(* history *)
+
+val cannot_undoP =
+  OuterSyntax.improper_command "cannot_undo" "report 'cannot undo' error message" K.control
+    (P.name >> (Toplevel.print oo IsarCmd.cannot_undo));
+
+val clear_undoP =
+  OuterSyntax.improper_command "clear_undo" "clear undo information" K.control
+    (Scan.succeed (Toplevel.print o IsarCmd.clear_undo));
+
+val redoP =
+  OuterSyntax.improper_command "redo" "redo last command" K.control
+    (Scan.succeed (Toplevel.print o IsarCmd.redo));
+
+val undos_proofP =
+  OuterSyntax.improper_command "undos_proof" "undo last proof commands" K.control
+    (P.nat >> (Toplevel.print oo IsarCmd.undos_proof));
+
+val kill_proofP =
+  OuterSyntax.improper_command "kill_proof" "undo current proof" K.control
+    (Scan.succeed (Toplevel.print o IsarCmd.kill_proof));
+
+val undoP =
+  OuterSyntax.improper_command "undo" "undo last command" K.control
+    (Scan.succeed (Toplevel.print o IsarCmd.undo));
+
+
 
 (** diagnostic commands (for interactive mode only) **)
 
@@ -528,10 +531,10 @@
   print_ast_translationP, token_translationP, oracleP,
   (*proof commands*)
   theoremP, lemmaP, showP, haveP, thusP, henceP, assumeP, fixP, letP,
-  thenP, fromP, factsP, beginP, endP, nextP, kill_proofP, qed_withP,
-  qedP, terminal_proofP, immediate_proofP, default_proofP, refineP,
-  then_refineP, proofP, cannot_undoP, clear_undoP, undoP, redoP,
-  undosP, backP, prevP, upP, topP,
+  thenP, fromP, factsP, beginP, endP, nextP, qed_withP, qedP,
+  terminal_proofP, immediate_proofP, default_proofP, refineP,
+  then_refineP, proofP, backP, prevP, upP, topP, cannot_undoP,
+  clear_undoP, redoP, undos_proofP, kill_proofP, undoP,
   (*diagnostic commands*)
   print_commandsP, print_theoryP, print_syntaxP, print_attributesP,
   print_methodsP, print_theoremsP, print_bindsP, print_lthmsP,