load_thy: avoid reloading of text;
tuned;

--- a/src/Pure/Isar/outer_syntax.ML	Sun Jul 29 22:41:55 2007 +0200
+++ b/src/Pure/Isar/outer_syntax.ML	Sun Jul 29 22:41:58 2007 +0200
@@ -256,16 +256,15 @@
       in Toplevel.excursion [Toplevel.empty |> Toplevel.name tr_name |> tr] end
   end;
 
-fun run_thy dir name time =
+fun run_thy dir name pos text time =
   let
-    val master as ((path, _), _) = ThyLoad.check_thy dir name false;
-    val text = Source.of_list (Library.untabify (explode (File.read path)));
+    val text_src = Source.of_list (Library.untabify text);
 
     val _ = Present.init_theory name;
-    val _ = Present.verbatim_source name (fn () => Source.exhaust (Symbol.source false text));
-    val toks = text
+    val _ = Present.verbatim_source name (fn () => Source.exhaust (Symbol.source false text_src));
+    val toks = text_src
       |> Symbol.source false
-      |> T.source NONE (K (get_lexicons ())) (Position.path path)
+      |> T.source NONE (K (get_lexicons ())) pos
       |> Source.exhausted;
     val trs = toks
       |> toplevel_source false false NONE (K (get_parser ()))
@@ -277,15 +276,12 @@
       |> Buffer.content
       |> Present.theory_output name);
     val _ = if time then writeln ("**** Finished theory " ^ quote name ^ " ****\n") else ();
-
-  in master end;
+  in () end;
 
-fun load_thy dir name ml time =
-  let
-    val master = run_thy dir name time;
-    val _ = ML_Context.set_context (SOME (Context.Theory (ThyInfo.get_theory name)));
-    val _ = if ml then try_ml_file dir name time else ();
-  in master end;
+fun load_thy dir name pos text ml time =
+ (run_thy dir name pos text time;
+  ML_Context.set_context (SOME (Context.Theory (ThyInfo.get_theory name)));
+  if ml then try_ml_file dir name time else ());
 
 in
 

--- a/src/Pure/Thy/thy_load.ML	Sun Jul 29 22:41:55 2007 +0200
+++ b/src/Pure/Thy/thy_load.ML	Sun Jul 29 22:41:58 2007 +0200
@@ -26,18 +26,17 @@
   val check_ml: Path.T -> Path.T -> (Path.T * File.ident) option
   val check_thy: Path.T -> string -> bool -> (Path.T * File.ident) * (Path.T * File.ident) option
   val deps_thy: Path.T -> string -> bool ->
-    ((Path.T * File.ident) * (Path.T * File.ident) option) * (string list * Path.T list)
+   {master: (Path.T * File.ident) * (Path.T * File.ident) option,
+    text: string list, imports: string list, uses: Path.T list}
   val load_ml: Path.T -> Path.T -> Path.T * File.ident
-  val load_thy: Path.T -> string -> bool -> bool ->
-    (Path.T * File.ident) * (Path.T * File.ident) option
+  val load_thy: Path.T -> string -> Position.T -> string list -> bool -> bool -> unit
 end;
 
-(*this backdoor sealed later*)
 signature PRIVATE_THY_LOAD =
 sig
   include THY_LOAD
-  val load_thy_fn: (Path.T -> string -> bool -> bool ->
-    (Path.T * File.ident) * (Path.T * File.ident) option) ref
+  (*this backdoor is sealed later*)
+  val load_thy_fn: (Path.T -> string -> Position.T -> string list -> bool -> bool -> unit) ref
 end;
 
 structure ThyLoad: PRIVATE_THY_LOAD =
@@ -106,15 +105,17 @@
 fun deps_thy dir name ml =
   let
     val master as ((path, _), _) = check_thy dir name ml;
+    val text = explode (File.read path);
     val (name', imports, uses) =
-      ThyHeader.read (Position.path path) (Source.of_string_limited (File.read path));
+      ThyHeader.read (Position.path path) (Source.of_list_limited 8000 text);
     val _ = name = name' orelse
       error ("Filename " ^ quote (Path.implode (Path.base path)) ^
         " does not agree with theory name " ^ quote name');
     val ml_file =
       if ml andalso is_some (check_file dir (ml_path name))
       then [ml_path name] else [];
-  in (master, (imports, map (Path.explode o #1) uses @ ml_file)) end;
+    val uses = map (Path.explode o #1) uses @ ml_file;
+  in {master = master, text = text, imports = imports, uses = uses} end;
 
 
 (* load files *)
@@ -125,9 +126,9 @@
   | SOME (path, id) => (ML_Context.use path; (path, id)));
 
 (*dependent on outer syntax*)
-val load_thy_fn = ref (undefined: Path.T -> string -> bool -> bool ->
-  (Path.T * File.ident) * (Path.T * File.ident) option);
-fun load_thy dir name ml time = ! load_thy_fn dir name ml time;
+val load_thy_fn =
+  ref (undefined: Path.T -> string -> Position.T -> string list -> bool -> bool -> unit);
+fun load_thy dir name pos text ml time = ! load_thy_fn dir name pos text ml time;
 
 end;