src/Pure/Thy/thy_info.ML

   - put_theory:
       . 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;
+  - hooks for init, update, finish operations (!?);
 *)
 
 signature BASIC_THY_INFO =
 sig
   val theory: string -> theory

 end;
 
 signature THY_INFO =
 sig
   include BASIC_THY_INFO
-  val verbose: bool ref
   val names: unit -> string list
   val get_theory: string -> theory
   val put_theory: theory -> unit
   val loaded_files: string -> (Path.T * File.info) list
   val load_file: bool -> Path.T -> unit

 
 val show_path = space_implode " via " o map quote;
 fun cycle_msg name names = loader_msg ("cyclic dependency of " ^ show_path (name :: names)) [];
 
 
-(* verbose mode *)
-
-val verbose = ref false;
-
-fun if_verbose f x = if ! verbose then f x else ();
-
-
 (* derived graph operations *)          (* FIXME more abstract (!?) *)
 
 fun add_deps name parents G =
   foldl (fn (H, parent) => Graph.add_edge_acyclic (parent, name) H) (G, parents)
     handle Graph.CYCLES namess => error (cat_lines (map (cycle_msg name) namess));

   let
     fun provide name info (deps as Some {present, outdated, master, files}) =
           if exists (equal path o #1) files then
             Some (make_deps present outdated master (overwrite (files, (path, Some info))))
           else (warning (loader_msg "undeclared dependency of theory" [name] ^
-            "\nfile: " ^ quote (Path.pack path)); deps)
+            "on file: " ^ quote (Path.pack path)); deps)
       | provide _ _ None = None;
   in
     (case apsome PureThy.get_name (Context.get_context ()) of
       None => (ThyLoad.load_file path; ())
     | Some name =>