# HG changeset patch
# User wenzelm
# Date 1192371226 -7200
# Node ID 7507f590486fad9260299c2667b4d5dbd176fb18
# Parent  3a72718c5ddd5787155ed704d0773d73e3ac5bd7
require_thy: read_text *after* checking parents
  (otherwise outdating an existing descendant will leave the dependencies corrupted);

diff -r 3a72718c5ddd -r 7507f590486f src/Pure/Thy/thy_info.ML
--- a/src/Pure/Thy/thy_info.ML	Sun Oct 14 16:13:45 2007 +0200
+++ b/src/Pure/Thy/thy_info.ML	Sun Oct 14 16:13:46 2007 +0200
@@ -423,11 +423,13 @@
             val current = update_time >= 0 andalso can get_theory name
               andalso forall (is_some o snd) files';
             val update_time' = if current then update_time else ~1;
-            val text' = if current then text else explode (File.read thy_path);
-            val deps' = SOME (make_deps update_time' master' text' parents files');
+            val deps' = SOME (make_deps update_time' master' text parents files');
           in (current, deps', parents) end
       end);
 
+fun read_text (SOME {update_time, master = master as SOME (path, _), text = _, parents, files}) =
+  SOME (make_deps update_time master (explode (File.read path)) parents files);
+
 in
 
 fun require_thys time initiators dir strs tasks =
@@ -454,9 +456,11 @@
               (Path.append dir (master_dir' deps)) parents tasks;
 
           val all_current = current andalso parents_current;
-          val theory = if all_current then SOME (get_theory name) else NONE;
           val _ = if not all_current andalso known_thy name then outdate_thy name else ();
-          val _ = change_thys (new_deps name parent_names (deps, theory));
+          val entry =
+            if all_current then (deps, SOME (get_theory name))
+            else (read_text deps, NONE);
+          val _ = change_thys (new_deps name parent_names entry);
 
           val upd_time = serial ();
           val tasks_graph'' = tasks_graph' |> new_deps name parent_names