1.1 --- a/src/Pure/General/name_space.ML	Tue May 03 22:26:16 2011 +0200
     1.2 +++ b/src/Pure/General/name_space.ML	Tue May 03 22:27:32 2011 +0200
     1.3 @@ -20,15 +20,15 @@
     1.4    val markup: T -> string -> Markup.T
     1.5    val is_concealed: T -> string -> bool
     1.6    val intern: T -> xstring -> string
     1.7 -  val long_names_default: bool Unsynchronized.ref
     1.8 -  val long_names_raw: Config.raw
     1.9 -  val long_names: bool Config.T
    1.10 -  val short_names_default: bool Unsynchronized.ref
    1.11 -  val short_names_raw: Config.raw
    1.12 -  val short_names: bool Config.T
    1.13 -  val unique_names_default: bool Unsynchronized.ref
    1.14 -  val unique_names_raw: Config.raw
    1.15 -  val unique_names: bool Config.T
    1.16 +  val names_long_default: bool Unsynchronized.ref
    1.17 +  val names_long_raw: Config.raw
    1.18 +  val names_long: bool Config.T
    1.19 +  val names_short_default: bool Unsynchronized.ref
    1.20 +  val names_short_raw: Config.raw
    1.21 +  val names_short: bool Config.T
    1.22 +  val names_unique_default: bool Unsynchronized.ref
    1.23 +  val names_unique_raw: Config.raw
    1.24 +  val names_unique: bool Config.T
    1.25    val extern: Proof.context -> T -> string -> xstring
    1.26    val hide: bool -> string -> T -> T
    1.27    val merge: T * T -> T
    1.28 @@ -161,33 +161,33 @@
    1.29  fun intern space xname = #1 (lookup space xname);
    1.30  
    1.31  
    1.32 -val long_names_default = Unsynchronized.ref false;
    1.33 -val long_names_raw = Config.declare "long_names" (fn _ => Config.Bool (! long_names_default));
    1.34 -val long_names = Config.bool long_names_raw;
    1.35 +val names_long_default = Unsynchronized.ref false;
    1.36 +val names_long_raw = Config.declare "names_long" (fn _ => Config.Bool (! names_long_default));
    1.37 +val names_long = Config.bool names_long_raw;
    1.38  
    1.39 -val short_names_default = Unsynchronized.ref false;
    1.40 -val short_names_raw = Config.declare "short_names" (fn _ => Config.Bool (! short_names_default));
    1.41 -val short_names = Config.bool short_names_raw;
    1.42 +val names_short_default = Unsynchronized.ref false;
    1.43 +val names_short_raw = Config.declare "names_short" (fn _ => Config.Bool (! names_short_default));
    1.44 +val names_short = Config.bool names_short_raw;
    1.45  
    1.46 -val unique_names_default = Unsynchronized.ref true;
    1.47 -val unique_names_raw = Config.declare "unique_names" (fn _ => Config.Bool (! unique_names_default));
    1.48 -val unique_names = Config.bool unique_names_raw;
    1.49 +val names_unique_default = Unsynchronized.ref true;
    1.50 +val names_unique_raw = Config.declare "names_unique" (fn _ => Config.Bool (! names_unique_default));
    1.51 +val names_unique = Config.bool names_unique_raw;
    1.52  
    1.53  fun extern ctxt space name =
    1.54    let
    1.55 -    val long_names = Config.get ctxt long_names;
    1.56 -    val short_names = Config.get ctxt short_names;
    1.57 -    val unique_names = Config.get ctxt unique_names;
    1.58 +    val names_long = Config.get ctxt names_long;
    1.59 +    val names_short = Config.get ctxt names_short;
    1.60 +    val names_unique = Config.get ctxt names_unique;
    1.61  
    1.62      fun valid require_unique xname =
    1.63        let val (name', is_unique) = lookup space xname
    1.64        in name = name' andalso (not require_unique orelse is_unique) end;
    1.65  
    1.66      fun ext [] = if valid false name then name else hidden name
    1.67 -      | ext (nm :: nms) = if valid unique_names nm then nm else ext nms;
    1.68 +      | ext (nm :: nms) = if valid names_unique nm then nm else ext nms;
    1.69    in
    1.70 -    if long_names then name
    1.71 -    else if short_names then Long_Name.base_name name
    1.72 +    if names_long then name
    1.73 +    else if names_short then Long_Name.base_name name
    1.74      else ext (get_accesses space name)
    1.75    end;
    1.76