tuned message;
authorwenzelm
Wed Apr 01 11:55:23 2015 +0200 (2015-04-01)
changeset 5988930eef3e45bd0
parent 59888 27e4d0ab0948
child 59890 01aff5aa081d
tuned message;
src/Pure/General/name_space.ML
     1.1 --- a/src/Pure/General/name_space.ML	Wed Apr 01 10:35:43 2015 +0200
     1.2 +++ b/src/Pure/General/name_space.ML	Wed Apr 01 11:55:23 2015 +0200
     1.3 @@ -12,10 +12,10 @@
     1.4    type T
     1.5    val empty: string -> T
     1.6    val kind_of: T -> string
     1.7 +  val markup: T -> string -> Markup.T
     1.8    val the_entry: T -> string ->
     1.9      {concealed: bool, group: serial option, theory_name: string, pos: Position.T, serial: serial}
    1.10    val entry_ord: T -> string * string -> order
    1.11 -  val markup: T -> string -> Markup.T
    1.12    val is_concealed: T -> string -> bool
    1.13    val intern: T -> xstring -> string
    1.14    val names_long_raw: Config.raw
    1.15 @@ -109,8 +109,6 @@
    1.16    error ("Duplicate " ^ plain_words kind ^ " declaration " ^
    1.17      print_entry_ref kind entry1 ^ " vs. " ^ print_entry_ref kind entry2 ^ Position.here pos);
    1.18  
    1.19 -fun undefined kind name = "Undefined " ^ plain_words kind ^ ": " ^ quote name;
    1.20 -
    1.21  
    1.22  (* internal names *)
    1.23  
    1.24 @@ -151,18 +149,29 @@
    1.25  
    1.26  fun kind_of (Name_Space {kind, ...}) = kind;
    1.27  
    1.28 -fun the_entry (Name_Space {kind, entries, ...}) name =
    1.29 -  (case Change_Table.lookup entries name of
    1.30 -    NONE => error (undefined kind name)
    1.31 -  | SOME (_, entry) => entry);
    1.32 -
    1.33 -fun entry_ord space = int_ord o apply2 (#serial o the_entry space);
    1.34 -
    1.35  fun markup (Name_Space {kind, entries, ...}) name =
    1.36    (case Change_Table.lookup entries name of
    1.37      NONE => Markup.intensify
    1.38    | SOME (_, entry) => entry_markup false kind (name, entry));
    1.39  
    1.40 +fun undefined (space as Name_Space {kind, entries, ...}) bad =
    1.41 +  let
    1.42 +    val (prfx, sfx) =
    1.43 +      (case Long_Name.dest_hidden bad of
    1.44 +        SOME name =>
    1.45 +          if Change_Table.defined entries name
    1.46 +          then ("Inaccessible", Markup.markup (markup space name) (quote name))
    1.47 +          else ("Undefined", quote name)
    1.48 +      | NONE => ("Undefined", quote bad));
    1.49 +  in prfx ^ " " ^ plain_words kind ^ ": " ^ sfx end;
    1.50 +
    1.51 +fun the_entry (space as Name_Space {entries, ...}) name =
    1.52 +  (case Change_Table.lookup entries name of
    1.53 +    NONE => error (undefined space name)
    1.54 +  | SOME (_, entry) => entry);
    1.55 +
    1.56 +fun entry_ord space = int_ord o apply2 (#serial o the_entry space);
    1.57 +
    1.58  fun is_concealed space name = #concealed (the_entry space name);
    1.59  
    1.60  
    1.61 @@ -391,7 +400,7 @@
    1.62  fun hide fully name space =
    1.63    space |> map_name_space (fn (kind, internals, entries) =>
    1.64      let
    1.65 -      val _ = Change_Table.defined entries name orelse error (undefined kind name);
    1.66 +      val _ = the_entry space name;
    1.67        val names = valid_accesses space name;
    1.68        val internals' = internals
    1.69          |> hide_name name
    1.70 @@ -406,7 +415,7 @@
    1.71  fun alias naming binding name space =
    1.72    space |> map_name_space (fn (kind, internals, entries) =>
    1.73      let
    1.74 -      val _ = Change_Table.defined entries name orelse error (undefined kind name);
    1.75 +      val _ = the_entry space name;
    1.76        val (accs, accs') = accesses naming binding;
    1.77        val internals' = internals |> fold (add_name name) accs;
    1.78        val entries' = entries
    1.79 @@ -502,7 +511,7 @@
    1.80          let
    1.81            val completions = map (fn pos => completion context space (xname, pos)) ps;
    1.82          in
    1.83 -          error (undefined (kind_of space) name ^ Position.here_list ps ^
    1.84 +          error (undefined space name ^ Position.here_list ps ^
    1.85              Markup.markup_report (implode (map Completion.reported_text completions)))
    1.86          end)
    1.87    end;
    1.88 @@ -520,7 +529,7 @@
    1.89  fun get table name =
    1.90    (case lookup_key table name of
    1.91      SOME (_, x) => x
    1.92 -  | NONE => error (undefined (kind_of (space_of_table table)) name));
    1.93 +  | NONE => error (undefined (space_of_table table) name));
    1.94  
    1.95  fun define context strict (binding, x) (Table (space, tab)) =
    1.96    let