src/Pure/config.ML
changeset 39163 4d701c0388c3
parent 39116 f14735a88886
child 40291 012ed4426fda
     1.1 --- a/src/Pure/config.ML	Mon Sep 06 19:23:54 2010 +0200
     1.2 +++ b/src/Pure/config.ML	Mon Sep 06 21:33:19 2010 +0200
     1.3 @@ -10,9 +10,10 @@
     1.4    val print_value: value -> string
     1.5    val print_type: value -> string
     1.6    type 'a T
     1.7 -  val bool: value T -> bool T
     1.8 -  val int: value T -> int T
     1.9 -  val string: value T -> string T
    1.10 +  type raw = value T
    1.11 +  val bool: raw -> bool T
    1.12 +  val int: raw -> int T
    1.13 +  val string: raw -> string T
    1.14    val get: Proof.context -> 'a T -> 'a
    1.15    val map: 'a T -> ('a -> 'a) -> Proof.context -> Proof.context
    1.16    val put: 'a T -> 'a -> Proof.context -> Proof.context
    1.17 @@ -22,9 +23,9 @@
    1.18    val get_generic: Context.generic -> 'a T -> 'a
    1.19    val map_generic: 'a T -> ('a -> 'a) -> Context.generic -> Context.generic
    1.20    val put_generic: 'a T -> 'a -> Context.generic -> Context.generic
    1.21 -  val declare_generic: {global: bool} -> string -> (Context.generic -> value) -> value T
    1.22 -  val declare_global: string -> (Context.generic -> value) -> value T
    1.23 -  val declare: string -> (Context.generic -> value) -> value T
    1.24 +  val declare_generic: {global: bool} -> string -> (Context.generic -> value) -> raw
    1.25 +  val declare_global: string -> (Context.generic -> value) -> raw
    1.26 +  val declare: string -> (Context.generic -> value) -> raw
    1.27    val name_of: 'a T -> string
    1.28  end;
    1.29  
    1.30 @@ -68,6 +69,8 @@
    1.31    get_value: Context.generic -> 'a,
    1.32    map_value: ('a -> 'a) -> Context.generic -> Context.generic};
    1.33  
    1.34 +type raw = value T;
    1.35 +
    1.36  fun coerce make dest (Config {name, get_value, map_value}) = Config
    1.37   {name = name,
    1.38    get_value = dest o get_value,