deps_thy/load_thy: store compact text to reduce space by factor 12;

--- a/src/Pure/Isar/outer_syntax.ML	Wed Jul 21 17:57:16 2010 +0200
+++ b/src/Pure/Isar/outer_syntax.ML	Wed Jul 21 20:32:08 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 list -> unit -> unit
+  val load_thy: string -> Position.T -> string -> unit -> unit
 end;
 
 structure Outer_Syntax: OUTER_SYNTAX =
@@ -275,7 +275,7 @@
 
     val _ = Present.init_theory name;
 
-    val toks = Source.exhausted (Thy_Syntax.token_source lexs pos (Source.of_list text));
+    val toks = Source.exhausted (Thy_Syntax.token_source lexs pos (Source.of_string text));
     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))

--- a/src/Pure/Thy/thy_info.ML	Wed Jul 21 17:57:16 2010 +0200
+++ b/src/Pure/Thy/thy_info.ML	Wed Jul 21 20:32:08 2010 +0200
@@ -85,7 +85,7 @@
 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 list,                    (*source text for thy*)
+    text: string,                         (*source text for thy*)
     parents: string list,                 (*source specification of parents (partially qualified)*)
       (*auxiliary files: source path, physical path + identifier*)
     files: (Path.T * (Path.T * File.ident) option) list};
@@ -329,11 +329,13 @@
 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 as _ :: _, files, ...} =>
-          (Path.position master_path, text, files)
-      | _ => error (loader_msg "corrupted dependency information" [name]));
+        SOME {master = SOME (master_path, _), text, files, ...} =>
+          if text = "" then corrupted ()
+          else (Path.position master_path, text, files)
+      | _ => corrupted ());
     val _ = touch_thy name;
     val _ = CRITICAL (fn () =>
       change_deps name (Option.map (fn {master, text, parents, files, ...} =>
@@ -343,7 +345,7 @@
       CRITICAL (fn () =>
        (change_deps name
           (Option.map (fn {update_time, master, parents, files, ...} =>
-            make_deps update_time master [] parents files));
+            make_deps update_time master "" parents files));
         perform Update name));
   in after_load end;
 
@@ -451,7 +453,7 @@
       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);
+  SOME (make_deps update_time master (File.read path) parents files);
 
 in
 
@@ -521,7 +523,7 @@
 
     val deps =
       if known_thy name then get_deps name
-      else init_deps NONE [] parents (map #1 uses);
+      else init_deps NONE "" parents (map #1 uses);
     val _ = change_thys (new_deps name parent_names (deps, NONE));
 
     val update_time = (case deps of NONE => 0 | SOME {update_time, ...} => update_time);
@@ -558,7 +560,7 @@
   in
     CRITICAL (fn () =>
      (change_deps name (Option.map
-       (fn {parents, files, ...} => make_deps upd_time (SOME master) [] parents files));
+       (fn {parents, files, ...} => make_deps upd_time (SOME master) "" parents files));
       perform Update name))
   end;
 

--- a/src/Pure/Thy/thy_load.ML	Wed Jul 21 17:57:16 2010 +0200
+++ b/src/Pure/Thy/thy_load.ML	Wed Jul 21 20:32:08 2010 +0200
@@ -27,7 +27,7 @@
   val check_thy: Path.T -> string -> Path.T * File.ident
   val check_name: string -> string -> unit
   val deps_thy: Path.T -> string ->
-   {master: Path.T * File.ident, text: string list, imports: string list, uses: Path.T list}
+   {master: Path.T * File.ident, text: string, imports: string list, uses: Path.T list}
   val load_ml: Path.T -> Path.T -> Path.T * File.ident
 end;
 
@@ -114,9 +114,9 @@
 fun deps_thy dir name =
   let
     val master as (path, _) = check_thy dir name;
-    val text = explode (File.read path);
+    val text = File.read path;
     val (name', imports, uses) =
-      Thy_Header.read (Path.position path) (Source.of_list_limited 8000 text);
+      Thy_Header.read (Path.position path) (Source.of_list_limited 8000 (explode text));
     val _ = check_name name name';
     val uses = map (Path.explode o #1) uses;
   in {master = master, text = text, imports = imports, uses = uses} end;