# HG changeset patch
# User wenzelm
# Date 1310118658 -7200
# Node ID e4ece46a9ca70e701c67deab1a2ae93d9ad7f1a0
# Parent  fb3d99df4b1e6c4df24d29db9fdc908bede7a785
clarified Thy_Load.digest_file -- read ML files only once;

diff -r fb3d99df4b1e -r e4ece46a9ca7 src/Pure/ML/ml_context.ML
--- a/src/Pure/ML/ml_context.ML	Fri Jul 08 11:13:21 2011 +0200
+++ b/src/Pure/ML/ml_context.ML	Fri Jul 08 11:50:58 2011 +0200
@@ -33,7 +33,6 @@
     Context.generic option -> (ML_Lex.token list * ML_Lex.token list) * Context.generic option
   val eval: bool -> Position.T -> ML_Lex.token Antiquote.antiquote list -> unit
   val eval_text: bool -> Position.T -> Symbol_Pos.text -> unit
-  val eval_file: Path.T -> unit
   val eval_in: Proof.context option -> bool -> Position.T ->
     ML_Lex.token Antiquote.antiquote list -> unit
   val eval_text_in: Proof.context option -> bool -> Position.T -> Symbol_Pos.text -> unit
@@ -207,7 +206,6 @@
 (* derived versions *)
 
 fun eval_text verbose pos txt = eval verbose pos (ML_Lex.read pos txt);
-fun eval_file path = eval_text true (Path.position path) (File.read path);
 
 fun eval_in ctxt verbose pos ants =
   Context.setmp_thread_data (Option.map Context.Proof ctxt) (fn () => eval verbose pos ants) ();
diff -r fb3d99df4b1e -r e4ece46a9ca7 src/Pure/Thy/thy_load.ML
--- a/src/Pure/Thy/thy_load.ML	Fri Jul 08 11:13:21 2011 +0200
+++ b/src/Pure/Thy/thy_load.ML	Fri Jul 08 11:50:58 2011 +0200
@@ -74,8 +74,9 @@
 fun digest_file dir file =
   let
     val full_path = check_file dir file;
-    val id = SHA1.digest (File.read full_path);
-  in (full_path, id) end;
+    val text = File.read full_path;
+    val id = SHA1.digest text;
+  in (text, (full_path, id)) end;
 
 fun check_thy dir name =
   let
@@ -112,7 +113,7 @@
     fun current (src_path, (_, id)) =
       (case try (digest_file master_dir) 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,17 +122,20 @@
 (* provide files *)
 
 fun provide_file src_path thy =
-  provide (src_path, digest_file (master_directory thy) 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 =
   if is_none (Context.thread_data ()) then
-    ML_Context.eval_file (check_file Path.current src_path)
+    let val path = check_file Path.current src_path
+    in eval_file path (File.read path) end
   else
     let
       val thy = ML_Context.the_global_context ();
-      val (path, id) = digest_file (master_directory thy) src_path;
 
-      val _ = ML_Context.eval_file path;
+      val (text, (path, id)) = digest_file (master_directory thy) src_path;
+      val _ = eval_file path text;
       val _ = Context.>> Local_Theory.propagate_ml_env;
 
       val provide = provide (src_path, (path, id));