--- a/src/Pure/Isar/isar_cmd.ML Fri Jul 16 22:22:59 1999 +0200
+++ b/src/Pure/Isar/isar_cmd.ML Fri Jul 16 22:23:26 1999 +0200
@@ -7,7 +7,6 @@
signature ISAR_CMD =
sig
- val break: Toplevel.transition -> Toplevel.transition
val exit: Toplevel.transition -> Toplevel.transition
val restart: Toplevel.transition -> Toplevel.transition
val quit: Toplevel.transition -> Toplevel.transition
@@ -47,8 +46,6 @@
(* variations on exit *)
-val break = Toplevel.keep (fn state => raise Toplevel.BREAK state);
-
val exit = Toplevel.keep (fn state =>
(Context.set_context (try Toplevel.theory_of state);
writeln "Leaving the Isar loop. Invoke 'loop();' to restart.";
--- a/src/Pure/Isar/isar_syn.ML Fri Jul 16 22:22:59 1999 +0200
+++ b/src/Pure/Isar/isar_syn.ML Fri Jul 16 22:23:26 1999 +0200
@@ -524,10 +524,6 @@
OuterSyntax.improper_command "restart" "restart Isar loop" K.control
(Scan.succeed IsarCmd.restart);
-val breakP =
- OuterSyntax.improper_command "break" "discontinue excursion (keep current state)" K.control
- (Scan.succeed IsarCmd.break);
-
(** the Pure outer syntax **)
@@ -564,7 +560,7 @@
print_thmsP, print_propP, print_termP, print_typeP,
(*system commands*)
cdP, pwdP, use_thyP, use_thy_onlyP, update_thyP, prP, commitP,
- quitP, exitP, restartP, breakP];
+ quitP, exitP, restartP];
end;