src/Pure/config.ML
changeset 40291 012ed4426fda
parent 39163 4d701c0388c3
child 47814 53668571d300
     1.1 --- a/src/Pure/config.ML	Sat Oct 30 15:26:40 2010 +0200
     1.2 +++ b/src/Pure/config.ML	Sat Oct 30 16:33:58 2010 +0200
     1.3 @@ -6,13 +6,14 @@
     1.4  
     1.5  signature CONFIG =
     1.6  sig
     1.7 -  datatype value = Bool of bool | Int of int | String of string
     1.8 +  datatype value = Bool of bool | Int of int | Real of real | String of string
     1.9    val print_value: value -> string
    1.10    val print_type: value -> string
    1.11    type 'a T
    1.12    type raw = value T
    1.13    val bool: raw -> bool T
    1.14    val int: raw -> int T
    1.15 +  val real: raw -> real T
    1.16    val string: raw -> string T
    1.17    val get: Proof.context -> 'a T -> 'a
    1.18    val map: 'a T -> ('a -> 'a) -> Proof.context -> Proof.context
    1.19 @@ -37,19 +38,23 @@
    1.20  datatype value =
    1.21    Bool of bool |
    1.22    Int of int |
    1.23 +  Real of real |
    1.24    String of string;
    1.25  
    1.26  fun print_value (Bool true) = "true"
    1.27    | print_value (Bool false) = "false"
    1.28    | print_value (Int i) = signed_string_of_int i
    1.29 +  | print_value (Real x) = signed_string_of_real x
    1.30    | print_value (String s) = quote s;
    1.31  
    1.32  fun print_type (Bool _) = "bool"
    1.33    | print_type (Int _) = "int"
    1.34 +  | print_type (Real _) = "real"
    1.35    | print_type (String _) = "string";
    1.36  
    1.37  fun same_type (Bool _) (Bool _) = true
    1.38    | same_type (Int _) (Int _) = true
    1.39 +  | same_type (Real _) (Real _) = true
    1.40    | same_type (String _) (String _) = true
    1.41    | same_type _ _ = false;
    1.42  
    1.43 @@ -78,6 +83,7 @@
    1.44  
    1.45  val bool = coerce Bool (fn Bool b => b);
    1.46  val int = coerce Int (fn Int i => i);
    1.47 +val real = coerce Real (fn Real x => x);
    1.48  val string = coerce String (fn String s => s);
    1.49  
    1.50  fun get_generic context (Config {get_value, ...}) = get_value context;
    1.51 @@ -118,7 +124,8 @@
    1.52      fun map_value f (context as Context.Proof _) =
    1.53            let val context' = update_value f context in
    1.54              if global andalso
    1.55 -              get_value (Context.Theory (Context.theory_of context')) <> get_value context'
    1.56 +              print_value (get_value (Context.Theory (Context.theory_of context'))) <>
    1.57 +                print_value (get_value context')
    1.58              then (warning ("Ignoring local change of global option " ^ quote name); context)
    1.59              else context'
    1.60            end