src/Pure/Thy/thy_info.ML

 (*  Title:      Pure/Thy/thy_info.ML
     ID:         $Id$
     Author:     Markus Wenzel, TU Muenchen
 
-Theory loader database: theory and file dependencies, theory values
-and user data.
+Theory loader database, including theory and file dependencies.
 
 TODO:
-  - data: ThyInfoFun;
   - remove operation (GC!?);
   - update_all operation (!?);
   - put_theory:
-      . include data;
       . allow for undef entry only;
       . elim (via theory_ref);
   - stronger handling of missing files (!?!?);
   - register_theory: do not require final parents (!?) (no?);
   - observe verbose flag;

   val end_theory: theory -> theory
   val finalize_all: unit -> unit
   val register_theory: theory -> unit
 end;
 
-signature PRIVATE_THY_INFO =
-sig
-  include THY_INFO
-(* FIXME
-  val init_data: Object.kind -> (Object.T * (Object.T -> Object.T) *
-    (Object.T * Object.T -> Object.T) * (Sign.sg -> Object.T -> unit)) -> unit
-  val print_data: Object.kind -> string -> unit
-  val get_data: Object.kind -> (Object.T -> 'a) -> string -> 'a
-  val put_data: Object.kind -> ('a -> Object.T) -> 'a -> unit
-*)
-end;
-
-structure ThyInfo: PRIVATE_THY_INFO =
+structure ThyInfo: THY_INFO =
 struct
 
 
 (** thy database **)
 

     master: (Path.T * File.info) list, files: (Path.T * (Path.T * File.info) option) list};
 
 fun make_deps present outdated master files =
   {present = present, outdated = outdated, master = master, files = files}: deps;
 
-type thy = deps option * (theory * Object.T Symtab.table) option;
-type kind = Object.kind * (Object.T * (Object.T -> unit));
-
+type thy = deps option * theory option;
 
 local
-  val database = ref (Graph.empty: thy Graph.T, Symtab.empty: kind Symtab.table);
+  val database = ref (Graph.empty: thy Graph.T);
 in
-
-fun get_thys () = #1 (! database);
-fun get_kinds () = #2 (! database);
-fun change_thys f = database := (f (get_thys ()), get_kinds ());
-fun change_kinds f = database := (get_thys (), f (get_kinds ()));
-
+  fun get_thys () = ! database;
+  fun change_thys f = database := (f (! database));
 end;
 
 
 (* access thy graph *)
 

 
 (* access theory *)
 
 fun get_theory name =
   (case get_thy name of
-    (_, Some (theory, _)) => theory
+    (_, Some theory) => theory
   | _ => error (loader_msg "undefined theory entry for" [name]));
 
 val theory_of_sign = get_theory o Sign.name_of;
 val theory_of_thm = theory_of_sign o Thm.sign_of_thm;
 
 fun put_theory theory =
-  change_thy (PureThy.get_name theory) (fn (deps, _) => (deps, (Some (theory, Symtab.empty))));
-
-
-(** thy data **)  (* FIXME *)
+  change_thy (PureThy.get_name theory) (fn (deps, _) => (deps, Some theory));
 
 
 
 (** thy operations **)
 

 
 fun begin_theory name parents paths =
   let
     val _ = seq weak_use_thy parents;
     val theory = PureThy.begin_theory name (map get_theory parents);
-    val _ = change_thys (update_node name parents (init_deps [] [], Some (theory, Symtab.empty)));
+    val _ = change_thys (update_node name parents (init_deps [] [], Some theory));
     val use_paths = mapfilter (fn (x, true) => Some x | _ => None) paths;
   in Context.setmp (Some theory) (seq use_path) use_paths; theory end;
 
 fun end_theory theory =
   let val theory' = PureThy.end_theory theory
   in put_theory theory'; theory' end;
 
 
 (* finalize entries *)
-
-(* FIXME
-fun finishs names =
-  let
-    fun err txt bads =
-      error (loader_msg txt bads ^ "\n" ^ gen_msg "cannot mark" names ^ " as finished");
-
-    val all_preds = thy_graph Graph.all_preds names;
-    val noncurrent = filter_out is_current all_preds;
-    val unfinished = filter_out is_finished (all_preds \\ names);
-  in
-    if not (null noncurrent) then err "non-current theories" noncurrent
-    else if not (null unfinished) then err "unfinished ancestor theories" unfinished
-    else seq (fn name => change_thy name (apfst (K Finished)))
-  end;
-
-fun finish name = finishs [name];
-*)
 
 fun update_all () = ();         (* FIXME fake *)
 
 fun finalize_all () =
   (update_all (); change_thys (Graph.map_nodes (fn (_, entry) => (None, entry))));

       if Theory.eq_thy (x, get_theory y_name) then None
       else Some y_name;
     val variants = mapfilter get_variant (parents ~~ parent_names);
 
     fun register G =
-      (Graph.new_node (name, (None, Some (theory, Symtab.empty))) G
+      (Graph.new_node (name, (None, Some theory)) G
         handle Graph.DUPLICATE _ => err "duplicate theory entry" [])
       |> add_deps name parent_names;
   in
     if not (null nonfinal) then err "non-final parent theories" nonfinal
     else if not (null variants) then err "different versions of parent theories" variants