src/Pure/Thy/thy_info.ML
changeset 9036 d9e09ef531dd
parent 8999 ad8260dc6e4a
child 9137 bec42c975d13
     1.1 --- a/src/Pure/Thy/thy_info.ML	Sun Jun 04 19:39:29 2000 +0200
     1.2 +++ b/src/Pure/Thy/thy_info.ML	Sun Jun 04 21:54:58 2000 +0200
     1.3 @@ -246,7 +246,7 @@
     1.4      let val name = Path.pack path in
     1.5        timeit (fn () =>
     1.6         (writeln ("\n**** Starting file " ^ quote name ^ " ****");
     1.7 -        setmp Library.timing true run_file path;
     1.8 +        run_file path;
     1.9          writeln ("**** Finished file " ^ quote name ^ " ****\n")))
    1.10      end
    1.11    else run_file path;
    1.12 @@ -307,11 +307,10 @@
    1.13                end)
    1.14        end);
    1.15  
    1.16 -fun require_thy ml time_arg strict keep_strict initiators prfx (visited, str) =
    1.17 +fun require_thy ml time strict keep_strict initiators prfx (visited, str) =
    1.18    let
    1.19      val path = Path.expand (Path.unpack str);
    1.20      val name = Path.pack (Path.base path);
    1.21 -    val time = time_arg orelse ! Library.timing;
    1.22    in
    1.23      if name mem_string initiators then error (cycle_msg name initiators) else ();
    1.24      if known_thy name andalso is_finished name orelse name mem_string visited then
    1.25 @@ -333,7 +332,7 @@
    1.26              ((case new_deps of
    1.27                Some deps => change_thys (update_node name parents (deps, None))
    1.28              | None => ());
    1.29 -             load_thy ml time initiators dir name parents;
    1.30 +             load_thy ml (time orelse ! Library.timing) initiators dir name parents;
    1.31               false);
    1.32        in (visited', (result, name)) end
    1.33    end;