src/Pure/Thy/thy_info.ML

--- a/src/Pure/Thy/thy_info.ML	Tue May 30 16:02:56 2000 +0200
+++ b/src/Pure/Thy/thy_info.ML	Tue May 30 16:03:09 2000 +0200
@@ -246,7 +246,7 @@
     let val name = Path.pack path in
       timeit (fn () =>
        (writeln ("\n**** Starting file " ^ quote name ^ " ****");
-        run_file path;
+        setmp Library.timing true run_file path;
         writeln ("**** Finished file " ^ quote name ^ " ****\n")))
     end
   else run_file path;
@@ -307,10 +307,11 @@
               end)
       end);
 
-fun require_thy ml time strict keep_strict initiators prfx (visited, str) =
+fun require_thy ml time_arg strict keep_strict initiators prfx (visited, str) =
   let
     val path = Path.expand (Path.unpack str);
     val name = Path.pack (Path.base path);
+    val time = time_arg orelse ! Library.timing;
   in
     if name mem_string initiators then error (cycle_msg name initiators) else ();
     if known_thy name andalso is_finished name orelse name mem_string visited then