# HG changeset patch
# User wenzelm
# Date 1185559907 -7200
# Node ID 8c962a9be9f2fe7ce688d08ede94d787e3728d0f
# Parent  da76d7e6435c8a6bfeffc6b6cbbf6432a4abcdcd
map_value: dynamic type checking;

diff -r da76d7e6435c -r 8c962a9be9f2 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 () =>