# HG changeset patch
# User aspinall
# Date 1111755882 -3600
# Node ID a8f71893950066880e6f8ee567c448ae22721e01
# Parent  43f1669cbae32912f0959cc115b6bb3497bf9a4c
Support new PGIP commands redostep, redoitem

diff -r 43f1669cbae3 -r a8f718939500 src/Pure/proof_general.ML
--- a/src/Pure/proof_general.ML	Fri Mar 25 13:03:47 2005 +0100
+++ b/src/Pure/proof_general.ML	Fri Mar 25 14:04:42 2005 +0100
@@ -1174,6 +1174,7 @@
      (* improperproofcmd: improper commands which *do not* belong in script *)
      | "dostep"         => isarscript data
      | "undostep"       => isarcmd "undos_proof 1"
+     | "redostep"       => isarcmd "redo"
      | "abortgoal"      => isarcmd "ProofGeneral.kill_proof"  
      | "forget"         => error "Not implemented" 
      | "restoregoal"    => error "Not implemented"  (* could just treat as forget? *)
@@ -1198,6 +1199,7 @@
      (* improperfilecmd: theory-level commands not in script *)
      | "doitem"         => isarscript data
      | "undoitem"       => isarcmd "ProofGeneral.undo"
+     | "redoitem"       => isarcmd "ProofGeneral.redo"
      | "aborttheory"    => isarcmd ("init_toplevel")
      | "retracttheory"  => isarcmd ("kill_thy " ^ (quote (thyname_attr attrs)))
      | "loadfile"       => use_thy_or_ml_file (fileurl_of attrs)
@@ -1289,6 +1291,10 @@
   OuterSyntax.improper_command "ProofGeneral.undo" "(internal)" K.control
     (Scan.succeed (Toplevel.no_timing o IsarCmd.undo));
 
+val redoP = (* redo without output *)
+  OuterSyntax.improper_command "ProofGeneral.redo" "(internal)" K.control
+    (Scan.succeed (Toplevel.no_timing o IsarCmd.redo));
+
 val context_thy_onlyP =
   OuterSyntax.improper_command "ProofGeneral.context_thy_only" "(internal)" K.control
     (P.name >> (Toplevel.no_timing oo IsarThy.init_context update_thy_only));
@@ -1324,7 +1330,7 @@
       (fn txt => Toplevel.imperative (fn () => process_pgip txt))));
 
 fun init_outer_syntax () = OuterSyntax.add_parsers
- [undoP, restartP, kill_proofP, context_thy_onlyP, try_context_thy_onlyP,
+ [undoP, redoP, restartP, kill_proofP, context_thy_onlyP, try_context_thy_onlyP,
   inform_file_processedP, inform_file_retractedP, process_pgipP];
 
 end;