simplified/clarified theory loader: more explicit task management, kill old versions at start, commit results only in the very end, non-optional master dependency, do not store text in deps;
explicit Thy_Info.toplevel_begin_theory, which does not maintain theory loader database;
Outer_Syntax.load_thy: modify Toplevel.init for theory loading, and avoid slightly odd implicit batch mode of 'theory' command;
added Thy_Load.begin_theory for clarity;
structure ProofGeneral.ThyLoad.add_path appears to be old ThyLoad.add_path to Proof General, but actually operates on new Thy_Load.master_path instead -- for more precise imitation of theory loader;
moved some basic commands from isar_cmd.ML to isar_syn.ML;
misc tuning and simplification;

--- a/src/Pure/General/secure.ML	Tue Jul 27 12:59:22 2010 +0200
+++ b/src/Pure/General/secure.ML	Tue Jul 27 22:00:26 2010 +0200
@@ -57,7 +57,7 @@
 fun commit () = use_global "commit();";   (*commit is dynamically bound!*)
 
 fun Isar_setup () = use_global "open Unsynchronized;";
-fun PG_setup () = use_global "structure ThyLoad = Thy_Load;";
+fun PG_setup () = use_global "structure ThyLoad = ProofGeneral.ThyLoad;";
 
 
 (* shell commands *)

--- a/src/Pure/Isar/isar_cmd.ML	Tue Jul 27 12:59:22 2010 +0200
+++ b/src/Pure/Isar/isar_cmd.ML	Tue Jul 27 22:00:26 2010 +0200
@@ -34,10 +34,6 @@
   val immediate_proof: Toplevel.transition -> Toplevel.transition
   val done_proof: Toplevel.transition -> Toplevel.transition
   val skip_proof: Toplevel.transition -> Toplevel.transition
-  val init_theory: string * string list * (string * bool) list ->
-    Toplevel.transition -> Toplevel.transition
-  val exit: Toplevel.transition -> Toplevel.transition
-  val quit: Toplevel.transition -> Toplevel.transition
   val pr: string list * (int option * int option) -> Toplevel.transition -> Toplevel.transition
   val disable_pr: Toplevel.transition -> Toplevel.transition
   val enable_pr: Toplevel.transition -> Toplevel.transition
@@ -271,19 +267,6 @@
 val skip_proof = local_skip_proof o global_skip_proof;
 
 
-(* init and exit *)
-
-fun init_theory (name, imports, uses) =
-  Toplevel.init_theory name
-    (Thy_Info.begin_theory name imports (map (apfst Path.explode) uses));
-
-val exit = Toplevel.keep (fn state =>
- (Context.set_thread_data (try Toplevel.generic_theory_of state);
-  raise Toplevel.TERMINATE));
-
-val quit = Toplevel.imperative quit;
-
-
 (* print state *)
 
 fun set_limit _ NONE = ()

--- a/src/Pure/Isar/isar_syn.ML	Tue Jul 27 12:59:22 2010 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Tue Jul 27 22:00:26 2010 +0200
@@ -28,7 +28,10 @@
 
 val _ =
   Outer_Syntax.command "theory" "begin theory" (Keyword.tag_theory Keyword.thy_begin)
-    (Thy_Header.args >> (Toplevel.print oo Isar_Cmd.init_theory));
+    (Thy_Header.args >> (fn (name, imports, uses) =>
+      Toplevel.print o
+        Toplevel.init_theory name
+          (fn () => Thy_Info.toplevel_begin_theory name imports (map (apfst Path.explode) uses))));
 
 val _ =
   Outer_Syntax.command "end" "end (local) theory" (Keyword.tag_theory Keyword.thy_end)
@@ -992,11 +995,14 @@
 
 val _ =
   Outer_Syntax.improper_command "quit" "quit Isabelle" Keyword.control
