simplified Thy_Header.read -- include Source.of_string_limited here;
tuned;

--- a/src/Pure/ProofGeneral/pgip_parser.ML	Tue Jul 27 22:00:26 2010 +0200
+++ b/src/Pure/ProofGeneral/pgip_parser.ML	Tue Jul 27 22:15:51 2010 +0200
@@ -19,7 +19,7 @@
 fun badcmd text = [D.Badcmd {text = text}];
 
 fun thy_begin text =
-  (case try (Thy_Header.read Position.none) (Source.of_string text) of
+  (case try (Thy_Header.read Position.none) text of
     NONE => D.Opentheory {thyname = NONE, parentnames = [], text = text}
   | SOME (name, imports, _) =>
        D.Opentheory {thyname = SOME name, parentnames = imports, text = text})

--- a/src/Pure/Thy/thy_header.ML	Tue Jul 27 22:00:26 2010 +0200
+++ b/src/Pure/Thy/thy_header.ML	Tue Jul 27 22:15:51 2010 +0200
@@ -7,7 +7,7 @@
 signature THY_HEADER =
 sig
   val args: Token.T list -> (string * string list * (string * bool) list) * Token.T list
-  val read: Position.T -> (string, 'a) Source.source -> string * string list * (string * bool) list
+  val read: Position.T -> string -> string * string list * (string * bool) list
   val thy_path: string -> Path.T
   val split_thy_path: Path.T -> Path.T * string
   val consistent_name: string -> string -> unit
@@ -53,9 +53,10 @@
       (Parse.$$$ theoryN -- Parse.tags) |-- args)) ||
   (Parse.$$$ theoryN -- Parse.tags) |-- Parse.!!! args;
 
-fun read pos src =
+fun read pos str =
   let val res =
-    src
+    str
+    |> Source.of_string_limited 8000
     |> Symbol.source {do_recover = false}
     |> Token.source {do_recover = NONE} (fn () => (header_lexicon, Scan.empty_lexicon)) pos
     |> Token.source_proper

--- a/src/Pure/Thy/thy_info.ML	Tue Jul 27 22:00:26 2010 +0200
+++ b/src/Pure/Thy/thy_info.ML	Tue Jul 27 22:15:51 2010 +0200
@@ -1,7 +1,7 @@
 (*  Title:      Pure/Thy/thy_info.ML
     Author:     Markus Wenzel, TU Muenchen
 
-Main part of theory loader database, including handling of theory and
+Global theory info database, with auto-loading according to theory and
 file dependencies.
 *)
 
@@ -295,8 +295,7 @@
 
     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)));
+    val uses = map (apfst Path.explode) (#3 (Thy_Header.read pos text));
     fun init () =
       Thy_Load.begin_theory dir name parent_thys uses
       |> Present.begin_theory update_time dir uses

--- a/src/Pure/Thy/thy_load.ML	Tue Jul 27 22:00:26 2010 +0200
+++ b/src/Pure/Thy/thy_load.ML	Tue Jul 27 22:15:51 2010 +0200
@@ -71,11 +71,11 @@
       error ("Duplicate source file dependency: " ^ Path.implode src_path)
     else (master_dir, src_path :: required, provided));
 
-fun provide (src_path, path_info) =
+fun provide (src_path, path_id) =
   map_files (fn (master_dir, required, provided) =>
     if AList.defined (op =) provided src_path then
       error ("Duplicate resolution of source file dependency: " ^ Path.implode src_path)
-    else (master_dir, required, (src_path, path_info) :: provided));
+    else (master_dir, required, (src_path, path_id) :: provided));
 
 
 (* maintain default paths *)
@@ -148,10 +148,9 @@
 
 fun deps_thy dir name =
   let
-    val master as (path, _) = check_thy dir name;
-    val text = File.read path;
-    val (name', imports, uses) =
-      Thy_Header.read (Path.position path) (Source.of_string_limited 8000 text);
+    val master as (thy_path, _) = check_thy dir name;
+    val text = File.read thy_path;
+    val (name', imports, uses) = Thy_Header.read (Path.position thy_path) text;
     val _ = Thy_Header.consistent_name name name';
     val uses = map (Path.explode o #1) uses;
   in {master = master, text = text, imports = imports, uses = uses} end;
@@ -179,10 +178,10 @@
 fun all_current thy =
   let
     val {master_dir, provided, ...} = Files.get thy;
-    fun current (src_path, path_info) =
+    fun current (src_path, (_, id)) =
       (case test_file master_dir src_path of
         NONE => false
-      | SOME path_info' => eq_snd (op =) (path_info, path_info'));
+      | SOME (_, id') => id = id');
   in can check_loaded thy andalso forall current provided end;
 
 val _ = Context.>> (Context.map_theory (Theory.at_end (fn thy => (check_loaded thy; NONE))));
@@ -199,14 +198,14 @@
   else
     let
       val thy = ML_Context.the_global_context ();
-      val (path, info) = check_file (master_directory thy) src_path;
+      val (path, id) = check_file (master_directory thy) src_path;
 
       val _ = ML_Context.eval_file path;
       val _ = Context.>> Local_Theory.propagate_ml_env;
 
-      val provide = provide (src_path, (path, info));
+      val provide = provide (src_path, (path, id));
       val _ = Context.>> (Context.mapping provide (Local_Theory.theory provide));
-    in () end
+    in () end;
 
 fun exec_ml src_path = ML_Context.exec (fn () => use_ml src_path);