more abstract Thy_Load.load_file/use_file for external theory resources;
prefer Boogie_Loader.parse_b2i on already loaded text, bypassing former File.fold_lines optimization;

--- a/src/HOL/Boogie/Tools/boogie_commands.ML	Fri Jul 08 13:59:54 2011 +0200
+++ b/src/HOL/Boogie/Tools/boogie_commands.ML	Fri Jul 08 14:37:19 2011 +0200
@@ -22,15 +22,14 @@
         "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 (text, thy') = Thy_Load.use_file base_path thy
 
-    val _ = Boogie_VCs.is_closed thy orelse
+    val _ = Boogie_VCs.is_closed thy' orelse
       error ("Found the beginning of a new Boogie environment, " ^
         "but another Boogie environment is still open.")
   in
-    thy
-    |> Boogie_Loader.load_b2i (not quiet) offsets full_path
-    |> Thy_Load.provide_file base_path
+    thy'
+    |> Boogie_Loader.parse_b2i (not quiet) offsets text
   end
 
 

--- a/src/HOL/Boogie/Tools/boogie_loader.ML	Fri Jul 08 13:59:54 2011 +0200
+++ b/src/HOL/Boogie/Tools/boogie_loader.ML	Fri Jul 08 14:37:19 2011 +0200
@@ -7,6 +7,7 @@
 signature BOOGIE_LOADER =
 sig
   val load_b2i: bool -> (string * int) list -> Path.T -> theory -> theory
+  val parse_b2i: bool -> (string * int) list -> string -> theory -> theory
 end
 
 structure Boogie_Loader: BOOGIE_LOADER =
@@ -321,12 +322,12 @@
 
 datatype token = Token of string | Newline | EOF
 
-fun tokenize path =
+fun tokenize fold_lines input =
   let
     fun blank c = (c = #" " orelse c = #"\t" orelse c = #"\n" orelse c = #"\r")
     fun split line (i, tss) = (i + 1,
       map (pair i) (map Token (String.tokens blank line) @ [Newline]) :: tss)
-  in apsnd (flat o rev) (File.fold_lines split path (1, [])) end
+  in apsnd (flat o rev) (fold_lines split input (1, [])) end
 
 fun stopper i = Scan.stopper (K (i, EOF)) (fn (_, EOF) => true | _ => false)
 
@@ -336,8 +337,8 @@
 
 fun scan_fail msg = Scan.fail_with (scan_err msg)
 
-fun finite scan path =
-  let val (i, ts) = tokenize path
+fun finite scan fold_lines input =
+  let val (i, ts) = tokenize fold_lines input
   in
     (case Scan.error (Scan.finite (stopper i) scan) ts of
       (x, []) => x
@@ -591,6 +592,9 @@
   var_decls tds fds |--
   vcs verbose offsets tds fds)))
 
