added name_of;
authorwenzelm
Thu Aug 02 12:06:28 2007 +0200 (2007-08-02)
changeset 24125454a0c895735
parent 24124 4399175e3014
child 24126 913e1fa904fb
added name_of;
src/Pure/config.ML
     1.1 --- a/src/Pure/config.ML	Thu Aug 02 12:06:27 2007 +0200
     1.2 +++ b/src/Pure/config.ML	Thu Aug 02 12:06:28 2007 +0200
     1.3 @@ -24,6 +24,7 @@
     1.4    val map_generic: 'a T -> ('a -> 'a) -> Context.generic -> Context.generic
     1.5    val put_generic: 'a T -> 'a -> Context.generic -> Context.generic
     1.6    val declare: bool -> string -> value -> value T
     1.7 +  val name_of: 'a T -> string
     1.8  end;
     1.9  
    1.10  structure Config: CONFIG =
    1.11 @@ -62,11 +63,14 @@
    1.12  (* abstract configuration options *)
    1.13  
    1.14  datatype 'a T = Config of
    1.15 - {get_value: Context.generic -> 'a,
    1.16 + {name: string,
    1.17 +  get_value: Context.generic -> 'a,
    1.18    map_value: ('a -> 'a) -> Context.generic -> Context.generic};
    1.19  
    1.20 -fun coerce make dest (Config {get_value, map_value}) =
    1.21 -  Config {get_value = dest o get_value, map_value = fn f => map_value (make o f o dest)};
    1.22 +fun coerce make dest (Config {name, get_value, map_value}) = Config
    1.23 + {name = name,
    1.24 +  get_value = dest o get_value,
    1.25 +  map_value = fn f => map_value (make o f o dest)};
    1.26  
    1.27  val bool = coerce Bool (fn Bool b => b);
    1.28  val int = coerce Int (fn Int i => i);
    1.29 @@ -110,7 +114,9 @@
    1.30              else context'
    1.31            end
    1.32        | map_value f context = modify_value f context;
    1.33 -  in Config {get_value = get_value, map_value = map_value} end;
    1.34 +  in Config {name = name, get_value = get_value, map_value = map_value} end;
    1.35 +
    1.36 +fun name_of (Config {name, ...}) = name;
    1.37  
    1.38  
    1.39  (*final declarations of this structure!*)