# HG changeset patch
# User clasohm
# Date 799507530 -7200
# Node ID 487089cb173edb8edd52d99c93349290474507eb
# Parent  01379c46ad2df6720c0f5340dae09fbab7f1601c
fixed bug in thy_unchanged that occurred when the .thy file was changed
but the .ML file hadn't been read before;
tmpfile is now deleted immediatly after reading the .thy file in use_thy

diff -r 01379c46ad2d -r 487089cb173e src/Pure/Thy/thy_read.ML
--- a/src/Pure/Thy/thy_read.ML	Wed May 03 15:06:41 1995 +0200
+++ b/src/Pure/Thy/thy_read.ML	Wed May 03 15:25:30 1995 +0200
@@ -109,19 +109,19 @@
 (*Check if a theory file has changed since its last use.
   Return a pair of boolean values for .thy and for .ML *)
 fun thy_unchanged thy thy_file ml_file =
-  let val t = get_thyinfo thy
-  in if is_some t then
-       let val ThyInfo {thy_time, ml_time, ...} = the t
-           val tn = is_none thy_time;
+  case get_thyinfo thy of
+      Some (ThyInfo {thy_time, ml_time, ...}) =>
+       let val tn = is_none thy_time;
            val mn = is_none ml_time
        in if not tn andalso not mn then
-              ((file_info thy_file = the thy_time),
-               (file_info ml_file = the ml_time))
-          else if not tn andalso mn then (true, false)
-          else (false, false)
+            ((file_info thy_file = the thy_time),
+             (file_info ml_file = the ml_time))
+          else if not tn andalso mn then
+            (file_info thy_file = the thy_time, false)
+          else
+            (false, false)
        end
-     else (false, false)
-  end;
+    | None => (false, false)
 
 exception FILE_NOT_FOUND;   (*raised by find_file *)
 
@@ -272,7 +272,10 @@
          if thy_uptodate orelse thy_file = "" then ()
          else (writeln ("Reading \"" ^ name ^ ".thy\"");
                read_thy tname thy_file;
-               use (out_name tname)
+               use (out_name tname);
+
+               if not (!delete_tmpfiles) then ()
+               else delete_file (out_name tname)
               );
          set_info (Some (file_info thy_file)) None tname;
                                        (*mark thy_file as successfully loaded*)
@@ -289,12 +292,7 @@
          set_path ();
 
          (*Mark theories that have to be reloaded*)
-         mark_children tname;
-
-         (*Remove temporary files*)
-         if not (!delete_tmpfiles) orelse (thy_file = "") orelse thy_uptodate
-           then ()
-         else delete_file (out_name tname)
+         mark_children tname
         )
     end;