# HG changeset patch
# User wenzelm
# Date 912341862 -3600
# Node ID 832ec852fc4ed252ff1b8e8f0247aa162db24018
# Parent  8b6de9bd7d729259aa3066fdd0cfad3842cab8b9
added restart;

diff -r 8b6de9bd7d72 -r 832ec852fc4e src/Pure/Isar/isar_cmd.ML
--- 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;
 
 
diff -r 8b6de9bd7d72 -r 832ec852fc4e src/Pure/Isar/isar_syn.ML
--- 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;