more informative markup for fixed variables (via name space entry);
authorwenzelm
Wed Apr 27 20:37:56 2011 +0200 (2011-04-27)
changeset 4249301430341fc79
parent 42492 83c57d850049
child 42494 eef1a23c9077
more informative markup for fixed variables (via name space entry);
uniform markup for undeclared entities;
tuned;
src/Pure/General/name_space.ML
src/Pure/Syntax/syntax_phases.ML
src/Pure/variable.ML
     1.1 --- a/src/Pure/General/name_space.ML	Wed Apr 27 20:28:27 2011 +0200
     1.2 +++ b/src/Pure/General/name_space.ML	Wed Apr 27 20:37:56 2011 +0200
     1.3 @@ -130,7 +130,7 @@
     1.4  
     1.5  fun markup (Name_Space {kind, entries, ...}) name =
     1.6    (case Symtab.lookup entries name of
     1.7 -    NONE => Markup.malformed
     1.8 +    NONE => Markup.hilite
     1.9    | SOME (_, entry) => entry_markup false kind (name, entry));
    1.10  
    1.11  fun is_concealed space name = #concealed (the_entry space name);
     2.1 --- a/src/Pure/Syntax/syntax_phases.ML	Wed Apr 27 20:28:27 2011 +0200
     2.2 +++ b/src/Pure/Syntax/syntax_phases.ML	Wed Apr 27 20:37:56 2011 +0200
     2.3 @@ -31,8 +31,9 @@
     2.4  
     2.5  fun markup_free ctxt x =
     2.6    [if can Name.dest_skolem x then Markup.skolem else Markup.free] @
     2.7 -  (if not (Variable.is_body ctxt) orelse Variable.is_fixed ctxt x then []
     2.8 -   else [Markup.hilite]);
     2.9 +  (if Variable.is_body ctxt orelse Variable.is_fixed ctxt x
    2.10 +   then [Variable.markup_fixed ctxt x]
    2.11 +   else []);
    2.12  
    2.13  fun markup_var xi = [Markup.name (Term.string_of_vname xi) Markup.var];
    2.14  
     3.1 --- a/src/Pure/variable.ML	Wed Apr 27 20:28:27 2011 +0200
     3.2 +++ b/src/Pure/variable.ML	Wed Apr 27 20:37:56 2011 +0200
     3.3 @@ -32,10 +32,11 @@
     3.4    val lookup_const: Proof.context -> string -> string option
     3.5    val is_const: Proof.context -> string -> bool
     3.6    val declare_const: string * string -> Proof.context -> Proof.context
     3.7 -  val fixed_ord: Proof.context -> string * string -> order
     3.8    val is_fixed: Proof.context -> string -> bool
     3.9    val newly_fixed: Proof.context -> Proof.context -> string -> bool
    3.10 +  val fixed_ord: Proof.context -> string * string -> order
    3.11    val intern_fixed: Proof.context -> string -> string
    3.12 +  val markup_fixed: Proof.context -> string -> Markup.T
    3.13    val lookup_fixed: Proof.context -> string -> string option
    3.14    val revert_fixed: Proof.context -> string -> string
    3.15    val add_fixed_names: Proof.context -> term -> string list -> string list
    3.16 @@ -154,6 +155,7 @@
    3.17  
    3.18  val names_of = #names o rep_data;
    3.19  val fixes_of = #fixes o rep_data;
    3.20 +val fixes_space = #1 o fixes_of;
    3.21  val binds_of = #binds o rep_data;
    3.22  val type_occs_of = #type_occs o rep_data;
    3.23  val maxidx_of = #maxidx o rep_data;
    3.24 @@ -289,12 +291,12 @@
    3.25  
    3.26  (* specialized name space *)
    3.27  
    3.28 -fun fixed_ord ctxt = Name_Space.entry_ord (#1 (fixes_of ctxt));
    3.29 -
    3.30 -fun is_fixed ctxt x = can (Name_Space.the_entry (#1 (fixes_of ctxt))) x;
    3.31 +fun is_fixed ctxt x = can (Name_Space.the_entry (fixes_space ctxt)) x;
    3.32  fun newly_fixed inner outer x = is_fixed inner x andalso not (is_fixed outer x);
    3.33  
    3.34 -fun intern_fixed ctxt = Name_Space.intern (#1 (fixes_of ctxt));
    3.35 +val fixed_ord = Name_Space.entry_ord o fixes_space;
    3.36 +val intern_fixed = Name_Space.intern o fixes_space;
    3.37 +val markup_fixed = Name_Space.markup o fixes_space;
    3.38  
    3.39  fun lookup_fixed ctxt x =
    3.40    let val x' = intern_fixed ctxt x