src/Pure/Isar/isar_syn.ML
changeset 5991 832ec852fc4e
parent 5958 c48efb523a4d
child 6013 6da9ae6d40f5
     1.1 --- a/src/Pure/Isar/isar_syn.ML	Sun Nov 29 13:17:21 1998 +0100
     1.2 +++ b/src/Pure/Isar/isar_syn.ML	Sun Nov 29 13:17:42 1998 +0100
     1.3 @@ -490,6 +490,10 @@
     1.4    OuterSyntax.parser true "exit" "exit Isar loop"
     1.5      (Scan.succeed IsarCmd.exit);
     1.6  
     1.7 +val restartP =
     1.8 +  OuterSyntax.parser true "restart" "restart Isar loop"
     1.9 +    (Scan.succeed IsarCmd.restart);
    1.10 +
    1.11  val breakP =
    1.12    OuterSyntax.parser true "break" "discontinue excursion (keep current state)"
    1.13      (Scan.succeed IsarCmd.break);
    1.14 @@ -528,7 +532,7 @@
    1.15    print_methodsP, print_theoremsP, print_bindsP, print_lthmsP,
    1.16    print_thmsP, print_propP, print_termP, print_typeP,
    1.17    (*system commands*)
    1.18 -  cdP, pwdP, use_thyP, loadP, prP, commitP, quitP, exitP, breakP];
    1.19 +  cdP, pwdP, use_thyP, loadP, prP, commitP, quitP, exitP, restartP, breakP];
    1.20  
    1.21  
    1.22  end;