-    (Parse.opt_unit >> (Toplevel.no_timing oo K Isar_Cmd.quit));
+    (Parse.opt_unit >> (Toplevel.no_timing oo K (Toplevel.imperative quit)));
 
 val _ =
   Outer_Syntax.improper_command "exit" "exit Isar loop" Keyword.control
-    (Scan.succeed (Toplevel.no_timing o Isar_Cmd.exit));
+    (Scan.succeed
+      (Toplevel.no_timing o Toplevel.keep (fn state =>
+        (Context.set_thread_data (try Toplevel.generic_theory_of state);
+          raise Toplevel.TERMINATE))));
 
 end;
 

--- a/src/Pure/Isar/outer_syntax.ML	Tue Jul 27 12:59:22 2010 +0200
+++ b/src/Pure/Isar/outer_syntax.ML	Tue Jul 27 22:00:26 2010 +0200
@@ -31,7 +31,7 @@
   type isar
   val isar: bool -> isar
   val prepare_command: Position.T -> string -> Toplevel.transition
-  val load_thy: string -> Position.T -> string -> (unit -> unit) * theory
+  val load_thy: string -> (unit -> theory) -> Position.T -> string -> (unit -> unit) * theory
 end;
 
 structure Outer_Syntax: OUTER_SYNTAX =
@@ -249,9 +249,9 @@
     handle ERROR msg => (Toplevel.malformed range_pos msg, true)
   end;
 
-fun prepare_unit commands (cmd, proof, proper_proof) =
+fun prepare_unit commands init (cmd, proof, proper_proof) =
   let
-    val (tr, proper_cmd) = prepare_span commands cmd;
+    val (tr, proper_cmd) = prepare_span commands cmd |>> Toplevel.modify_init init;
     val proof_trs = map (prepare_span commands) proof |> filter #2 |> map #1;
   in
     if proper_cmd andalso proper_proof then [(tr, proof_trs)]
@@ -268,7 +268,7 @@
 
 (* load_thy *)
 
-fun load_thy name pos text =
+fun load_thy name init pos text =
   let
     val (lexs, commands) = get_syntax ();
     val time = ! Output.timing;
@@ -279,7 +279,7 @@
     val spans = Source.exhaust (Thy_Syntax.span_source toks);
     val _ = List.app Thy_Syntax.report_span spans;
     val units = Source.exhaust (Thy_Syntax.unit_source (Source.of_list spans))
-      |> Par_List.map (prepare_unit commands) |> flat;
+      |> Par_List.map (prepare_unit commands init) |> flat;
 
     val _ = Present.theory_source name
       (fn () => HTML.html_mode (implode o map Thy_Syntax.present_span) spans);

--- a/src/Pure/Isar/toplevel.ML	Tue Jul 27 12:59:22 2010 +0200
+++ b/src/Pure/Isar/toplevel.ML	Tue Jul 27 22:00:26 2010 +0200
@@ -46,7 +46,8 @@
   val interactive: bool -> transition -> transition
   val print: transition -> transition
   val no_timing: transition -> transition
-  val init_theory: string -> (bool -> theory) -> transition -> transition
+  val init_theory: string -> (unit -> theory) -> transition -> transition
+  val modify_init: (unit -> theory) -> transition -> transition
   val exit: transition -> transition
   val keep: (state -> unit) -> transition -> transition
   val keep': (bool -> state -> unit) -> transition -> transition
@@ -295,16 +296,16 @@
 (* primitive transitions *)
 
 datatype trans =
-  Init of string * (bool -> theory) |    (*theory name, init*)
+  Init of string * (unit -> theory) |    (*theory name, init*)
   Exit |                                 (*formal exit of theory*)
   Keep of bool -> state -> unit |        (*peek at state*)
   Transaction of (bool -> node -> node) * (state -> unit);  (*node transaction and presentation*)
 
 local
 
