src/Pure/Thy/thy_info.ML
changeset 6362 bbbea7fecb93
parent 6329 bbd03b119f36
child 6377 e7b051fae849
     1.1 --- a/src/Pure/Thy/thy_info.ML	Fri Mar 12 18:48:11 1999 +0100
     1.2 +++ b/src/Pure/Thy/thy_info.ML	Fri Mar 12 18:48:51 1999 +0100
     1.3 @@ -2,15 +2,12 @@
     1.4      ID:         $Id$
     1.5      Author:     Markus Wenzel, TU Muenchen
     1.6  
     1.7 -Theory loader database: theory and file dependencies, theory values
     1.8 -and user data.
     1.9 +Theory loader database, including theory and file dependencies.
    1.10  
    1.11  TODO:
    1.12 -  - data: ThyInfoFun;
    1.13    - remove operation (GC!?);
    1.14    - update_all operation (!?);
    1.15    - put_theory:
    1.16 -      . include data;
    1.17        . allow for undef entry only;
    1.18        . elim (via theory_ref);
    1.19    - stronger handling of missing files (!?!?);
    1.20 @@ -49,19 +46,7 @@
    1.21    val register_theory: theory -> unit
    1.22  end;
    1.23  
    1.24 -signature PRIVATE_THY_INFO =
    1.25 -sig
    1.26 -  include THY_INFO
    1.27 -(* FIXME
    1.28 -  val init_data: Object.kind -> (Object.T * (Object.T -> Object.T) *
    1.29 -    (Object.T * Object.T -> Object.T) * (Sign.sg -> Object.T -> unit)) -> unit
    1.30 -  val print_data: Object.kind -> string -> unit
    1.31 -  val get_data: Object.kind -> (Object.T -> 'a) -> string -> 'a
    1.32 -  val put_data: Object.kind -> ('a -> Object.T) -> 'a -> unit
    1.33 -*)
    1.34 -end;
    1.35 -
    1.36 -structure ThyInfo: PRIVATE_THY_INFO =
    1.37 +structure ThyInfo: THY_INFO =
    1.38  struct
    1.39  
    1.40  
    1.41 @@ -108,19 +93,13 @@
    1.42  fun make_deps present outdated master files =
    1.43    {present = present, outdated = outdated, master = master, files = files}: deps;
    1.44  
    1.45 -type thy = deps option * (theory * Object.T Symtab.table) option;
    1.46 -type kind = Object.kind * (Object.T * (Object.T -> unit));
    1.47 -
    1.48 +type thy = deps option * theory option;
    1.49  
    1.50  local
    1.51 -  val database = ref (Graph.empty: thy Graph.T, Symtab.empty: kind Symtab.table);
    1.52 +  val database = ref (Graph.empty: thy Graph.T);
    1.53  in
    1.54 -
    1.55 -fun get_thys () = #1 (! database);
    1.56 -fun get_kinds () = #2 (! database);
    1.57 -fun change_thys f = database := (f (get_thys ()), get_kinds ());
    1.58 -fun change_kinds f = database := (get_thys (), f (get_kinds ()));
    1.59 -
    1.60 +  fun get_thys () = ! database;
    1.61 +  fun change_thys f = database := (f (! database));
    1.62  end;
    1.63  
    1.64  
    1.65 @@ -157,17 +136,14 @@
    1.66  
    1.67  fun get_theory name =
    1.68    (case get_thy name of
    1.69 -    (_, Some (theory, _)) => theory
    1.70 +    (_, Some theory) => theory
    1.71    | _ => error (loader_msg "undefined theory entry for" [name]));
    1.72  
    1.73  val theory_of_sign = get_theory o Sign.name_of;
    1.74  val theory_of_thm = theory_of_sign o Thm.sign_of_thm;
    1.75  
    1.76  fun put_theory theory =
    1.77 -  change_thy (PureThy.get_name theory) (fn (deps, _) => (deps, (Some (theory, Symtab.empty))));
    1.78 -
    1.79 -
    1.80 -(** thy data **)  (* FIXME *)
    1.81 +  change_thy (PureThy.get_name theory) (fn (deps, _) => (deps, Some theory));
    1.82  
    1.83  
    1.84  
    1.85 @@ -314,7 +290,7 @@
    1.86    let
    1.87      val _ = seq weak_use_thy parents;
    1.88      val theory = PureThy.begin_theory name (map get_theory parents);
    1.89 -    val _ = change_thys (update_node name parents (init_deps [] [], Some (theory, Symtab.empty)));
    1.90 +    val _ = change_thys (update_node name parents (init_deps [] [], Some theory));
    1.91      val use_paths = mapfilter (fn (x, true) => Some x | _ => None) paths;
    1.92    in Context.setmp (Some theory) (seq use_path) use_paths; theory end;
    1.93  
    1.94 @@ -325,24 +301,6 @@
    1.95  
    1.96  (* finalize entries *)
    1.97  
    1.98 -(* FIXME
    1.99 -fun finishs names =
   1.100 -  let
   1.101 -    fun err txt bads =
   1.102 -      error (loader_msg txt bads ^ "\n" ^ gen_msg "cannot mark" names ^ " as finished");
   1.103 -
   1.104 -    val all_preds = thy_graph Graph.all_preds names;
   1.105 -    val noncurrent = filter_out is_current all_preds;
   1.106 -    val unfinished = filter_out is_finished (all_preds \\ names);
   1.107 -  in
   1.108 -    if not (null noncurrent) then err "non-current theories" noncurrent
   1.109 -    else if not (null unfinished) then err "unfinished ancestor theories" unfinished
   1.110 -    else seq (fn name => change_thy name (apfst (K Finished)))
   1.111 -  end;
   1.112 -
   1.113 -fun finish name = finishs [name];
   1.114 -*)
   1.115 -
   1.116  fun update_all () = ();         (* FIXME fake *)
   1.117  
   1.118  fun finalize_all () =
   1.119 @@ -367,7 +325,7 @@
   1.120      val variants = mapfilter get_variant (parents ~~ parent_names);
   1.121  
   1.122      fun register G =
   1.123 -      (Graph.new_node (name, (None, Some (theory, Symtab.empty))) G
   1.124 +      (Graph.new_node (name, (None, Some theory)) G
   1.125          handle Graph.DUPLICATE _ => err "duplicate theory entry" [])
   1.126        |> add_deps name parent_names;
   1.127    in