src/Pure/Thy/thy_info.ML
changeset 6233 9cc37487f995
parent 6219 b360065c2b07
child 6241 d3c6184ca6c5
     1.1 --- a/src/Pure/Thy/thy_info.ML	Thu Feb 04 18:18:02 1999 +0100
     1.2 +++ b/src/Pure/Thy/thy_info.ML	Thu Feb 04 18:18:19 1999 +0100
     1.3 @@ -17,6 +17,7 @@
     1.4    - stronger handling of missing files (!?!?);
     1.5    - register_theory: do not require finished parents (!?) (no?);
     1.6    - observe verbose flag;
     1.7 +  - touch_thy: msg;
     1.8  *)
     1.9  
    1.10  signature BASIC_THY_INFO =
    1.11 @@ -38,6 +39,7 @@
    1.12    val get_theory: string -> theory
    1.13    val put_theory: theory -> unit
    1.14    val load_file: Path.T -> unit
    1.15 +  val time_load_file: Path.T -> unit
    1.16    val use_thy_only: string -> unit
    1.17    val begin_theory: string -> string list -> theory
    1.18    val end_theory: theory -> theory
    1.19 @@ -65,8 +67,6 @@
    1.20  
    1.21  (* messages *)
    1.22  
    1.23 -val verbose = ref false;
    1.24 -
    1.25  fun gen_msg txt [] = txt
    1.26    | gen_msg txt names = txt ^ " " ^ commas_quote names;
    1.27  
    1.28 @@ -76,6 +76,13 @@
    1.29  fun cycle_msg name names = loader_msg ("cyclic dependency of " ^ show_path (name :: names)) [];
    1.30  
    1.31  
    1.32 +(* verbose mode *)
    1.33 +
    1.34 +val verbose = ref false;
    1.35 +
    1.36 +fun if_verbose f x = if ! verbose then f x else ();
    1.37 +
    1.38 +
    1.39  (* derived graph operations *)		(* FIXME more abstract (!?) *)
    1.40  
    1.41  fun add_deps name parents G =
    1.42 @@ -94,7 +101,7 @@
    1.43  
    1.44  type deps =
    1.45    {present: bool, outdated: bool,
    1.46 -    master: File.info option, files: (Path.T * File.info option) list} option;
    1.47 +    master: (Path.T * File.info) list, files: (Path.T * (Path.T * File.info) option) list} option;
    1.48  
    1.49  fun make_depends present outdated master files =
    1.50    Some {present = present, outdated = outdated, master = master, files = files}: deps;
    1.51 @@ -194,7 +201,7 @@
    1.52      if null missing_files then ()
    1.53      else warning (loader_msg ("unresolved dependencies on file(s) " ^ commas_quote missing_files ^
    1.54        "\nfor theory") [name]);
    1.55 -    change_deps name (fn _ => make_depends true false (Some master) files)
    1.56 +    change_deps name (fn _ => make_depends true false master files)
    1.57    end;
    1.58  
    1.59  
    1.60 @@ -217,13 +224,21 @@
    1.61    end;
    1.62  
    1.63  
    1.64 +fun time_load_file path =
    1.65 +  let val s = Path.pack path in
    1.66 +    timeit (fn () =>
    1.67 +     (writeln ("\n**** Starting " ^ s ^ " ****"); load_file path;
    1.68 +      writeln ("\n**** Finished " ^ s ^ " ****")))
    1.69 +  end;
    1.70 +
    1.71 +
    1.72  (* require_thy *)
    1.73  
    1.74  fun init_deps master files = make_depends false false master (map (rpair None) files);
    1.75  
    1.76  fun load_deps name ml =
    1.77    let val (master, (parents, files)) = ThyLoad.deps_thy name ml
    1.78 -  in (Some (init_deps (Some master) files), parents) end;
    1.79 +  in (Some (init_deps master files), parents) end;
    1.80  
    1.81  fun file_current (_, None) = false
    1.82    | file_current (path, info) = info = ThyLoad.check_file path;
    1.83 @@ -238,7 +253,7 @@
    1.84          | Some {present, outdated, master, files} =>
    1.85              if present andalso not strict then (true, same_deps)
    1.86              else
    1.87 -              let val master' = Some (ThyLoad.check_thy name ml) in
    1.88 +              let val master' = ThyLoad.check_thy name ml in
    1.89                  if master <> master' then (false, load_deps name ml)
    1.90                  else (not outdated andalso forall file_current files, same_deps)
    1.91                end)
    1.92 @@ -258,21 +273,22 @@
    1.93      val (current, (new_deps, parents)) = current_deps ml strict name handle ERROR =>
    1.94        error (loader_msg "The error(s) above occurred while examining theory" [name] ^ "\n" ^
    1.95          required_by initiators);
    1.96 -    val pre_outdated = outdated name;
    1.97 +    val parents_current = map require_parent parents;
    1.98    in
    1.99 -    seq require_parent parents;
   1.100 -    if current andalso pre_outdated = outdated name then ()	(* FIXME ?? *)
   1.101 +    if current andalso forall I parents_current then true
   1.102      else
   1.103        ((case new_deps of
   1.104          Some deps => change_thys (update_node name parents (untouch deps, None))
   1.105 -      | None => ()); load_thy ml time initiators name parents)
   1.106 +      | None => ());
   1.107 +        load_thy ml time initiators name parents;
   1.108 +        false)
   1.109    end;
   1.110  
   1.111 -val weak_use_thy = require_thy true false false false [];
   1.112 -val use_thy      = require_thy true false true false [];
   1.113 -val update_thy   = require_thy true false true true [];
   1.114 -val time_use_thy = require_thy true true true false [];
   1.115 -val use_thy_only = require_thy false false true false [];
   1.116 +val weak_use_thy = K () o require_thy true false false false [];
   1.117 +val use_thy      = K () o require_thy true false true false [];
   1.118 +val update_thy   = K () o require_thy true false true true [];
   1.119 +val time_use_thy = K () o require_thy true true true false [];
   1.120 +val use_thy_only = K () o require_thy false false true false [];
   1.121  
   1.122  
   1.123  (* begin / end theory *)		(* FIXME tune *)
   1.124 @@ -281,7 +297,7 @@
   1.125    let
   1.126      val _ = seq weak_use_thy parents;
   1.127      val theory = PureThy.begin_theory name (map get_theory parents);
   1.128 -    val _ = change_thys (update_node name parents (init_deps None [], Some (theory, Symtab.empty)));
   1.129 +    val _ = change_thys (update_node name parents (init_deps [] [], Some (theory, Symtab.empty)));
   1.130    in theory end;
   1.131  
   1.132  fun end_theory theory =
   1.133 @@ -311,7 +327,8 @@
   1.134  
   1.135  fun update_all () = ();         (* FIXME fake *)
   1.136  
   1.137 -fun finish_all () = (update_all (); change_thys (Graph.map_nodes (fn (_, entry) => (None, entry))));
   1.138 +fun finish_all () =
   1.139 +  (update_all (); change_thys (Graph.map_nodes (fn (_, entry) => (None, entry))));
   1.140  
   1.141  
   1.142  (* register existing theories *)