tuned error message;
authorwenzelm
Mon, 05 Sep 2022 11:09:35 +0200
changeset 76058 d45a45eb1aee
parent 76051 854e9223767f
child 76059 7cf72240cdd4
tuned error message;
src/Pure/config.ML
--- a/src/Pure/config.ML	Sat Sep 03 23:10:38 2022 +0200
+++ b/src/Pure/config.ML	Mon Sep 05 11:09:35 2022 +0200
@@ -164,7 +164,7 @@
 
 fun declare_option (name, pos) =
   let
-    val typ = Options.default_typ name;
+    val typ = Options.default_typ name handle ERROR msg => error (msg ^ Position.here pos);
     val default =
       if typ = Options.boolT then fn _ => Bool (Options.default_bool name)
       else if typ = Options.intT then fn _ => Int (Options.default_int name)