tuned msgs;
authorwenzelm
Wed Mar 17 13:41:50 1999 +0100 (1999-03-17)
changeset 6377e7b051fae849
parent 6376 c87f3769203a
child 6378 5780d71203bb
tuned msgs;
removed verbose flag;
src/Pure/Thy/thy_info.ML
     1.1 --- a/src/Pure/Thy/thy_info.ML	Wed Mar 17 13:41:14 1999 +0100
     1.2 +++ b/src/Pure/Thy/thy_info.ML	Wed Mar 17 13:41:50 1999 +0100
     1.3 @@ -12,7 +12,7 @@
     1.4        . elim (via theory_ref);
     1.5    - stronger handling of missing files (!?!?);
     1.6    - register_theory: do not require final parents (!?) (no?);
     1.7 -  - observe verbose flag;
     1.8 +  - hooks for init, update, finish operations (!?);
     1.9  *)
    1.10  
    1.11  signature BASIC_THY_INFO =
    1.12 @@ -31,7 +31,6 @@
    1.13  signature THY_INFO =
    1.14  sig
    1.15    include BASIC_THY_INFO
    1.16 -  val verbose: bool ref
    1.17    val names: unit -> string list
    1.18    val get_theory: string -> theory
    1.19    val put_theory: theory -> unit
    1.20 @@ -63,13 +62,6 @@
    1.21  fun cycle_msg name names = loader_msg ("cyclic dependency of " ^ show_path (name :: names)) [];
    1.22  
    1.23  
    1.24 -(* verbose mode *)
    1.25 -
    1.26 -val verbose = ref false;
    1.27 -
    1.28 -fun if_verbose f x = if ! verbose then f x else ();
    1.29 -
    1.30 -
    1.31  (* derived graph operations *)          (* FIXME more abstract (!?) *)
    1.32  
    1.33  fun add_deps name parents G =
    1.34 @@ -206,7 +198,7 @@
    1.35            if exists (equal path o #1) files then
    1.36              Some (make_deps present outdated master (overwrite (files, (path, Some info))))
    1.37            else (warning (loader_msg "undeclared dependency of theory" [name] ^
    1.38 -            "\nfile: " ^ quote (Path.pack path)); deps)
    1.39 +            "on file: " ^ quote (Path.pack path)); deps)
    1.40        | provide _ _ None = None;
    1.41    in
    1.42      (case apsome PureThy.get_name (Context.get_context ()) of