Support new PGIP commands redostep, redoitem
authoraspinall
Fri Mar 25 14:04:42 2005 +0100 (2005-03-25)
changeset 15626a8f718939500
parent 15625 43f1669cbae3
child 15627 7a108ae4c798
Support new PGIP commands redostep, redoitem
src/Pure/proof_general.ML
     1.1 --- a/src/Pure/proof_general.ML	Fri Mar 25 13:03:47 2005 +0100
     1.2 +++ b/src/Pure/proof_general.ML	Fri Mar 25 14:04:42 2005 +0100
     1.3 @@ -1174,6 +1174,7 @@
     1.4       (* improperproofcmd: improper commands which *do not* belong in script *)
     1.5       | "dostep"         => isarscript data
     1.6       | "undostep"       => isarcmd "undos_proof 1"
     1.7 +     | "redostep"       => isarcmd "redo"
     1.8       | "abortgoal"      => isarcmd "ProofGeneral.kill_proof"  
     1.9       | "forget"         => error "Not implemented" 
    1.10       | "restoregoal"    => error "Not implemented"  (* could just treat as forget? *)
    1.11 @@ -1198,6 +1199,7 @@
    1.12       (* improperfilecmd: theory-level commands not in script *)
    1.13       | "doitem"         => isarscript data
    1.14       | "undoitem"       => isarcmd "ProofGeneral.undo"
    1.15 +     | "redoitem"       => isarcmd "ProofGeneral.redo"
    1.16       | "aborttheory"    => isarcmd ("init_toplevel")
    1.17       | "retracttheory"  => isarcmd ("kill_thy " ^ (quote (thyname_attr attrs)))
    1.18       | "loadfile"       => use_thy_or_ml_file (fileurl_of attrs)
    1.19 @@ -1289,6 +1291,10 @@
    1.20    OuterSyntax.improper_command "ProofGeneral.undo" "(internal)" K.control
    1.21      (Scan.succeed (Toplevel.no_timing o IsarCmd.undo));
    1.22  
    1.23 +val redoP = (* redo without output *)
    1.24 +  OuterSyntax.improper_command "ProofGeneral.redo" "(internal)" K.control
    1.25 +    (Scan.succeed (Toplevel.no_timing o IsarCmd.redo));
    1.26 +
    1.27  val context_thy_onlyP =
    1.28    OuterSyntax.improper_command "ProofGeneral.context_thy_only" "(internal)" K.control
    1.29      (P.name >> (Toplevel.no_timing oo IsarThy.init_context update_thy_only));
    1.30 @@ -1324,7 +1330,7 @@
    1.31        (fn txt => Toplevel.imperative (fn () => process_pgip txt))));
    1.32  
    1.33  fun init_outer_syntax () = OuterSyntax.add_parsers
    1.34 - [undoP, restartP, kill_proofP, context_thy_onlyP, try_context_thy_onlyP,
    1.35 + [undoP, redoP, restartP, kill_proofP, context_thy_onlyP, try_context_thy_onlyP,
    1.36    inform_file_processedP, inform_file_retractedP, process_pgipP];
    1.37  
    1.38  end;