# HG changeset patch
# User wenzelm
# Date 1216027180 -7200
# Node ID 38f26d4079befa8095333d463c668abccb08bf79
# Parent  bcb01eb565eec52d3c3de245afe996314b520a16
removed obsolete 'redo' command;
cannot_undo: global history;
tuned;

diff -r bcb01eb565ee -r 38f26d4079be src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Mon Jul 14 11:19:39 2008 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Mon Jul 14 11:19:40 2008 +0200
@@ -667,8 +667,8 @@
   OuterSyntax.command "proof" "backward proof"
     (K.tag_proof K.prf_block)
     (Scan.option Method.parse >> (fn m => Toplevel.print o
-      Toplevel.actual_proof (ProofHistory.applys (Proof.proof m)) o
-      Toplevel.skip_proof (History.apply (fn i => i + 1))));
+      Toplevel.actual_proof (ProofNode.applys (Proof.proof m)) o
+      Toplevel.skip_proof (fn i => i + 1)));
 
 
 (* calculational proof commands *)
@@ -702,18 +702,7 @@
 val _ =
   OuterSyntax.command "back" "backtracking of proof command"
     (K.tag_proof K.prf_script)
-    (Scan.succeed (Toplevel.print o IsarCmd.back));
-
-
-(* history *)
-
-val _ =
-  OuterSyntax.improper_command "cannot_undo" "report 'cannot undo' error message" K.control
-    (P.name >> (Toplevel.no_timing oo IsarCmd.cannot_undo));
-
-val _ =
-  OuterSyntax.improper_command "redo" "redo last command" K.control
-    (Scan.succeed (Toplevel.no_timing o Toplevel.print o IsarCmd.redo));
+    (Scan.succeed (Toplevel.print o Toplevel.actual_proof ProofNode.back o Toplevel.skip_proof I));
 
 
 (* nested command *)
@@ -725,7 +714,7 @@
         handle ERROR msg => Scan.fail_with (K msg)));
 
 
-(* global Isar state commands *)
+(* global history commands *)
 
 val _ =
   OuterSyntax.improper_command "init_toplevel" "init toplevel point-of-interest" K.control
@@ -748,6 +737,12 @@
         if Toplevel.is_proof state then (Isar.undo n; Isar.print ()) else raise Toplevel.UNDEF)));
 
 val _ =
+  OuterSyntax.improper_command "cannot_undo" "partial undo -- Proof General legacy" K.control
+    (P.name >>
+      (fn "end" => Toplevel.no_timing o Toplevel.imperative (fn () => Isar.undo 1)
+        | txt => Toplevel.imperative (fn () => error ("Cannot undo " ^ quote txt))));
+
+val _ =
   OuterSyntax.improper_command "kill" "kill partial proof or theory development" K.control
     (Scan.succeed (Toplevel.no_timing o Toplevel.imperative Isar.kill));