map_value: dynamic type checking;
authorwenzelm
Fri, 27 Jul 2007 20:11:47 +0200
changeset 24004 8c962a9be9f2
parent 24003 da76d7e6435c
child 24005 2d473ed15491
map_value: dynamic type checking;
src/Pure/config.ML
--- a/src/Pure/config.ML	Fri Jul 27 16:31:16 2007 +0200
+++ b/src/Pure/config.ML	Fri Jul 27 20:11:47 2007 +0200
@@ -45,6 +45,19 @@
   | print_type (Int _) = "integer"
   | print_type (String _) = "string";
 
+fun same_type (Bool _) (Bool _) = true
+  | same_type (Int _) (Int _) = true
+  | same_type (String _) (String _) = true
+  | same_type _ _ = false;
+
+fun type_check f value =
+  let
+    val value' = f value;
+    val _ = same_type value value' orelse
+      error ("Ill-typed configuration option: " ^ print_type value ^
+        " expected,\nbut " ^ print_type value' ^ " was found");
+  in value' end;
+
 structure ConfigData = GenericDataFun
 (
   type T = value Inttab.table;
@@ -96,7 +109,7 @@
     val default_value = make default;
     fun get_value context =
       the_default default_value (Inttab.lookup (ConfigData.get context) id);
-    fun map_value f = ConfigData.map (Inttab.map_default (id, default_value) f);
+    fun map_value f = ConfigData.map (Inttab.map_default (id, default_value) (type_check f));
     val config_value = Config {get_value = get_value, map_value = map_value};
 
     val _ = CRITICAL (fn () =>