src/Pure/Thy/thy_info.ML

 
 signature THY_INFO =
 sig
   datatype action = Update | Remove
   val add_hook: (action -> string -> unit) -> unit
-  val base_name: string -> string
   val get_names: unit -> string list
   val status: unit -> unit
   val lookup_theory: string -> theory option
   val get_theory: string -> theory
   val is_finished: string -> bool

 
 
 
 (** thy database **)
 
-(* base name *)
-
-fun base_name s = Path.implode (Path.base (Path.explode s));
-
-
 (* messages *)
 
 fun loader_msg txt [] = "Theory loader: " ^ txt
   | loader_msg txt names = "Theory loader: " ^ txt ^ " " ^ commas_quote names;
 

   imports: string list};  (*source specification of imports (partially qualified)*)
 
 fun make_deps master imports : deps = {master = master, imports = imports};
 
 fun master_dir (d: deps option) = the_default Path.current (Option.map (Path.dir o #1 o #master) d);
+fun base_name s = Path.implode (Path.base (Path.explode s));
 
 local
   val database = Unsynchronized.ref (Graph.empty: (deps option * theory option) Graph.T);
 in
   fun get_thys () = ! database;