replaced File.check by specific File.check_file, File.check_dir;
clarified File.full_path -- include parts of former Thy_Load.get_file;
simplified Thy_Load.check_file -- do not read/digest yet;
merged Thy_Load.check_thy/deps_thy -- always read text and parse header;
clarified Thy_Header.read -- NB: partial Path.explode outside of args parser combinator;
Thy_Info.check_deps etc.: File.read exactly once;

--- a/src/HOL/Boogie/Tools/boogie_commands.ML	Sun Mar 20 13:49:21 2011 +0100
+++ b/src/HOL/Boogie/Tools/boogie_commands.ML	Sun Mar 20 17:40:45 2011 +0100
@@ -22,8 +22,7 @@
         "expected file ending " ^ quote ext)
 
     val base_path = Path.explode base_name |> tap check_ext
-    val (full_path, _) =
-      Thy_Load.check_file (Thy_Load.master_directory thy) base_path
+    val full_path = Thy_Load.check_file (Thy_Load.master_directory thy) base_path
 
     val _ = Boogie_VCs.is_closed thy orelse
       error ("Found the beginning of a new Boogie environment, " ^

--- a/src/HOL/SPARK/Tools/spark_commands.ML	Sun Mar 20 13:49:21 2011 +0100
+++ b/src/HOL/SPARK/Tools/spark_commands.ML	Sun Mar 20 17:40:45 2011 +0100
@@ -15,8 +15,7 @@
 
 fun spark_open vc_name thy =
   let
-    val (vc_path, _) = Thy_Load.check_file
-      (Thy_Load.master_directory thy) (Path.explode vc_name);
+    val vc_path = Thy_Load.check_file (Thy_Load.master_directory thy) (Path.explode vc_name);
     val (base, header) =
       (case Path.split_ext vc_path of
         (base, "vcg") => (base, Fdl_Lexer.vcg_header >> K ())

--- a/src/Pure/General/file.ML	Sun Mar 20 13:49:21 2011 +0100
+++ b/src/Pure/General/file.ML	Sun Mar 20 17:40:45 2011 +0100
@@ -11,12 +11,13 @@
   val shell_path: Path.T -> string
   val cd: Path.T -> unit
   val pwd: unit -> Path.T
-  val full_path: Path.T -> Path.T
+  val full_path: Path.T -> Path.T -> Path.T
   val tmp_path: Path.T -> Path.T
   val exists: Path.T -> bool
-  val check: Path.T -> unit
   val rm: Path.T -> unit
   val is_dir: Path.T -> bool
+  val check_dir: Path.T -> Path.T
+  val check_file: Path.T -> Path.T
   val open_input: (TextIO.instream -> 'a) -> Path.T -> 'a
   val open_output: (TextIO.outstream -> 'a) -> Path.T -> 'a
   val open_append: (TextIO.outstream -> 'a) -> Path.T -> 'a
@@ -51,9 +52,18 @@
 val cd = cd o platform_path;
 val pwd = Path.explode o pwd;
 
-fun full_path path =
-  if Path.is_absolute path then path
-  else Path.append (pwd ()) path;
+
+(* full_path *)
+
+fun full_path dir path =
+  let
+    val path' = Path.expand path;
+    val _ = Path.is_current path' andalso error "Bad file specification";
+    val path'' = Path.append dir path';
+  in
+    if Path.is_absolute path'' then path''
+    else Path.append (pwd ()) path''
+  end;
 
 
 (* tmp_path *)
@@ -66,15 +76,19 @@
 
 val exists = can OS.FileSys.modTime o platform_path;
 
-fun check path =
-  if exists path then ()
-  else error ("No such file or directory: " ^ Path.print path);
-
 val rm = OS.FileSys.remove o platform_path;
 
 fun is_dir path =
   the_default false (try OS.FileSys.isDir (platform_path path));
 
+fun check_dir path =
+  if exists path andalso is_dir path then path
+  else error ("No such directory: " ^ Path.print path);
+
+fun check_file path =
+  if exists path andalso not (is_dir path) then path
+  else error ("No such file: " ^ Path.print path);
+
 
 (* open files *)
 

--- a/src/Pure/ProofGeneral/pgip_types.ML	Sun Mar 20 13:49:21 2011 +0100
+++ b/src/Pure/ProofGeneral/pgip_types.ML	Sun Mar 20 17:40:45 2011 +0100
@@ -364,7 +364,9 @@
 
 fun string_of_pgipurl p = Path.implode p
 
-fun attrval_of_pgipurl purl = "file:" ^ (XML.text (File.platform_path (File.full_path purl)))
+fun attrval_of_pgipurl purl =
+  "file:" ^ XML.text (File.platform_path (File.full_path Path.current purl))
+
 fun attrs_of_pgipurl purl = [("url", attrval_of_pgipurl purl)]
 
 val pgipurl_of_attrs = pgipurl_of_string o get_attr "url"

--- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Sun Mar 20 13:49:21 2011 +0100
+++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Sun Mar 20 17:40:45 2011 +0100
@@ -588,14 +588,14 @@
 
         fun filerefs f =
             let val thy = thy_name f
-                val filerefs = #uses (Thy_Load.deps_thy (Path.dir f) thy)
+                val filerefs = map #1 (#uses (Thy_Load.check_thy (Path.dir f) thy))
             in
                 issue_pgip (Setrefs {url=url, thyname=NONE, objtype=SOME PgipTypes.ObjFile,
                                      name=NONE, idtables=[], fileurls=filerefs})
             end
 
         fun thyrefs thy =
-            let val thyrefs = #imports (Thy_Load.deps_thy Path.current thy)
+            let val thyrefs = #imports (Thy_Load.check_thy Path.current thy)
             in
                 issue_pgip (Setrefs {url=url, thyname=thyname, objtype=SOME PgipTypes.ObjTheory,
                                      name=NONE, idtables=[{context=NONE, objtype=PgipTypes.ObjTheory,

--- a/src/Pure/Thy/present.ML	Sun Mar 20 13:49:21 2011 +0100
+++ b/src/Pure/Thy/present.ML	Sun Mar 20 17:40:45 2011 +0100
@@ -462,7 +462,7 @@
 
     val files_html = files |> map (fn (raw_path, loadit) =>
       let
-        val path = #1 (Thy_Load.check_file dir raw_path);
+        val path = Thy_Load.check_file dir raw_path;
         val base = Path.base path;
         val base_html = html_ext base;
         val _ = add_file (Path.append html_prefix base_html,

--- a/src/Pure/Thy/thy_header.ML	Sun Mar 20 13:49:21 2011 +0100
+++ b/src/Pure/Thy/thy_header.ML	Sun Mar 20 17:40:45 2011 +0100
@@ -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 -> string * string list * (string * bool) list
+  val read: Position.T -> string -> string * string list * (Path.T * bool) list
   val thy_path: string -> Path.T
   val split_thy_path: Path.T -> Path.T * string
   val consistent_name: string -> string -> unit
@@ -63,7 +63,8 @@
     |> Source.source Token.stopper (Scan.single (Scan.error (Parse.!!! header))) NONE
     |> Source.get_single;
   in
-    (case res of SOME (x, _) => x
+    (case res of
+      SOME ((name, imports, uses), _) => (name, imports, map (apfst Path.explode) uses)
     | NONE => error ("Unexpected end of input" ^ Position.str_of pos))
   end;
 

--- a/src/Pure/Thy/thy_info.ML	Sun Mar 20 13:49:21 2011 +0100
+++ b/src/Pure/Thy/thy_info.ML	Sun Mar 20 17:40:45 2011 +0100
@@ -232,7 +232,7 @@
     val {master = (thy_path, _), imports} = deps;
     val dir = Path.dir thy_path;
     val pos = Path.position thy_path;
-    val uses = map (apfst Path.explode) (#3 (Thy_Header.read pos text));
+    val (_, _, uses) = Thy_Header.read pos text;
     fun init _ =
       Thy_Load.begin_theory dir name imports parent_thys uses
       |> Present.begin_theory update_time dir uses;
@@ -251,24 +251,20 @@
 
 fun check_deps dir name =
   (case lookup_deps name of
-    SOME NONE => (true, NONE, get_parents name, NONE)
+    SOME NONE => (true, NONE, get_parents name)
   | NONE =>
-      let val {master, text, imports, ...} = Thy_Load.deps_thy dir name
-      in (false, SOME (make_deps master imports), imports, SOME text) end
+      let val {master, text, imports, ...} = Thy_Load.check_thy dir name
+      in (false, SOME (make_deps master imports, text), imports) end
   | SOME (SOME {master, imports}) =>
-      let val master' = Thy_Load.check_thy dir name in
-        if #2 master <> #2 master' then
-          let val {text = text', imports = imports', ...} = Thy_Load.deps_thy dir name;
-          in (false, SOME (make_deps master' imports'), imports', SOME text') end
-        else
-          let
-            val current =
-              (case lookup_theory name of
-                NONE => false
-              | SOME theory => Thy_Load.all_current theory);
-            val deps' = SOME (make_deps master' imports);
-          in (current, deps', imports, NONE) end
-      end);
+      let
+        val {master = master', text = text', imports = imports', ...} = Thy_Load.check_thy dir name;
+        val deps' = SOME (make_deps master' imports', text');
+        val current =
+          #2 master = #2 master' andalso
+            (case lookup_theory name of
+              NONE => false
+            | SOME theory => Thy_Load.all_current theory);
+      in (current, deps', imports') end);
 
 in
 
@@ -285,14 +281,15 @@
       SOME task => (task_finished task, tasks)
     | NONE =>
         let
-          val (current, deps, imports, opt_text) = check_deps dir' name
+          val (current, deps, imports) = check_deps dir' name
             handle ERROR msg => cat_error msg
               (loader_msg "the error(s) above occurred while examining theory" [name] ^
                 required_by "\n" initiators);
 
           val parents = map base_name imports;
           val (parents_current, tasks') =
-            require_thys (name :: initiators) (Path.append dir (master_dir deps)) imports tasks;
+            require_thys (name :: initiators)
+              (Path.append dir (master_dir (Option.map #1 deps))) imports tasks;
 
           val all_current = current andalso parents_current;
           val task =
@@ -300,10 +297,8 @@
             else
               (case deps of
                 NONE => raise Fail "Malformed deps"
-              | SOME (dep as {master = (thy_path, _), ...}) =>
-                  let
-                    val text = (case opt_text of SOME text => text | NONE => File.read thy_path);
-                    val update_time = serial ();
+              | SOME (dep, text) =>
+                  let val update_time = serial ()
                   in Task (parents, load_thy initiators update_time dep text name) end);
         in (all_current, new_entry name parents task tasks') end)
   end;
@@ -336,7 +331,7 @@
 fun register_thy theory =
   let
     val name = Context.theory_name theory;
-    val master = Thy_Load.check_thy (Thy_Load.master_directory theory) name;
+    val {master, ...} = Thy_Load.check_thy (Thy_Load.master_directory theory) name;
     val parents = map Context.theory_name (Theory.parents_of theory);
     val imports = Thy_Load.imports_of theory;
     val deps = make_deps master imports;

--- a/src/Pure/Thy/thy_load.ML	Sun Mar 20 13:49:21 2011 +0100
+++ b/src/Pure/Thy/thy_load.ML	Sun Mar 20 17:40:45 2011 +0100
@@ -9,10 +9,9 @@
   val master_directory: theory -> Path.T
   val imports_of: theory -> string list
   val provide: Path.T * (Path.T * SHA1.digest) -> theory -> theory
-  val check_file: Path.T -> Path.T -> Path.T * SHA1.digest
-  val check_thy: Path.T -> string -> Path.T * SHA1.digest
-  val deps_thy: Path.T -> string ->
-   {master: Path.T * SHA1.digest, text: string, imports: string list, uses: Path.T list}
+  val check_file: Path.T -> Path.T -> Path.T
+  val check_thy: Path.T -> string ->
+    {master: Path.T * SHA1.digest, text: string, imports: string list, uses: (Path.T * bool) list}
   val loaded_files: theory -> Path.T list
   val all_current: theory -> bool
   val provide_file: Path.T -> theory -> theory
@@ -70,37 +69,23 @@
 
 (* check files *)
 
-fun get_file dir src_path =
+fun check_file dir file = File.check_file (File.full_path dir file);
+
+fun digest_file dir file =
   let
-    val path = Path.expand src_path;
-    val _ = Path.is_current path andalso error "Bad file specification";
-    val full_path = File.full_path (Path.append dir path);
-  in
-    if File.exists full_path
-    then SOME (full_path, SHA1.digest (File.read full_path))
-    else NONE
-  end;
-
-fun check_file dir file =
-  (case get_file dir file of
-    SOME path_id => path_id
-  | NONE => error ("Could not find file " ^ Path.print file ^ "\nin " ^ Path.print dir));
+    val full_path = check_file dir file;
+    val id = SHA1.digest (File.read full_path);
+  in (full_path, id) end;
 
 fun check_thy dir name =
-  check_file dir (Thy_Header.thy_path name);
-
-
-(* theory deps *)
-
-fun deps_thy master_dir name =
   let
-    val master as (thy_path, _) = check_thy master_dir name;
-    val text = File.read thy_path;
-    val (name', imports, uses) = Thy_Header.read (Path.position thy_path) text;
+    val master_file = check_file dir (Thy_Header.thy_path name);
+    val text = File.read master_file;
+    val (name', imports, uses) =
+      if name = Context.PureN then (Context.PureN, [], [])
+      else Thy_Header.read (Path.position master_file) 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;
-
+  in {master = (master_file, SHA1.digest text), text = text, imports = imports, uses = uses} end;
 
 
 (* loaded files *)
@@ -125,7 +110,7 @@
   let
     val {master_dir, provided, ...} = Files.get thy;
     fun current (src_path, (_, id)) =
-      (case get_file master_dir src_path of
+      (case try (digest_file master_dir) src_path of
         NONE => false
       | SOME (_, id') => id = id');
   in can check_loaded thy andalso forall current provided end;
@@ -136,15 +121,15 @@
 (* provide files *)
 
 fun provide_file src_path thy =
-  provide (src_path, check_file (master_directory thy) src_path) thy;
+  provide (src_path, digest_file (master_directory thy) src_path) thy;
 
 fun use_ml src_path =
   if is_none (Context.thread_data ()) then
-    ML_Context.eval_file (#1 (check_file Path.current src_path))
+    ML_Context.eval_file (check_file Path.current src_path)
   else
     let
       val thy = ML_Context.the_global_context ();
-      val (path, id) = check_file (master_directory thy) src_path;
+      val (path, id) = digest_file (master_directory thy) src_path;
 
       val _ = ML_Context.eval_file path;
       val _ = Context.>> Local_Theory.propagate_ml_env;

--- a/src/Tools/Code/code_haskell.ML	Sun Mar 20 13:49:21 2011 +0100
+++ b/src/Tools/Code/code_haskell.ML	Sun Mar 20 17:40:45 2011 +0100
@@ -350,7 +350,7 @@
     (*serialization*)
     fun write_module width (SOME destination) (module_name, content) =
           let
-            val _ = File.check destination;
+            val _ = File.check_dir destination;
             val filepath = (Path.append destination o Path.ext "hs" o Path.explode o implode
               o separate "/" o Long_Name.explode) module_name;
             val _ = Isabelle_System.mkdirs (Path.dir filepath);