-fun load_b2i verbose offsets path thy = finite (parse verbose offsets thy) path
+fun load_b2i verbose offsets path thy = finite (parse verbose offsets thy) File.fold_lines path
+
+fun parse_b2i verbose offsets text thy =
+  finite (parse verbose offsets thy) (fn f => fold f o String.tokens (fn c => c = #"\n")) text
 
 end

--- a/src/HOL/Quickcheck_Narrowing.thy	Fri Jul 08 13:59:54 2011 +0200
+++ b/src/HOL/Quickcheck_Narrowing.thy	Fri Jul 08 14:37:19 2011 +0200
@@ -5,9 +5,9 @@
 theory Quickcheck_Narrowing
 imports Quickcheck_Exhaustive
 uses
-  ("~~/src/HOL/Tools/Quickcheck/PNF_Narrowing_Engine.hs")
-  ("~~/src/HOL/Tools/Quickcheck/Narrowing_Engine.hs")
-  ("~~/src/HOL/Tools/Quickcheck/narrowing_generators.ML")
+  ("Tools/Quickcheck/PNF_Narrowing_Engine.hs")
+  ("Tools/Quickcheck/Narrowing_Engine.hs")
+  ("Tools/Quickcheck/narrowing_generators.ML")
 begin
 
 subsection {* Counterexample generator *}
@@ -352,9 +352,7 @@
 
 subsubsection {* Setting up the counterexample generator *}
 
-setup {* Thy_Load.provide_file (Path.explode ("~~/src/HOL/Tools/Quickcheck/PNF_Narrowing_Engine.hs")) *}
-setup {* Thy_Load.provide_file (Path.explode ("~~/src/HOL/Tools/Quickcheck/Narrowing_Engine.hs")) *}
-use "~~/src/HOL/Tools/Quickcheck/narrowing_generators.ML"
+use "Tools/Quickcheck/narrowing_generators.ML"
 
 setup {* Narrowing_Generators.setup *}
 

--- a/src/HOL/SPARK/Tools/spark_commands.ML	Fri Jul 08 13:59:54 2011 +0200
+++ b/src/HOL/SPARK/Tools/spark_commands.ML	Fri Jul 08 14:37:19 2011 +0200
@@ -13,9 +13,10 @@
 structure SPARK_Commands: SPARK_COMMANDS =
 struct
 
+(* FIXME proper Thy_Load.use_file, also for fdl_path and rls_path (!?) *)
 fun spark_open (vc_name, prfx) thy =
   let
-    val vc_path = Thy_Load.check_file (Thy_Load.master_directory thy) (Path.explode vc_name);
+    val ((vc_path, vc_id), vc_text) = Thy_Load.load_file thy (Path.explode vc_name);
     val (base, header) =
       (case Path.split_ext vc_path of
         (base, "vcg") => (base, Fdl_Lexer.vcg_header >> K ())
@@ -27,7 +28,7 @@
     SPARK_VCs.set_vcs
       (snd (Fdl_Parser.parse_declarations (Path.position fdl_path) (File.read fdl_path)))
       (Fdl_Parser.parse_rules (Path.position rls_path) (File.read rls_path))
-      (snd (Fdl_Parser.parse_vcs header (Path.position vc_path) (File.read vc_path)))
+      (snd (Fdl_Parser.parse_vcs header (Path.position vc_path) vc_text))
       base prfx thy
   end;
 

--- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Fri Jul 08 13:59:54 2011 +0200
+++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Fri Jul 08 14:37:19 2011 +0200
@@ -198,8 +198,13 @@
 
 (** invocation of Haskell interpreter **)
 
-val narrowing_engine = File.read (Path.explode "~~/src/HOL/Tools/Quickcheck/Narrowing_Engine.hs")
-val pnf_narrowing_engine = File.read (Path.explode "~~/src/HOL/Tools/Quickcheck/PNF_Narrowing_Engine.hs")
+val narrowing_engine =
+  Context.>>> (Context.map_theory_result
+    (Thy_Load.use_file (Path.explode "Tools/Quickcheck/Narrowing_Engine.hs")))
+
+val pnf_narrowing_engine =
+  Context.>>> (Context.map_theory_result
+    (Thy_Load.use_file (Path.explode "Tools/Quickcheck/PNF_Narrowing_Engine.hs")))
 
 fun exec verbose code =
   ML_Context.exec (fn () => Secure.use_text ML_Env.local_context (0, "generated code") verbose code)

--- a/src/Pure/Thy/thy_load.ML	Fri Jul 08 13:59:54 2011 +0200
+++ b/src/Pure/Thy/thy_load.ML	Fri Jul 08 14:37:19 2011 +0200
@@ -12,9 +12,10 @@
   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 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
   val all_current: theory -> bool
-  val provide_file: Path.T -> theory -> theory
   val use_ml: Path.T -> unit
   val exec_ml: Path.T -> generic_theory -> generic_theory
   val begin_theory: Path.T -> string -> string list -> theory list -> (Path.T * bool) list -> theory
@@ -71,13 +72,6 @@
 
 fun check_file dir file = File.check_file (File.full_path dir file);
 
-fun digest_file dir file =
-  let
-    val full_path = check_file dir file;
-    val text = File.read full_path;
-    val id = SHA1.digest text;
-  in (text, (full_path, id)) end;
-
 fun check_thy dir name =
   let
     val master_file = check_file dir (Thy_Header.thy_path name);
@@ -89,7 +83,20 @@
   in {master = (master_file, SHA1.digest text), text = text, imports = imports, uses = uses} end;
 
 
-(* loaded files *)
+(* load files *)
+
+fun load_file thy src_path =
+  let
+    val full_path = check_file (master_directory thy) src_path;
+    val text = File.read full_path;
+    val id = SHA1.digest text;
+  in ((full_path, id), text) end;
+
+fun use_file src_path thy =
+  let
+    val (path_id, text) = load_file thy src_path;
+    val thy' = provide (src_path, path_id) thy;
+  in (text, thy') end;
 
 val loaded_files = map (#1 o #2) o #provided o Files.get;
 
@@ -109,11 +116,11 @@
 
 fun all_current thy =
   let
-    val {master_dir, provided, ...} = Files.get thy;
+    val {provided, ...} = Files.get thy;
     fun current (src_path, (_, id)) =
-      (case try (digest_file master_dir) src_path of
+      (case try (load_file thy) src_path of
         NONE => false
-      | SOME (_, (_, id')) => id = id');
+      | SOME ((_, id'), _) => id = id');
   in can check_loaded thy andalso forall current provided end;
 
 val _ = Context.>> (Context.map_theory (Theory.at_end (fn thy => (check_loaded thy; NONE))));
@@ -121,9 +128,6 @@
 
 (* provide files *)
 
-fun provide_file src_path thy =
-  provide (src_path, #2 (digest_file (master_directory thy) src_path)) thy;
-
 fun eval_file path text = ML_Context.eval_text true (Path.position path) text;
 
 fun use_ml src_path =
@@ -134,7 +138,7 @@
     let
       val thy = ML_Context.the_global_context ();
 
-      val (text, (path, id)) = digest_file (master_directory thy) src_path;
+      val ((path, id), text) = load_file thy src_path;
       val _ = eval_file path text;
       val _ = Context.>> Local_Theory.propagate_ml_env;