# HG changeset patch
# User wenzelm
# Date 921674510 -3600
# Node ID e7b051fae84945295cef8933d32bd8794d561f10
# Parent  c87f3769203a1cc86a9afe60e37f19a6b809dc7f
tuned msgs;
removed verbose flag;

diff -r c87f3769203a -r e7b051fae849 src/Pure/Thy/thy_info.ML
--- a/src/Pure/Thy/thy_info.ML	Wed Mar 17 13:41:14 1999 +0100
+++ b/src/Pure/Thy/thy_info.ML	Wed Mar 17 13:41:50 1999 +0100
@@ -12,7 +12,7 @@
       . 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 =
@@ -31,7 +31,6 @@
 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
@@ -63,13 +62,6 @@
 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 =
@@ -206,7 +198,7 @@
           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