src/Pure/Isar/isar_syn.ML
changeset 6742 6b5cb872d997
parent 6735 e5138b3dbd3b
child 6755 9f830d69a46d
--- a/src/Pure/Isar/isar_syn.ML	Thu May 27 11:39:44 1999 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Thu May 27 20:45:20 1999 +0200
@@ -29,7 +29,7 @@
 
 val kill_excursionP =
   OuterSyntax.command "kill" "kill current excursion" K.control
-    (Scan.succeed (Toplevel.print o Toplevel.kill));
+    (Scan.succeed (Toplevel.print o IsarCmd.kill_theory));
 
 val contextP =
   OuterSyntax.improper_command "context" "switch theory context" K.thy_begin
@@ -320,10 +320,6 @@
 
 (* end proof *)
 
-val kill_proofP =
-  OuterSyntax.improper_command "kill_proof" "abort current proof" K.control
-    (Scan.succeed (Toplevel.print o Toplevel.proof_to_theory IsarThy.kill_proof));
-
 val qed_withP =
   OuterSyntax.improper_command "qed_with" "conclude proof, may patch name and attributes"
     K.qed_block
@@ -363,27 +359,7 @@
       >> (Toplevel.print oo (Toplevel.proof o IsarThy.proof)));
 
 
-(* proof history *)
-
-val cannot_undoP =
-  OuterSyntax.improper_command "cannot_undo" "report 'cannot undo' error message" K.control
-    (P.name >> (Toplevel.print oo IsarCmd.cannot_undo));
-
-val clear_undoP =
-  OuterSyntax.improper_command "clear_undo" "clear undo information" K.control
-    (Scan.succeed (Toplevel.print o IsarCmd.clear_undo));
-
-val undoP =
-  OuterSyntax.improper_command "undo" "undo last command" K.control
-    (Scan.succeed (Toplevel.print o IsarCmd.undo));
-
-val redoP =
-  OuterSyntax.improper_command "redo" "redo last command" K.control
-    (Scan.succeed (Toplevel.print o IsarCmd.redo));
-
-val undosP =
-  OuterSyntax.improper_command "undos" "undo last commands" K.control
-    (P.nat >> (fn n => Toplevel.print o IsarCmd.undos n));
+(* proof navigation *)
 
 val backP =
   OuterSyntax.improper_command "back" "backtracking of proof command" K.prf_script
@@ -402,6 +378,33 @@
     (Scan.succeed (Toplevel.print o Toplevel.proof ProofHistory.top));
 
 
+(* history *)
+
+val cannot_undoP =
+  OuterSyntax.improper_command "cannot_undo" "report 'cannot undo' error message" K.control
+    (P.name >> (Toplevel.print oo IsarCmd.cannot_undo));
+
+val clear_undoP =
+  OuterSyntax.improper_command "clear_undo" "clear undo information" K.control
+    (Scan.succeed (Toplevel.print o IsarCmd.clear_undo));
+
+val redoP =
+  OuterSyntax.improper_command "redo" "redo last command" K.control
+    (Scan.succeed (Toplevel.print o IsarCmd.redo));
+
+val undos_proofP =
+  OuterSyntax.improper_command "undos_proof" "undo last proof commands" K.control
+    (P.nat >> (Toplevel.print oo IsarCmd.undos_proof));
+
+val kill_proofP =
+  OuterSyntax.improper_command "kill_proof" "undo current proof" K.control
+    (Scan.succeed (Toplevel.print o IsarCmd.kill_proof));
+
+val undoP =
+  OuterSyntax.improper_command "undo" "undo last command" K.control
+    (Scan.succeed (Toplevel.print o IsarCmd.undo));
+
+
 
 (** diagnostic commands (for interactive mode only) **)
 
@@ -528,10 +531,10 @@
   print_ast_translationP, token_translationP, oracleP,
   (*proof commands*)
   theoremP, lemmaP, showP, haveP, thusP, henceP, assumeP, fixP, letP,
-  thenP, fromP, factsP, beginP, endP, nextP, kill_proofP, qed_withP,
-  qedP, terminal_proofP, immediate_proofP, default_proofP, refineP,
-  then_refineP, proofP, cannot_undoP, clear_undoP, undoP, redoP,
-  undosP, backP, prevP, upP, topP,
+  thenP, fromP, factsP, beginP, endP, nextP, qed_withP, qedP,
+  terminal_proofP, immediate_proofP, default_proofP, refineP,
+  then_refineP, proofP, backP, prevP, upP, topP, cannot_undoP,
+  clear_undoP, redoP, undos_proofP, kill_proofP, undoP,
   (*diagnostic commands*)
   print_commandsP, print_theoryP, print_syntaxP, print_attributesP,
   print_methodsP, print_theoremsP, print_bindsP, print_lthmsP,