tuned;

--- a/src/Pure/Thy/thy_load.ML	Tue Nov 19 22:12:54 2013 +0100
+++ b/src/Pure/Thy/thy_load.ML	Wed Nov 20 10:51:47 2013 +0100
@@ -1,7 +1,7 @@
 (*  Title:      Pure/Thy/thy_load.ML
     Author:     Makarius
 
-Loading files that contribute to a theory.
+Management of theory sources and auxiliary files.
 *)
 
 signature THY_LOAD =
@@ -9,10 +9,10 @@
   val master_directory: theory -> Path.T
   val imports_of: theory -> (string * Position.T) list
   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, theory_pos: Position.T,
     imports: (string * Position.T) list, keywords: Thy_Header.keywords}
+  val parse_files: string -> (theory -> Token.file list) parser
   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
@@ -55,10 +55,30 @@
 fun put_deps master_dir imports = map_files (fn _ => (master_dir, imports, []));
 
 
-(* auxiliary files *)
+(* theory files *)
+
+val thy_path = Path.ext "thy";
 
 fun check_file dir file = File.check_file (File.full_path dir file);
 
+fun check_thy dir thy_name =
+  let
+    val path = thy_path (Path.basic thy_name);
+    val master_file = check_file dir path;
+    val text = File.read master_file;
+
+    val {name = (name, pos), imports, keywords} =
+      Thy_Header.read (Path.position master_file) text;
+    val _ = thy_name <> name andalso
+      error ("Bad file name " ^ Path.print path ^ " for theory " ^ quote name ^ Position.here pos);
+  in
+   {master = (master_file, SHA1.digest text), text = text, theory_pos = pos,
+    imports = imports, keywords = keywords}
+  end;
+
+
+(* inlined files *)
+
 fun read_files dir cmd (path, pos) =
   let
     fun make_file src_path =
@@ -74,25 +94,8 @@
       [] => read_files (master_directory thy) cmd (Path.explode name, Token.position_of tok)
     | files => map Exn.release files));
 
-
-(* theory files *)
-
-val thy_path = Path.ext "thy";
-
-fun check_thy dir thy_name =
-  let
-    val path = thy_path (Path.basic thy_name);
-    val master_file = check_file dir path;
-    val text = File.read master_file;
-
-    val {name = (name, pos), imports, keywords} =
-      Thy_Header.read (Path.position master_file) text;
-    val _ = thy_name <> name andalso
-      error ("Bad file name " ^ Path.print path ^ " for theory " ^ quote name ^ Position.here pos);
-  in
-   {master = (master_file, SHA1.digest text), text = text, theory_pos = pos,
-    imports = imports, keywords = keywords}
-  end;
+fun resolve_files master_dir =
+  Thy_Syntax.resolve_files (map Exn.Res oo read_files master_dir);
 
 
 (* load files *)
@@ -130,7 +133,7 @@
   in map (File.full_path master_dir o #1) provided end;
 
 
-(* load_thy *)
+(* load theory *)
 
 fun begin_theory master_dir {name, imports, keywords} parents =
   Theory.begin_theory name parents
@@ -166,9 +169,7 @@
 
     val lexs = Keyword.get_lexicons ();
     val toks = Thy_Syntax.parse_tokens lexs text_pos text;
-    val spans =
-      map (Thy_Syntax.resolve_files (map Exn.Res oo read_files master_dir))
-        (Thy_Syntax.parse_spans toks);
+    val spans = map (resolve_files master_dir) (Thy_Syntax.parse_spans toks);
     val elements = Thy_Syntax.parse_elements spans;
 
     fun init () =