removed obsolete touch_all_thys;
authorwenzelm
Fri Aug 17 23:10:46 2007 +0200 (2007-08-17 ago)
changeset 24314665b3ab2dabe
parent 24313 5a6342236a32
child 24315 09b35593d091
removed obsolete touch_all_thys;
src/Pure/Isar/isar_cmd.ML
src/Pure/Isar/isar_syn.ML
src/Pure/Thy/thy_info.ML
     1.1 --- a/src/Pure/Isar/isar_cmd.ML	Fri Aug 17 23:10:45 2007 +0200
     1.2 +++ b/src/Pure/Isar/isar_cmd.ML	Fri Aug 17 23:10:46 2007 +0200
     1.3 @@ -46,7 +46,6 @@
     1.4    val exit: Toplevel.transition -> Toplevel.transition
     1.5    val quit: Toplevel.transition -> Toplevel.transition
     1.6    val touch_child_thys: string -> Toplevel.transition -> Toplevel.transition
     1.7 -  val touch_all_thys: Toplevel.transition -> Toplevel.transition
     1.8    val touch_thy: string -> Toplevel.transition -> Toplevel.transition
     1.9    val remove_thy: string -> Toplevel.transition -> Toplevel.transition
    1.10    val kill_thy: string -> Toplevel.transition -> Toplevel.transition
    1.11 @@ -323,7 +322,6 @@
    1.12  (* touch theories *)
    1.13  
    1.14  fun touch_child_thys name = Toplevel.imperative (fn () => ThyInfo.touch_child_thys name);
    1.15 -val touch_all_thys = Toplevel.imperative ThyInfo.touch_all_thys;
    1.16  fun touch_thy name = Toplevel.imperative (fn () => ThyInfo.touch_thy name);
    1.17  fun remove_thy name = Toplevel.imperative (fn () => ThyInfo.remove_thy name);
    1.18  fun kill_thy name = Toplevel.imperative (fn () => kill_theory name);
     2.1 --- a/src/Pure/Isar/isar_syn.ML	Fri Aug 17 23:10:45 2007 +0200
     2.2 +++ b/src/Pure/Isar/isar_syn.ML	Fri Aug 17 23:10:46 2007 +0200
     2.3 @@ -905,10 +905,6 @@
     2.4    OuterSyntax.improper_command "touch_thy" "outdate theory, including descendants" K.diag
     2.5      (P.name >> (Toplevel.no_timing oo IsarCmd.touch_thy));
     2.6  
     2.7 -val touch_all_thysP =
     2.8 -  OuterSyntax.improper_command "touch_all_thys" "outdate all non-finished theories" K.diag
     2.9 -    (Scan.succeed (Toplevel.no_timing o IsarCmd.touch_all_thys));
    2.10 -
    2.11  val touch_child_thysP =
    2.12    OuterSyntax.improper_command "touch_child_thys" "outdate child theories" K.diag
    2.13      (P.name >> (Toplevel.no_timing oo IsarCmd.touch_child_thys));
    2.14 @@ -1019,9 +1015,8 @@
    2.15    print_full_prfsP, print_propP, print_termP, print_typeP,
    2.16    print_codesetupP,
    2.17    (*system commands*)
    2.18 -  cdP, pwdP, use_thyP, touch_thyP, touch_all_thysP, touch_child_thysP,
    2.19 -  remove_thyP, kill_thyP, display_draftsP, print_draftsP, prP,
    2.20 -  disable_prP, enable_prP, commitP, quitP, exitP, init_toplevelP,
    2.21 -  welcomeP];
    2.22 +  cdP, pwdP, use_thyP, touch_thyP, touch_child_thysP, remove_thyP,
    2.23 +  kill_thyP, display_draftsP, print_draftsP, prP, disable_prP,
    2.24 +  enable_prP, commitP, quitP, exitP, init_toplevelP, welcomeP];
    2.25  
    2.26  end;
     3.1 --- a/src/Pure/Thy/thy_info.ML	Fri Aug 17 23:10:45 2007 +0200
     3.2 +++ b/src/Pure/Thy/thy_info.ML	Fri Aug 17 23:10:46 2007 +0200
     3.3 @@ -30,7 +30,6 @@
     3.4    val get_parents: string -> string list
     3.5    val pretty_theory: theory -> Pretty.T
     3.6    val touch_child_thys: string -> unit
     3.7 -  val touch_all_thys: unit -> unit
     3.8    val load_file: bool -> Path.T -> unit
     3.9    val use: string -> unit
    3.10    val time_use: string -> unit
    3.11 @@ -254,8 +253,6 @@
    3.12  fun touch_thy name = touch_thys [name];
    3.13  fun touch_child_thys name = touch_thys (thy_graph Graph.imm_succs name);
    3.14  
    3.15 -fun touch_all_thys () = List.app outdate_thy (get_names ());
    3.16 -
    3.17  end;
    3.18  
    3.19