-fun apply_tr int (Init (_, f)) (State (NONE, _)) =
+fun apply_tr _ (Init (_, f)) (State (NONE, _)) =
       State (SOME (Theory (Context.Theory
-          (Theory.checkpoint (Runtime.controlled_execution f int)), NONE)), NONE)
+          (Theory.checkpoint (Runtime.controlled_execution f ())), NONE)), NONE)
   | apply_tr _ Exit (State (prev as SOME (Theory (Context.Theory _, _)), _)) =
       State (NONE, prev)
   | apply_tr int (Keep f) state =
@@ -394,6 +395,12 @@
 (* basic transitions *)
 
 fun init_theory name f = add_trans (Init (name, f));
+
+fun modify_init f tr =
+  (case init_of tr of
+    SOME name => init_theory name f (reset_trans tr)
+  | NONE => tr);
+
 val exit = add_trans Exit;
 val keep' = add_trans o Keep;
 

--- a/src/Pure/ProofGeneral/proof_general_emacs.ML	Tue Jul 27 12:59:22 2010 +0200
+++ b/src/Pure/ProofGeneral/proof_general_emacs.ML	Tue Jul 27 22:00:26 2010 +0200
@@ -8,9 +8,10 @@
 signature PROOF_GENERAL =
 sig
   val test_markupN: string
+  val sendback: string -> Pretty.T list -> unit
   val init: bool -> unit
   val init_outer_syntax: unit -> unit
-  val sendback: string -> Pretty.T list -> unit
+  structure ThyLoad: sig val add_path: string -> unit end
 end;
 
 structure ProofGeneral: PROOF_GENERAL =
@@ -130,19 +131,17 @@
 (*liberal low-level version*)
 val thy_name = perhaps (try (unsuffix ".thy")) o List.last o space_explode "/";
 
-val inform_file_retracted = Thy_Info.if_known_thy Thy_Info.remove_thy o thy_name;
+val inform_file_retracted = Thy_Info.kill_thy o thy_name;
 
 fun inform_file_processed file =
   let
     val name = thy_name file;
     val _ = name = "" andalso error ("Bad file name: " ^ quote file);
     val _ =
-      if Thy_Info.known_thy name then
-        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))
-      else ();
+      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))
     val _ = Isar.init ();
   in () end;
 
@@ -247,4 +246,12 @@
        Secure.PG_setup ();
        Isar.toplevel_loop {init = true, welcome = true, sync = true, secure = Secure.is_secure ()});
 
+
+(* fake old ThyLoad -- with new semantics *)
+
+structure ThyLoad =
+struct
+  val add_path = Thy_Load.set_master_path o Path.explode;
 end;
+
+end;

--- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Tue Jul 27 12:59:22 2010 +0200
+++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Tue Jul 27 22:00:26 2010 +0200
@@ -217,11 +217,11 @@
 
 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_retracted = Thy_Info.kill_thy o thy_name;
 
 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
