improved messages;
authorwenzelm
Sat Nov 18 19:48:07 2000 +0100 (2000-11-18 ago)
changeset 10494305b37c8d8a3
parent 10493 76e05ec87b57
child 10495 284ee538991c
improved messages;
src/Pure/theory.ML
     1.1 --- a/src/Pure/theory.ML	Sat Nov 18 19:47:36 2000 +0100
     1.2 +++ b/src/Pure/theory.ML	Sat Nov 18 19:48:07 2000 +0100
     1.3 @@ -164,10 +164,10 @@
     1.4  (* extend logical part of a theory *)
     1.5  
     1.6  fun err_dup_axms names =
     1.7 -  error ("Duplicate axiom name(s) " ^ commas_quote names);
     1.8 +  error ("Duplicate axiom name(s): " ^ commas_quote names);
     1.9  
    1.10  fun err_dup_oras names =
    1.11 -  error ("Duplicate oracles " ^ commas_quote names);
    1.12 +  error ("Duplicate oracles: " ^ commas_quote names);
    1.13  
    1.14  fun ext_theory thy ext_sg ext_deps new_axms new_oras =
    1.15    let
    1.16 @@ -384,12 +384,15 @@
    1.17  
    1.18  fun check_defn sg overloaded ((deps, axms), def as (name, tm)) =
    1.19    let
    1.20 -    fun show_const (c, ty) = quote (Pretty.string_of (Pretty.block
    1.21 -      [Pretty.str (c ^ " ::"), Pretty.brk 1, Sign.pretty_typ sg ty]));
    1.22 +    fun pretty_const (c, ty) = [Pretty.str c, Pretty.str " ::", Pretty.brk 1,
    1.23 +      Pretty.quote (Sign.pretty_typ sg (#1 (Type.freeze_thaw_type ty)))];
    1.24  
    1.25 -    fun def_txt c_ty = "Definition of " ^ show_const c_ty;
    1.26 -    fun show_defn c (dfn, ty') = show_const (c, ty') ^ " in " ^ dfn;
    1.27 -    fun show_defns c = cat_lines o map (show_defn c);
    1.28 +    fun def_txt (c_ty, txt) = Pretty.block
    1.29 +      (Pretty.str "Definition of " :: pretty_const c_ty @
    1.30 +        (if txt = "" then [] else [Pretty.str txt]));
    1.31 +
    1.32 +    fun show_defn c (dfn, ty') = Pretty.block
    1.33 +      (Pretty.str "  " :: pretty_const (c, ty') @ [Pretty.str " in ", Pretty.str dfn]);
    1.34  
    1.35      val (c_ty as (c, ty), rhs) = dest_defn tm
    1.36        handle TERM (msg, _) => err_in_defn sg name msg;
    1.37 @@ -400,7 +403,8 @@
    1.38      val clashed = clash_defns c_ty axms;
    1.39    in
    1.40      if not (null clashed) then
    1.41 -      err_in_defn sg name (def_txt c_ty ^"\nclashes with "^ show_defns c clashed)
    1.42 +      err_in_defn sg name (Pretty.string_of (Pretty.chunks
    1.43 +        (def_txt (c_ty, " clashes with") :: map (show_defn c) clashed)))
    1.44      else
    1.45        (case overloading sg c_decl ty of
    1.46          NoOverloading =>
    1.47 @@ -408,12 +412,13 @@
    1.48                handle Graph.CYCLES namess => err_in_defn sg name (cycle_msg namess),
    1.49              def :: axms)
    1.50        | Useless =>
    1.51 -           err_in_defn sg name (Library.setmp show_sorts true def_txt c_ty ^
    1.52 -             "\nimposes additional sort constraints on the declared type of the constant.")
    1.53 +           err_in_defn sg name (Pretty.string_of (Pretty.chunks
    1.54 +             [Library.setmp show_sorts true def_txt (c_ty, ""), Pretty.str
    1.55 +                 "imposes additional sort constraints on the declared type of the constant"]))
    1.56        | Plain =>
    1.57 -         (if not overloaded then
    1.58 -           warning (def_txt c_ty ^ "\nis strictly less general than the declared type (see "
    1.59 -             ^ quote (Sign.full_name sg name) ^ ")")
    1.60 +         (if not overloaded then warning (Pretty.string_of (Pretty.chunks
    1.61 +           [def_txt (c_ty, ""), Pretty.str ("is strictly less general than the declared type (see "
    1.62 +               ^ quote (Sign.full_name sg name) ^ ")")]))
    1.63           else (); (deps, def :: axms)))
    1.64    end;
    1.65