removed update_context;
authorwenzelm
Tue Jul 27 21:57:58 1999 +0200 (1999-07-27 ago)
changeset 7102ead5c234b28c
parent 7101 ee79bf6feee2
child 7103 1c44df10a7bc
removed update_context;
removed restart;
added init_toplevel, touch_all_thys, touch_thy, remove_thy, update_thy_only;
src/Pure/Isar/isar_syn.ML
     1.1 --- a/src/Pure/Isar/isar_syn.ML	Tue Jul 27 21:56:32 1999 +0200
     1.2 +++ b/src/Pure/Isar/isar_syn.ML	Tue Jul 27 21:57:58 1999 +0200
     1.3 @@ -32,13 +32,9 @@
     1.4      (Scan.succeed (Toplevel.print o IsarCmd.kill_theory));
     1.5  
     1.6  val contextP =
     1.7 -  OuterSyntax.improper_command "context" "switch theory context" K.thy_begin
     1.8 +  OuterSyntax.improper_command "context" "switch theory context" K.thy_switch
     1.9      (P.name >> (Toplevel.print oo IsarThy.context));
    1.10  
    1.11 -val update_contextP =
    1.12 -  OuterSyntax.improper_command "update_context" "switch theory context, forcing update" K.thy_begin
    1.13 -    (P.name >> (Toplevel.print oo IsarThy.update_context));
    1.14 -
    1.15  
    1.16  
    1.17  (** formal comments **)
    1.18 @@ -494,13 +490,29 @@
    1.19      (P.name >> IsarCmd.use_thy);
    1.20  
    1.21  val use_thy_onlyP =
    1.22 -  OuterSyntax.improper_command "use_thy_only" "use theory file only, ignoring associated ML" K.diag
    1.23 -    (P.name >> IsarCmd.use_thy_only);
    1.24 +  OuterSyntax.improper_command "use_thy_only" "use theory file only, ignoring associated ML"
    1.25 +    K.diag (P.name >> IsarCmd.use_thy_only);
    1.26  
    1.27  val update_thyP =
    1.28    OuterSyntax.improper_command "update_thy" "update theory file" K.diag
    1.29      (P.name >> IsarCmd.update_thy);
    1.30  
    1.31 +val update_thy_onlyP =
    1.32 +  OuterSyntax.improper_command "update_thy_only" "update theory file, ignoring associated ML"
    1.33 +    K.diag (P.name >> IsarCmd.update_thy);
    1.34 +
    1.35 +val touch_thyP =
    1.36 +  OuterSyntax.improper_command "touch_thy" "outdate theory, including descendants" K.diag
    1.37 +    (P.name >> IsarCmd.touch_thy);
    1.38 +
    1.39 +val touch_all_thysP =
    1.40 +  OuterSyntax.improper_command "touch_all_thys" "outdate all non-finished theories" K.diag
    1.41 +    (Scan.succeed IsarCmd.touch_all_thys);
    1.42 +
    1.43 +val remove_thyP =
    1.44 +  OuterSyntax.improper_command "remove_thy" "remove theory from loader database" K.diag
    1.45 +    (P.name >> IsarCmd.remove_thy);
    1.46 +
    1.47  val prP =
    1.48    OuterSyntax.improper_command "pr" "print current toplevel state" K.diag
    1.49      (Scan.succeed (Toplevel.print o Toplevel.imperative (K ())));
    1.50 @@ -520,9 +532,9 @@
    1.51    OuterSyntax.improper_command "exit" "exit Isar loop" K.control
    1.52      (Scan.succeed IsarCmd.exit);
    1.53  
    1.54 -val restartP =
    1.55 -  OuterSyntax.improper_command "restart" "restart Isar loop" K.control
    1.56 -    (Scan.succeed IsarCmd.restart);
    1.57 +val init_toplevelP =
    1.58 +  OuterSyntax.improper_command "init_toplevel" "restart Isar toplevel loop" K.control
    1.59 +    (Scan.succeed IsarCmd.init_toplevel);
    1.60  
    1.61  
    1.62  
    1.63 @@ -539,7 +551,7 @@
    1.64  
    1.65  val parsers = [
    1.66    (*theory structure*)
    1.67 -  theoryP, end_excursionP, kill_excursionP, contextP, update_contextP,
    1.68 +  theoryP, end_excursionP, kill_excursionP, contextP,
    1.69    (*theory sections*)
    1.70    txtP, textP, titleP, chapterP, sectionP, subsectionP,
    1.71    subsubsectionP, classesP, classrelP, defaultsortP, typedeclP,
    1.72 @@ -559,8 +571,9 @@
    1.73    print_methodsP, print_theoremsP, print_bindsP, print_lthmsP,
    1.74    print_thmsP, print_propP, print_termP, print_typeP,
    1.75    (*system commands*)
    1.76 -  cdP, pwdP, use_thyP, use_thy_onlyP, update_thyP, prP, commitP,
    1.77 -  quitP, exitP, restartP];
    1.78 +  cdP, pwdP, use_thyP, use_thy_onlyP, update_thyP, update_thy_onlyP,
    1.79 +  touch_thyP, touch_all_thysP, remove_thyP, prP, commitP, quitP,
    1.80 +  exitP, init_toplevelP];
    1.81  
    1.82  
    1.83  end;