added restart;
authorwenzelm
Sun Nov 29 13:17:42 1998 +0100 (1998-11-29)
changeset 5991832ec852fc4e
parent 5990 8b6de9bd7d72
child 5992 263051aaf0de
added restart;
src/Pure/Isar/isar_cmd.ML
src/Pure/Isar/isar_syn.ML
     1.1 --- a/src/Pure/Isar/isar_cmd.ML	Sun Nov 29 13:17:21 1998 +0100
     1.2 +++ b/src/Pure/Isar/isar_cmd.ML	Sun Nov 29 13:17:42 1998 +0100
     1.3 @@ -9,6 +9,7 @@
     1.4  sig
     1.5    val break: Toplevel.transition -> Toplevel.transition
     1.6    val exit: Toplevel.transition -> Toplevel.transition
     1.7 +  val restart: Toplevel.transition -> Toplevel.transition
     1.8    val quit: Toplevel.transition -> Toplevel.transition
     1.9    val use: string -> Toplevel.transition -> Toplevel.transition
    1.10    val use_mltext_theory: string -> Toplevel.transition -> Toplevel.transition
    1.11 @@ -44,6 +45,7 @@
    1.12      writeln "Leaving the Isar loop.  Invoke 'main_loop();' to restart.";
    1.13      raise Toplevel.TERMINATE));
    1.14  
    1.15 +val restart = Toplevel.imperative (fn () => raise Toplevel.RESTART);
    1.16  val quit = Toplevel.imperative quit;
    1.17  
    1.18  
     2.1 --- a/src/Pure/Isar/isar_syn.ML	Sun Nov 29 13:17:21 1998 +0100
     2.2 +++ b/src/Pure/Isar/isar_syn.ML	Sun Nov 29 13:17:42 1998 +0100
     2.3 @@ -490,6 +490,10 @@
     2.4    OuterSyntax.parser true "exit" "exit Isar loop"
     2.5      (Scan.succeed IsarCmd.exit);
     2.6  
     2.7 +val restartP =
     2.8 +  OuterSyntax.parser true "restart" "restart Isar loop"
     2.9 +    (Scan.succeed IsarCmd.restart);
    2.10 +
    2.11  val breakP =
    2.12    OuterSyntax.parser true "break" "discontinue excursion (keep current state)"
    2.13      (Scan.succeed IsarCmd.break);
    2.14 @@ -528,7 +532,7 @@
    2.15    print_methodsP, print_theoremsP, print_bindsP, print_lthmsP,
    2.16    print_thmsP, print_propP, print_termP, print_typeP,
    2.17    (*system commands*)
    2.18 -  cdP, pwdP, use_thyP, loadP, prP, commitP, quitP, exitP, breakP];
    2.19 +  cdP, pwdP, use_thyP, loadP, prP, commitP, quitP, exitP, restartP, breakP];
    2.20  
    2.21  
    2.22  end;