simplified/clarified register_thy: more precise treatment of new dependencies, remove descendants;
eliminated obsolete touch_child_thys, register_theory;

--- a/src/Pure/ProofGeneral/proof_general_emacs.ML	Sun Jul 25 14:41:48 2010 +0200
+++ b/src/Pure/ProofGeneral/proof_general_emacs.ML	Sun Jul 25 21:42:39 2010 +0200
@@ -138,8 +138,7 @@
     val _ = name = "" andalso error ("Bad file name: " ^ quote file);
     val _ =
       if Thy_Info.known_thy name then
-       (Thy_Info.register_thy name (Toplevel.end_theory Position.none (Isar.state ()));
-        Thy_Info.touch_child_thys name)
+        Thy_Info.register_thy (Toplevel.end_theory Position.none (Isar.state ()))
           handle ERROR msg =>
             (warning (cat_lines ["Failed to register theory: " ^ quote name, msg]);
               tell_file_retracted (Thy_Header.thy_path name))

--- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Sun Jul 25 14:41:48 2010 +0200
+++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Sun Jul 25 21:42:39 2010 +0200
@@ -218,15 +218,14 @@
 val thy_name = Path.implode o #1 o Path.split_ext o Path.base;
 
 val inform_file_retracted = Thy_Info.if_known_thy Thy_Info.remove_thy o thy_name;
-val inform_file_processed = Thy_Info.if_known_thy Thy_Info.touch_child_thys o thy_name;
 
-fun proper_inform_file_processed path state =
+fun inform_file_processed path state =
   let val name = thy_name path in
     if Toplevel.is_toplevel state andalso Thy_Info.known_thy name then
-     (Thy_Info.touch_child_thys name;
-      Thy_Info.register_thy name (Toplevel.end_theory Position.none state) handle ERROR msg =>
-       (warning (cat_lines [msg, "Failed to register theory: " ^ quote name]);
-        tell_file_retracted true (Path.base path)))
+      Thy_Info.register_thy (Toplevel.end_theory Position.none state)
+        handle ERROR msg =>
+          (warning (cat_lines [msg, "Failed to register theory: " ^ quote name]);
+            tell_file_retracted true (Path.base path))
     else raise Toplevel.UNDEF
   end;
 
@@ -819,7 +818,7 @@
 
 fun closefile _ =
     case !currently_open_file of
-        SOME f => (proper_inform_file_processed f (Isar.state());
+        SOME f => (inform_file_processed f (Isar.state ());
                    priority ("Finished working in file: " ^ PgipTypes.string_of_pgipurl f);
                    currently_open_file := NONE)
       | NONE => raise PGIP ("<closefile> when no file is open!")

--- a/src/Pure/Thy/thy_info.ML	Sun Jul 25 14:41:48 2010 +0200
+++ b/src/Pure/Thy/thy_info.ML	Sun Jul 25 21:42:39 2010 +0200
@@ -18,15 +18,13 @@
   val master_directory: string -> Path.T
   val loaded_files: string -> Path.T list
   val touch_thy: string -> unit
-  val touch_child_thys: string -> unit
   val thy_ord: theory * theory -> order
   val remove_thy: string -> unit
   val kill_thy: string -> unit
   val use_thys: string list -> unit
   val use_thy: string -> unit
   val begin_theory: string -> string list -> (Path.T * bool) list -> bool -> theory
-  val register_thy: string -> theory -> unit
-  val register_theory: theory -> unit
+  val register_thy: theory -> unit
   val finish: unit -> unit
 end;
 
@@ -187,7 +185,6 @@
   List.app outdate_thy (thy_graph Graph.all_succs (map_filter unfinished names));
 
 fun touch_thy name = touch_thys [name];
-fun touch_child_thys name = touch_thys (thy_graph Graph.imm_succs name);
 
 end;
 
@@ -454,45 +451,28 @@
 
 (* register existing theories *)
 
-fun register_thy name theory =
-  let
-    val _ = priority ("Registering theory " ^ quote name);
-    val _ = map get_theory (get_parents name);
-    val _ = check_unfinished name;
-    val _ = touch_thy name;
-    val master = #master (Thy_Load.deps_thy Path.current name);
-    val upd_time = #2 (Management_Data.get theory);
-  in
-    CRITICAL (fn () =>
-     (change_deps name (Option.map (fn {parents, ...} =>
-        make_deps upd_time (SOME master) "" parents));
-      put_theory name theory;
-      perform Update name))
-  end;
-
-fun register_theory theory =
+fun register_thy theory =
   let
     val name = Context.theory_name theory;
-    val parents = Theory.parents_of theory;
-    val parent_names = map Context.theory_name parents;
-
-    fun err txt bads =
-      error (loader_msg txt bads ^ "\ncannot register theory " ^ quote name);
+    val _ = priority ("Registering theory " ^ quote name);
+    val parent_names = map Context.theory_name (Theory.parents_of theory);
+    val _ = map get_theory parent_names;
 
-    val nonfinished = filter_out is_finished parent_names;
-    fun get_variant (x, y_name) =
-      if Theory.eq_thy (x, get_theory y_name) then NONE
-      else SOME y_name;
-    val variants = map_filter get_variant (parents ~~ parent_names);
-
-    fun register G =
-      (Graph.new_node (name, (NONE, SOME theory)) G
-        handle Graph.DUP _ => err "duplicate theory entry" [])
-      |> add_deps name parent_names;
+    val master = Thy_Load.check_thy (Thy_Load.master_directory theory) name;
+    val update_time = #2 (Management_Data.get theory);
+    val parents =
+      (case lookup_deps name of
+        SOME (SOME {parents, ...}) => parents
+      | _ => parent_names);
+    val deps = make_deps update_time (SOME master) "" parents;
   in
-    if not (null nonfinished) then err "non-finished parent theories" nonfinished
-    else if not (null variants) then err "different versions of parent theories" variants
-    else CRITICAL (fn () => (change_thys register; perform Update name))
+    CRITICAL (fn () =>
+     (if known_thy name then
+        (List.app remove_thy (thy_graph Graph.imm_succs name);
+          change_thys (Graph.del_nodes [name]))
+      else ();
+      change_thys (new_deps name parents (SOME deps, SOME theory));
+      perform Update name))
   end;
 
 

--- a/src/Pure/pure_setup.ML	Sun Jul 25 14:41:48 2010 +0200
+++ b/src/Pure/pure_setup.ML	Sun Jul 25 21:42:39 2010 +0200
@@ -4,14 +4,16 @@
 Pure theory and ML toplevel setup.
 *)
 
-(* the Pure theories *)
+(* the Pure theory *)
 
 Context.>> (Context.map_theory
  (Outer_Syntax.process_file (Path.explode "Pure.thy") #>
   Theory.end_theory));
+
 structure Pure = struct val thy = ML_Context.the_global_context () end;
+
 Context.set_thread_data NONE;
-Thy_Info.register_theory Pure.thy;
+Thy_Info.register_thy Pure.thy;
 
 
 (* ML toplevel pretty printing *)