# 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;