--- a/src/Pure/Isar/isar_cmd.ML Sun Nov 29 13:17:21 1998 +0100
+++ b/src/Pure/Isar/isar_cmd.ML Sun Nov 29 13:17:42 1998 +0100
@@ -9,6 +9,7 @@
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
val use: string -> Toplevel.transition -> Toplevel.transition
val use_mltext_theory: string -> Toplevel.transition -> Toplevel.transition
@@ -44,6 +45,7 @@
writeln "Leaving the Isar loop. Invoke 'main_loop();' to restart.";
raise Toplevel.TERMINATE));
+val restart = Toplevel.imperative (fn () => raise Toplevel.RESTART);
val quit = Toplevel.imperative quit;
--- a/src/Pure/Isar/isar_syn.ML Sun Nov 29 13:17:21 1998 +0100
+++ b/src/Pure/Isar/isar_syn.ML Sun Nov 29 13:17:42 1998 +0100
@@ -490,6 +490,10 @@
OuterSyntax.parser true "exit" "exit Isar loop"
(Scan.succeed IsarCmd.exit);
+val restartP =
+ OuterSyntax.parser true "restart" "restart Isar loop"
+ (Scan.succeed IsarCmd.restart);
+
val breakP =
OuterSyntax.parser true "break" "discontinue excursion (keep current state)"
(Scan.succeed IsarCmd.break);
@@ -528,7 +532,7 @@
print_methodsP, print_theoremsP, print_bindsP, print_lthmsP,
print_thmsP, print_propP, print_termP, print_typeP,
(*system commands*)
- cdP, pwdP, use_thyP, loadP, prP, commitP, quitP, exitP, breakP];
+ cdP, pwdP, use_thyP, loadP, prP, commitP, quitP, exitP, restartP, breakP];
end;