tuned signature;

--- a/src/Pure/Thy/thy_load.ML	Thu Aug 23 13:55:27 2012 +0200
+++ b/src/Pure/Thy/thy_load.ML	Thu Aug 23 14:58:42 2012 +0200
@@ -8,11 +8,13 @@
 sig
   val master_directory: theory -> Path.T
   val imports_of: theory -> string list
-  val provide: Path.T * SHA1.digest -> theory -> theory
   val thy_path: Path.T -> Path.T
+  val parse_files: string -> (theory -> Token.file list) parser
   val check_thy: Path.T -> string ->
    {master: Path.T * SHA1.digest, text: string, imports: string list,
     uses: (Path.T * bool) list, keywords: Thy_Header.keywords}
+  val provide: Path.T * SHA1.digest -> theory -> theory
+  val provide_parse_files: string -> (theory -> Token.file list * theory) parser
   val load_file: theory -> Path.T -> (Path.T * SHA1.digest) * string
   val use_file: Path.T -> theory -> string * theory
   val loaded_files: theory -> Path.T list
@@ -22,7 +24,6 @@
   val begin_theory: Path.T -> Thy_Header.header -> theory list -> theory
   val load_thy: int -> Path.T -> Thy_Header.header -> Position.T -> string ->
     theory list -> theory * unit future
-  val parse_files: string -> (theory -> Token.file list) parser
   val set_master_path: Path.T -> unit
   val get_master_path: unit -> Path.T
 end;
@@ -58,12 +59,6 @@
 
 fun put_deps master_dir imports = map_files (fn _ => (master_dir, imports, []));
 
-fun provide (src_path, id) =
-  map_files (fn (master_dir, imports, provided) =>
-    if AList.defined (op =) provided src_path then
-      error ("Duplicate use of source file: " ^ Path.print src_path)
-    else (master_dir, imports, (src_path, id) :: provided));
-
 
 (* inlined files *)
 
@@ -147,6 +142,19 @@
 
 (* load files *)
 
+fun provide (src_path, id) =
+  map_files (fn (master_dir, imports, provided) =>
+    if AList.defined (op =) provided src_path then
+      error ("Duplicate use of source file: " ^ Path.print src_path)
+    else (master_dir, imports, (src_path, id) :: provided));
+
+fun provide_parse_files cmd =
+  parse_files cmd >> (fn files => fn thy =>
+    let
+      val fs = files thy;
+      val thy' = fold (fn {src_path, text, ...} => provide (src_path, SHA1.digest text)) fs thy;
+    in (fs, thy') end);
+
 fun load_file thy src_path =
   let
     val full_path = check_file (master_directory thy) src_path;