# HG changeset patch # User wenzelm # Date 1215716040 -7200 # Node ID 518380d435856ed9b99bd6521ffcba70c65fa29c # Parent 048294b251ee232569c9bda7706d600f8944136e activated new versions of undo, kill_proof; diff -r 048294b251ee -r 518380d43585 src/Pure/ProofGeneral/proof_general_emacs.ML --- a/src/Pure/ProofGeneral/proof_general_emacs.ML Thu Jul 10 20:53:52 2008 +0200 +++ b/src/Pure/ProofGeneral/proof_general_emacs.ML Thu Jul 10 20:54:00 2008 +0200 @@ -204,7 +204,7 @@ fun undoP () = (*undo without output -- historical*) OuterSyntax.improper_command "ProofGeneral.undo" "(internal)" K.control - (Scan.succeed (Toplevel.no_timing o IsarCmd.undo)); + (Scan.succeed (Toplevel.no_timing o Toplevel.imperative (fn () => Isar.undo 1))); fun restartP () = OuterSyntax.improper_command "ProofGeneral.restart" "(internal)" K.control @@ -212,10 +212,6 @@ fun kill_proofP () = OuterSyntax.improper_command "ProofGeneral.kill_proof" "(internal)" K.control - (Scan.succeed (Toplevel.no_timing o IsarCmd.kill_proof_notify tell_clear_goals)); - -fun isar_kill_proofP () = - OuterSyntax.improper_command "ProofGeneral.isar_kill_proof" "(internal)" K.control (Scan.succeed (Toplevel.no_timing o Toplevel.imperative (fn () => (Isar.kill_proof (); tell_clear_goals ())))); @@ -238,8 +234,7 @@ (fn txt => Toplevel.imperative (fn () => ProofGeneralPgip.process_pgip txt)))); fun init_outer_syntax () = List.app (fn f => f ()) - [undoP, restartP, kill_proofP, isar_kill_proofP, inform_file_processedP, - inform_file_retractedP, process_pgipP]; + [undoP, restartP, kill_proofP, inform_file_processedP, inform_file_retractedP, process_pgipP]; end;