# HG changeset patch # User wenzelm # Date 1215713010 -7200 # Node ID f3d92b5dcd45cec7987037b85a40dd5233102bc5 # Parent bddf129af8ba7844ba6cd062b77502ea93a9684f added ProofGeneral.isar_kill_proof; diff -r bddf129af8ba -r f3d92b5dcd45 src/Pure/ProofGeneral/proof_general_emacs.ML --- a/src/Pure/ProofGeneral/proof_general_emacs.ML Thu Jul 10 20:03:28 2008 +0200 +++ b/src/Pure/ProofGeneral/proof_general_emacs.ML Thu Jul 10 20:03:30 2008 +0200 @@ -214,6 +214,11 @@ 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 ())))); + fun inform_file_processedP () = OuterSyntax.improper_command "ProofGeneral.inform_file_processed" "(internal)" K.control (P.name >> (fn file => Toplevel.no_timing o @@ -233,7 +238,8 @@ (fn txt => Toplevel.imperative (fn () => ProofGeneralPgip.process_pgip txt)))); fun init_outer_syntax () = List.app (fn f => f ()) - [undoP, restartP, kill_proofP, inform_file_processedP, inform_file_retractedP, process_pgipP]; + [undoP, restartP, kill_proofP, isar_kill_proofP, inform_file_processedP, + inform_file_retractedP, process_pgipP]; end;