map_value: dynamic type checking;
authorwenzelm
Fri Jul 27 20:11:47 2007 +0200 (2007-07-27)
changeset 240048c962a9be9f2
parent 24003 da76d7e6435c
child 24005 2d473ed15491
map_value: dynamic type checking;
src/Pure/config.ML
     1.1 --- a/src/Pure/config.ML	Fri Jul 27 16:31:16 2007 +0200
     1.2 +++ b/src/Pure/config.ML	Fri Jul 27 20:11:47 2007 +0200
     1.3 @@ -45,6 +45,19 @@
     1.4    | print_type (Int _) = "integer"
     1.5    | print_type (String _) = "string";
     1.6  
     1.7 +fun same_type (Bool _) (Bool _) = true
     1.8 +  | same_type (Int _) (Int _) = true
     1.9 +  | same_type (String _) (String _) = true
    1.10 +  | same_type _ _ = false;
    1.11 +
    1.12 +fun type_check f value =
    1.13 +  let
    1.14 +    val value' = f value;
    1.15 +    val _ = same_type value value' orelse
    1.16 +      error ("Ill-typed configuration option: " ^ print_type value ^
    1.17 +        " expected,\nbut " ^ print_type value' ^ " was found");
    1.18 +  in value' end;
    1.19 +
    1.20  structure ConfigData = GenericDataFun
    1.21  (
    1.22    type T = value Inttab.table;
    1.23 @@ -96,7 +109,7 @@
    1.24      val default_value = make default;
    1.25      fun get_value context =
    1.26        the_default default_value (Inttab.lookup (ConfigData.get context) id);
    1.27 -    fun map_value f = ConfigData.map (Inttab.map_default (id, default_value) f);
    1.28 +    fun map_value f = ConfigData.map (Inttab.map_default (id, default_value) (type_check f));
    1.29      val config_value = Config {get_value = get_value, map_value = map_value};
    1.30  
    1.31      val _ = CRITICAL (fn () =>