src/Pure/Thy/thy_info.ML

 
 Main part of theory loader database, including handling of theory and
 file dependencies.
 *)
 
-signature BASIC_THY_INFO =
-sig
-  val touch_thy: string -> unit
-  val remove_thy: string -> unit
-end;
-
 signature THY_INFO =
 sig
-  include BASIC_THY_INFO
   datatype action = Update | Outdate | Remove
   val str_of_action: action -> string
   val add_hook: (action -> string -> unit) -> unit
   val get_names: unit -> string list
   val known_thy: string -> bool

   val the_theory: string -> theory -> theory
   val is_finished: string -> bool
   val master_directory: string -> Path.T
   val loaded_files: string -> Path.T list
   val get_parents: string -> string list
+  val touch_thy: string -> unit
   val touch_child_thys: string -> unit
   val provide_file: Path.T -> string -> unit
   val load_file: bool -> Path.T -> unit
   val exec_file: bool -> Path.T -> Context.generic -> Context.generic
   val use: string -> unit
   val time_use: string -> unit
   val use_thys: string list -> unit
   val use_thy: string -> unit
   val time_use_thy: string -> unit
+  val remove_thy: string -> unit
+  val kill_thy: string -> unit
   val thy_ord: theory * theory -> order
   val begin_theory: string -> string list -> (Path.T * bool) list -> bool -> theory
   val end_theory: theory -> theory
   val register_thy: string -> unit
   val register_theory: theory -> unit

 val time_use_thy = gen_use_thy (require_thy true);
 
 end;
 
 
-(* remove_thy *)
+(* remove theory *)
 
 fun remove_thy name =
   if is_finished name then error (loader_msg "cannot remove finished theory" [name])
   else
     let val succs = thy_graph Graph.all_succs [name] in
       priority (loader_msg "removing" succs);
       CRITICAL (fn () => (List.app (perform Remove) succs; change_thys (Graph.del_nodes succs)))
     end;
+
+val kill_thy = if_known_thy remove_thy;
 
 
 (* update_time *)
 
 structure UpdateTime = TheoryDataFun

 
 fun finish () = change_thys (Graph.map_nodes (fn (_, entry) => (NONE, entry)));
 
 end;
 
-structure BasicThyInfo: BASIC_THY_INFO = ThyInfo;
-open BasicThyInfo;