# HG changeset patch
# User wenzelm
# Date 1280264502 -7200
# Node ID 9a15982f41fe282603edb7857d43b7b3d141ad96
# Parent  b8c3d4dc1e3ee8fc4b9973ae120b3a9c23a2125e
theory loader: removed obsolete touch/outdate operations (require_thy no longer changes the database implicitly);

diff -r b8c3d4dc1e3e -r 9a15982f41fe src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Tue Jul 27 22:42:53 2010 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Tue Jul 27 23:01:42 2010 +0200
@@ -952,11 +952,6 @@
       Toplevel.no_timing o Toplevel.imperative (fn () => Thy_Info.use_thy name)));
 
 val _ =
-  Outer_Syntax.improper_command "touch_thy" "outdate theory, including descendants" Keyword.diag
-    (Parse.name >> (fn name =>
-      Toplevel.no_timing o Toplevel.imperative (fn () => Thy_Info.touch_thy name)));
-
-val _ =
   Outer_Syntax.improper_command "remove_thy" "remove theory from loader database" Keyword.diag
     (Parse.name >> (fn name =>
       Toplevel.no_timing o Toplevel.imperative (fn () => Thy_Info.remove_thy name)));
diff -r b8c3d4dc1e3e -r 9a15982f41fe src/Pure/ProofGeneral/proof_general_emacs.ML
--- a/src/Pure/ProofGeneral/proof_general_emacs.ML	Tue Jul 27 22:42:53 2010 +0200
+++ b/src/Pure/ProofGeneral/proof_general_emacs.ML	Tue Jul 27 23:01:42 2010 +0200
@@ -116,7 +116,7 @@
 fun trace_action action name =
   if action = Thy_Info.Update then
     List.app tell_file_loaded (Thy_Info.loaded_files name)
-  else if action = Thy_Info.Outdate orelse action = Thy_Info.Remove then
+  else if action = Thy_Info.Remove then
     List.app tell_file_retracted (Thy_Info.loaded_files name)
   else ();
 
diff -r b8c3d4dc1e3e -r 9a15982f41fe src/Pure/ProofGeneral/proof_general_pgip.ML
--- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Tue Jul 27 22:42:53 2010 +0200
+++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Tue Jul 27 23:01:42 2010 +0200
@@ -200,8 +200,6 @@
 fun trace_action action name =
   if action = Thy_Info.Update then
     List.app (tell_file_loaded true) (Thy_Info.loaded_files name)
-  else if action = Thy_Info.Outdate then
-    List.app (tell_file_outdated true) (Thy_Info.loaded_files name)
   else if action = Thy_Info.Remove then
       List.app (tell_file_retracted true) (Thy_Info.loaded_files name)
   else ()
diff -r b8c3d4dc1e3e -r 9a15982f41fe src/Pure/Thy/thy_info.ML
--- a/src/Pure/Thy/thy_info.ML	Tue Jul 27 22:42:53 2010 +0200
+++ b/src/Pure/Thy/thy_info.ML	Tue Jul 27 23:01:42 2010 +0200
@@ -7,7 +7,7 @@
 
 signature THY_INFO =
 sig
-  datatype action = Update | Outdate | Remove
+  datatype action = Update | Remove
   val add_hook: (action -> string -> unit) -> unit
   val get_names: unit -> string list
   val lookup_theory: string -> theory option
@@ -15,7 +15,6 @@
   val is_finished: string -> bool
   val master_directory: string -> Path.T
   val loaded_files: string -> Path.T list
-  val touch_thy: string -> unit
   val thy_ord: theory * theory -> order
   val remove_thy: string -> unit
   val kill_thy: string -> unit
@@ -31,7 +30,7 @@
 
 (** theory loader actions and hooks **)
 
-datatype action = Update | Outdate | Remove;
+datatype action = Update | Remove;
 
 local
   val hooks = Unsynchronized.ref ([]: (action -> string -> unit) list);
@@ -153,35 +152,6 @@
 
 (** thy operations **)
 
-(* maintain update_time *)
-
-local
-
-fun is_outdated name =
-  (case lookup_deps name of
-    SOME (SOME {update_time, ...}) => update_time < 0
-  | _ => false);
-
-fun unfinished name =
-  if is_finished name then (warning (loader_msg "tried to touch finished theory" [name]); NONE)
-  else SOME name;
-
-in
-
-fun outdate_thy name =
-  if is_finished name orelse is_outdated name then ()
-  else CRITICAL (fn () =>
-   (change_deps name (Option.map (fn {master, parents, ...} =>
-    make_deps ~1 master parents)); perform Outdate name));
-
-fun touch_thys names =
-  List.app outdate_thy (thy_graph Graph.all_succs (map_filter unfinished names));
-
-fun touch_thy name = touch_thys [name];
-
-end;
-
-
 (* abstract update time *)
 
 structure Update_Time = Theory_Data
@@ -351,16 +321,12 @@
             handle ERROR msg => cat_error msg
               (loader_msg "the error(s) above occurred while examining theory" [name] ^
                 required_by "\n" initiators);
+
           val parent_names = map base_name parents;
-
           val (parents_current, tasks') =
             require_thys (name :: initiators) (Path.append dir (master_dir deps)) parents tasks;
 
           val all_current = current andalso parents_current;
-
-          (* FIXME ?? *)
-          val _ = if not all_current andalso known_thy name then outdate_thy name else ();
-
           val task =
             if all_current then Finished (get_theory name)
             else