# HG changeset patch
# User wenzelm
# Date 960148498 -7200
# Node ID d9e09ef531ddee8a1a0862667b613a9a5d788e25
# Parent  371f023d3dbdc644093361e08eef06ec7226e01d
do not setmp Library.timing;

diff -r 371f023d3dbd -r d9e09ef531dd src/Pure/Isar/outer_syntax.ML
--- a/src/Pure/Isar/outer_syntax.ML	Sun Jun 04 19:39:29 2000 +0200
+++ b/src/Pure/Isar/outer_syntax.ML	Sun Jun 04 21:54:58 2000 +0200
@@ -443,7 +443,7 @@
  (if time then
     timeit (fn () =>
      (writeln ("\n**** Starting theory " ^ quote name ^ " ****");
-      setmp Library.timing true (run_thy name) path;
+      run_thy name path;
       writeln ("**** Finished theory " ^ quote name ^ " ****\n")))
   else run_thy name path;
   Context.context (ThyInfo.get_theory name);
diff -r 371f023d3dbd -r d9e09ef531dd src/Pure/Thy/thy_info.ML
--- a/src/Pure/Thy/thy_info.ML	Sun Jun 04 19:39:29 2000 +0200
+++ b/src/Pure/Thy/thy_info.ML	Sun Jun 04 21:54:58 2000 +0200
@@ -246,7 +246,7 @@
     let val name = Path.pack path in
       timeit (fn () =>
        (writeln ("\n**** Starting file " ^ quote name ^ " ****");
-        setmp Library.timing true run_file path;
+        run_file path;
         writeln ("**** Finished file " ^ quote name ^ " ****\n")))
     end
   else run_file path;
@@ -307,11 +307,10 @@
               end)
       end);
 
-fun require_thy ml time_arg strict keep_strict initiators prfx (visited, str) =
+fun require_thy ml time 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
@@ -333,7 +332,7 @@
             ((case new_deps of
               Some deps => change_thys (update_node name parents (deps, None))
             | None => ());
-             load_thy ml time initiators dir name parents;
+             load_thy ml (time orelse ! Library.timing) initiators dir name parents;
              false);
       in (visited', (result, name)) end
   end;