+    if Toplevel.is_toplevel state then
       Thy_Info.register_thy (Toplevel.end_theory Position.none state)
         handle ERROR msg =>
           (warning (cat_lines [msg, "Failed to register theory: " ^ quote name]);
@@ -804,8 +804,7 @@
       val filepath = PgipTypes.path_of_pgipurl url
       val filedir = Path.dir filepath
       val thy_name = Path.implode o #1 o Path.split_ext o Path.base
-      val openfile_retract = Output.no_warnings_CRITICAL
-        (Thy_Info.if_known_thy Thy_Info.remove_thy) o thy_name;
+      val openfile_retract = Output.no_warnings_CRITICAL Thy_Info.kill_thy o thy_name;
   in
       case !currently_open_file of
           SOME f => raise PGIP ("<openfile> when a file is already open!\nCurrently open file: " ^

--- a/src/Pure/Thy/thy_info.ML	Tue Jul 27 12:59:22 2010 +0200
+++ b/src/Pure/Thy/thy_info.ML	Tue Jul 27 22:00:26 2010 +0200
@@ -10,8 +10,6 @@
   datatype action = Update | Outdate | Remove
   val add_hook: (action -> string -> unit) -> unit
   val get_names: unit -> string list
-  val known_thy: string -> bool
-  val if_known_thy: (string -> unit) -> string -> unit
   val lookup_theory: string -> theory option
   val get_theory: string -> theory
   val is_finished: string -> bool
@@ -23,7 +21,7 @@
   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 toplevel_begin_theory: string -> string list -> (Path.T * bool) list -> theory
   val register_thy: theory -> unit
   val finish: unit -> unit
 end;
@@ -60,6 +58,9 @@
 fun add_deps name parents G = Graph.add_deps_acyclic (name, parents) G
   handle Graph.CYCLES namess => error (cat_lines (map cycle_msg namess));
 
+fun new_node name parents entry =
+  Graph.new_node (name, entry) #> add_deps name parents;
+
 fun upd_deps name entry G =
   fold (fn parent => Graph.del_edge (parent, name)) (Graph.imm_preds G name) G
   |> Graph.map_node name (K entry);
@@ -72,21 +73,18 @@
 (* thy database *)
 
 type deps =
- {update_time: int,                      (*symbolic time of update; negative value means outdated*)
-  master: (Path.T * File.ident) option,  (*master dependencies for thy file*)
-  text: string,                          (*source text for thy*)
-  parents: string list};                 (*source specification of parents (partially qualified)*)
-
-fun make_deps update_time master text parents : deps =
-  {update_time = update_time, master = master, text = text, parents = parents};
+ {update_time: int,               (*symbolic time of update; negative value means outdated*)
+  master: (Path.T * File.ident),  (*master dependencies for thy file*)
+  parents: string list};          (*source specification of parents (partially qualified)*)
 
-fun init_deps master text parents = SOME (make_deps ~1 master text parents);
+fun make_deps update_time master parents : deps =
+  {update_time = update_time, master = master, parents = parents};
 
-fun master_dir NONE = Path.current
-  | master_dir (SOME (path, _)) = Path.dir path;
+fun init_deps master parents = SOME (make_deps (serial ()) master parents);
 
-fun master_dir' (d: deps option) = the_default Path.current (Option.map (master_dir o #master) d);
-fun master_dir'' d = the_default Path.current (Option.map master_dir' d);
+fun master_dir (path, _) = Path.dir path;
+
+fun master_dir' (d: deps option) = the_default Path.current (Option.map (Path.dir o #1 o #master) d);
 
 fun base_name s = Path.implode (Path.base (Path.explode s));
 
@@ -112,7 +110,6 @@
   SOME (thy_graph Graph.get_node name) handle Graph.UNDEF _ => NONE;
 
 val known_thy = is_some o lookup_thy;
-fun if_known_thy f name = if known_thy name then f name else ();
 
 fun get_thy name =
   (case lookup_thy name of
@@ -128,7 +125,6 @@
 val lookup_deps = Option.map #1 o lookup_thy;
 val get_deps = #1 o get_thy;
 fun change_deps name f = change_thy name (fn (deps, x) => (f deps, x));
-fun put_theory name theory = change_thy name (fn (deps, _) => (deps, SOME theory));
 
 val is_finished = is_none o get_deps;
 val master_directory = master_dir' o get_deps;
@@ -153,10 +149,7 @@
 fun loaded_files name =
   (case get_deps name of
     NONE => []
-  | SOME {master, ...} =>
-      (case master of
-        NONE => []
-      | SOME (thy_path, _) => thy_path :: Thy_Load.loaded_files (get_theory name)));
+  | SOME {master = (thy_path, _), ...} => thy_path :: Thy_Load.loaded_files (get_theory name));
 
 
 
@@ -180,8 +173,8 @@
 fun outdate_thy name =
   if is_finished name orelse is_outdated name then ()
   else CRITICAL (fn () =>
-   (change_deps name (Option.map (fn {master, text, parents, ...} =>
-    make_deps ~1 master text parents)); perform Outdate name));
+   (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));
@@ -191,136 +184,91 @@
 end;
 
 
-(* management data *)
+(* abstract update time *)
 
-structure Management_Data = Theory_Data
+structure Update_Time = Theory_Data
 (
-  type T =
-    Task_Queue.group option *   (*worker thread group*)
-    int;                        (*abstract update time*)
-  val empty = (NONE, 0);
+  type T = int;
+  val empty = 0;
   fun extend _ = empty;
   fun merge _ = empty;
 );
 
-val thy_ord = int_ord o pairself (#2 o Management_Data.get);
-
-
-(* pending proofs *)
-
-fun join_thy name =
-  (case lookup_theory name of
-    NONE => ()
-  | SOME thy => PureThy.join_proofs thy);
-
-fun cancel_thy name =
-  (case lookup_theory name of
-    NONE => ()
-  | SOME thy =>
-      (case #1 (Management_Data.get thy) of
-        NONE => ()
-      | SOME group => Future.cancel_group group));
+val thy_ord = int_ord o pairself Update_Time.get;
 
 
 (* remove theory *)
 
 fun remove_thy name =
-  if is_finished name then error (loader_msg "cannot remove finished theory" [name])
+  if is_finished name then error (loader_msg "cannot change finished theory" [name])
   else
     let
       val succs = thy_graph Graph.all_succs [name];
-      val _ = List.app cancel_thy succs;
       val _ = priority (loader_msg "removing" succs);
       val _ = CRITICAL (fn () =>
         (List.app (perform Remove) succs; change_thys (Graph.del_nodes succs)));
     in () end;
 
-val kill_thy = if_known_thy remove_thy;
-
-
-(* load_thy *)
-
-fun required_by _ [] = ""
-  | required_by s initiators = s ^ "(required by " ^ show_path (rev initiators) ^ ")";
-
-fun load_thy upd_time initiators name =
-  let
-    val _ = priority ("Loading theory " ^ quote name ^ required_by " " initiators);
-    fun corrupted () = error (loader_msg "corrupted dependency information" [name]);
-    val (pos, text) =
-      (case get_deps name of
-        SOME {master = SOME (master_path, _), text, ...} =>
-          if text = "" then corrupted ()
-          else (Path.position master_path, text)
-      | _ => corrupted ());
-    val _ = touch_thy name;
-    val _ =
-      change_deps name (Option.map (fn {master, text, parents, ...} =>
-        make_deps upd_time master text parents));
-    val (after_load, theory) = Outer_Syntax.load_thy name pos text;
-    val _ = put_theory name theory;
-    val _ =
-      CRITICAL (fn () =>
-       (change_deps name
-          (Option.map (fn {update_time, master, parents, ...} =>
-            make_deps update_time master "" parents));
-        perform Update name));
-  in after_load end;
+fun kill_thy name =
+  if known_thy name then remove_thy name
+  else ();
 
 
 (* scheduling loader tasks *)
 
-datatype task = Task of (unit -> unit -> unit) | Finished | Running;
-fun task_finished Finished = true | task_finished _ = false;
+datatype task =
+  Task of string list * (theory list -> (theory * (unit -> unit))) |
+  Finished of theory;
+
+fun task_finished (Task _) = false
+  | task_finished (Finished _) = true;
 
 local
 
+fun schedule_seq task_graph =
+  ((Graph.topological_order task_graph, Symtab.empty) |-> fold (fn name => fn tab =>
+    (case Graph.get_node task_graph name of
+      Task (parents, body) =>
+        let
+          val (thy, after_load) = body (map (the o Symtab.lookup tab) parents);
+          val _ = after_load ();
+        in Symtab.update (name, thy) tab end
+    | Finished thy => Symtab.update (name, thy) tab))) |> ignore;
+
 fun schedule_futures task_graph = uninterruptible (fn _ => fn () =>
   let
-    val tasks = Graph.topological_order task_graph |> map_filter (fn name =>
-      (case Graph.get_node task_graph name of Task body => SOME (name, body) | _ => NONE));
-
+    val tasks = Graph.topological_order task_graph;
     val par_proofs = ! parallel_proofs >= 1;
 
-    fun fork (name, body) tab =
-      let
-        val deps = Graph.imm_preds task_graph name
-          |> map_filter (fn parent =>
-            (case Symtab.lookup tab parent of SOME future => SOME (parent, future) | NONE => NONE));
-        fun failed (parent, future) = if can Future.join future then NONE else SOME parent;
-
-        val future = Future.fork_deps (map #2 deps) (fn () =>
-          (case map_filter failed deps of
-            [] => body ()
-          | bad => error (loader_msg
-              ("failed to load " ^ quote name ^ " (unresolved " ^ commas_quote bad ^ ")") [])));
-        val future' =
-          if par_proofs then future
-          else Future.map (fn after_load => (after_load (); fn () => ())) future;
-      in Symtab.update (name, future') tab end;
-
-    val futures = fold fork tasks Symtab.empty;
+    val futures = (tasks, Symtab.empty) |-> fold (fn name => fn tab =>
+      (case Graph.get_node task_graph name of
+        Task (parents, body) =>
+          let
+            val get = the o Symtab.lookup tab;
+            val deps = map (`get) (Graph.imm_preds task_graph name);
+            fun failed (future, parent) = if can Future.join future then NONE else SOME parent;
 
-    val failed = tasks |> maps (fn (name, _) =>
+            val future = Future.fork_deps (map #1 deps) (fn () =>
+              (case map_filter failed deps of
+                [] => body (map (#1 o Future.join o get) parents)
+              | bad => error (loader_msg
+                  ("failed to load " ^ quote name ^ " (unresolved " ^ commas_quote bad ^ ")") [])));
+            val future' =
+              if par_proofs then future
+              else Future.map (fn (thy, after_load) => (after_load (); (thy, I))) future;
+          in Symtab.update (name, future') tab end
+      | Finished thy => Symtab.update (name, Future.value (thy, I)) tab));
+
+    val exns = tasks |> maps (fn name =>
       let
-        val after_load = Future.join (the (Symtab.lookup futures name));
-        val _ = join_thy name;
+        val (thy, after_load) = Future.join (the (Symtab.lookup futures name));
+        val _ = PureThy.join_proofs thy;
         val _ = after_load ();
-      in [] end handle exn => [(name, exn)]) |> rev;
+      in [] end handle exn => [exn]) |> rev;
 
-    val _ = List.app (kill_thy o #1) failed;
-    val _ = Exn.release_all (map (Exn.Exn o #2) failed);
+    val _ = Exn.release_all (map Exn.Exn exns);
   in () end) ();
 
-fun schedule_seq tasks =
-  Graph.topological_order tasks
-  |> List.app (fn name =>
-    (case Graph.get_node tasks name of
-      Task body =>
-        let val after_load = body ()
-        in after_load () handle exn => (kill_thy name; reraise exn) end
-    | _ => ()));
-
 in
 
 fun schedule_tasks tasks =
@@ -337,34 +285,56 @@
 
 local
 
+fun required_by _ [] = ""
+  | required_by s initiators = s ^ "(required by " ^ show_path (rev initiators) ^ ")";
+
+fun load_thy initiators (deps: deps) text dir name parent_thys =
+  let
+    val _ = kill_thy name;
+    val _ = priority ("Loading theory " ^ quote name ^ required_by " " initiators);
+
+    val {update_time, master = (thy_path, _), ...} = deps;
+    val pos = Path.position thy_path;
+    val uses =
+      map (apfst Path.explode) (#3 (Thy_Header.read pos (Source.of_string_limited 8000 text)));
+    fun init () =
+      Thy_Load.begin_theory dir name parent_thys uses
+      |> Present.begin_theory update_time dir uses
+      |> Update_Time.put update_time;
+
+    val (after_load, theory) = Outer_Syntax.load_thy name init pos text;
+
+    val parent_names = map Context.theory_name parent_thys;
+    fun after_load' () =
+     (after_load ();
+      CRITICAL (fn () =>
+        (change_thys (new_node name parent_names (SOME deps, SOME theory));
+          perform Update name)));
+
+  in (theory, after_load') end;
+
 fun check_deps dir name =
   (case lookup_deps name of
     SOME NONE => (true, NONE, get_parents name)
   | NONE =>
-      let val {master, text, imports = parents, ...} = Thy_Load.deps_thy dir name
-      in (false, init_deps (SOME master) text parents, parents) end
-  | SOME (SOME {update_time, master, text, parents}) =>
-      let
-        val (thy_path, thy_id) = Thy_Load.check_thy dir name;
-        val master' = SOME (thy_path, thy_id);
-      in
-        if Option.map #2 master <> SOME thy_id then
-          let val {text = text', imports = parents', ...} = Thy_Load.deps_thy dir name;
-          in (false, init_deps master' text' parents', parents') end
+      let val {master, imports = parents, ...} = Thy_Load.deps_thy dir name
+      in (false, init_deps master parents, parents) end
+  | SOME (SOME {update_time, master, parents}) =>
+      let val master' = Thy_Load.check_thy dir name in
+        if #2 master <> #2 master' then
+          let val {imports = parents', ...} = Thy_Load.deps_thy dir name;
+          in (false, init_deps master' parents', parents') end
         else
           let
             val current =
               (case lookup_theory name of
                 NONE => false
               | SOME theory => update_time >= 0 andalso Thy_Load.all_current theory);
-            val update_time' = if current then update_time else ~1;
-            val deps' = SOME (make_deps update_time' master' text parents);
+            val update_time' = if current then update_time else serial ();
+            val deps' = SOME (make_deps update_time' master' parents);
           in (current, deps', parents) end
       end);
 
-fun read_text (SOME {update_time, master = master as SOME (path, _), text = _, parents}) =
-  SOME (make_deps update_time master (File.read path) parents);
-
 in
 
 fun require_thys initiators dir strs tasks =
@@ -386,21 +356,22 @@
                 required_by "\n" initiators);
           val parent_names = map base_name parents;
 
-          val (parents_current, tasks_graph') =
+          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 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
-           (if all_current then Finished
-            else Task (fn () => load_thy upd_time initiators name));
-        in (all_current, tasks_graph'') end)
+          val task =
+            if all_current then Finished (get_theory name)
+            else
+              let
+                val SOME {master = (thy_path, _), ...} = deps;
+                val text = File.read thy_path;
+              in Task (parent_names, load_thy initiators (the deps) text dir' name) end;
+        in (all_current, new_node name parent_names task tasks') end)
   end;
 
 end;
@@ -417,56 +388,32 @@
 
 (* begin theory *)
 
-fun check_unfinished name =
-  if known_thy name andalso is_finished name then
-    error (loader_msg "cannot update finished theory" [name])
-  else ();
-
-fun begin_theory name parents uses int =
+fun toplevel_begin_theory name imports uses =
   let
-    val parent_names = map base_name parents;
-    val dir = master_dir'' (lookup_deps name);
-    val _ = check_unfinished name;
-    val _ = if int then use_thys_dir dir parents else ();
-
-    val theory =
-      Theory.begin_theory name (map get_theory parent_names)
-      |> Thy_Load.init dir
-      |> fold (Thy_Load.require o fst) uses;
-
-    val deps =
-      if known_thy name then get_deps name
-      else init_deps NONE "" parents;
-    val _ = change_thys (new_deps name parent_names (deps, NONE));
-
-    val update_time = (case deps of NONE => 0 | SOME {update_time, ...} => update_time);
-    val update_time = if update_time > 0 then update_time else serial ();
-    val theory' = theory
-      |> Management_Data.put (Future.worker_group (), update_time)
-      |> Present.begin_theory update_time dir uses;
-
-    val uses_now = map_filter (fn (x, true) => SOME x | _ => NONE) uses;
-    val theory'' =
-      fold (fn x => Context.theory_map (Thy_Load.exec_ml x) o Theory.checkpoint) uses_now theory';
-  in theory'' end;
+    val dir = Thy_Load.get_master_path ();
+    val _ = kill_thy name;
+    val _ = use_thys_dir dir imports;
+    val parents = map (get_theory o base_name) imports;
+  in Thy_Load.begin_theory dir name parents uses end;
 
 
-(* register existing theories *)
+(* register theory *)
 
 fun register_thy theory =
   let
     val name = Context.theory_name theory;
+    (* FIXME kill_thy 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 master = Thy_Load.check_thy (Thy_Load.master_directory theory) name;
-    val update_time = #2 (Management_Data.get theory);
+    val update_time = Update_Time.get theory;
     val parents =
       (case lookup_deps name of
         SOME (SOME {parents, ...}) => parents
       | _ => parent_names);
-    val deps = make_deps update_time (SOME master) "" parents;
+    val deps = make_deps update_time master parents;
   in
     CRITICAL (fn () =>
      (if known_thy name then

--- a/src/Pure/Thy/thy_load.ML	Tue Jul 27 12:59:22 2010 +0200
+++ b/src/Pure/Thy/thy_load.ML	Tue Jul 27 22:00:26 2010 +0200
@@ -17,8 +17,9 @@
 signature THY_LOAD =
 sig
   include BASIC_THY_LOAD
+  val set_master_path: Path.T -> unit
+  val get_master_path: unit -> Path.T
   val master_directory: theory -> Path.T
-  val init: Path.T -> theory -> theory
   val require: Path.T -> theory -> theory
   val provide: Path.T * (Path.T * File.ident) -> theory -> theory
   val test_file: Path.T -> Path.T -> (Path.T * File.ident) option
@@ -31,6 +32,7 @@
   val provide_file: Path.T -> theory -> theory
   val use_ml: Path.T -> unit
   val exec_ml: Path.T -> generic_theory -> generic_theory
+  val begin_theory: Path.T -> string -> theory list -> (Path.T * bool) list -> theory
 end;
 
 structure Thy_Load: THY_LOAD =
@@ -61,7 +63,7 @@
 
 val master_directory = #master_dir o Files.get;
 
-fun init master_dir = map_files (fn _ => (master_dir, [], []));
+fun master dir = map_files (fn _ => (dir, [], []));
 
 fun require src_path =
   map_files (fn (master_dir, required, provided) =>
@@ -76,9 +78,12 @@
     else (master_dir, required, (src_path, path_info) :: provided));
 
 
-(* maintain load path *)
+(* maintain default paths *)
 
-local val load_path = Unsynchronized.ref [Path.current] in
+local
+  val load_path = Unsynchronized.ref [Path.current];
+  val master_path = Unsynchronized.ref Path.current;
+in
 
 fun show_path () = map Path.implode (! load_path);
 
@@ -97,6 +102,9 @@
 fun search_path dir path =
   distinct (op =) (dir :: (if Path.is_basic path then (! load_path) else [Path.current]));
 
+fun set_master_path path = master_path := path;
+fun get_master_path () = ! master_path;
+
 end;
 
 
@@ -202,6 +210,16 @@
 
 fun exec_ml src_path = ML_Context.exec (fn () => use_ml src_path);
 
+
+(* begin theory *)
+
+fun begin_theory dir name parents uses =
+  Theory.begin_theory name parents
+  |> master dir
+  |> fold (require o fst) uses
+  |> fold (fn (path, true) => Context.theory_map (exec_ml path) o Theory.checkpoint | _ => I) uses
+  |> Theory.checkpoint;
+
 end;
 
 structure Basic_Thy_Load: BASIC_THY_LOAD = Thy_Load;