177 will cause that all tracing information is printed into the file @{text "foo.bar"}. |
184 will cause that all tracing information is printed into the file @{text "foo.bar"}. |
178 |
185 |
179 You can print out error messages with the function @{ML_ind error}; for |
186 You can print out error messages with the function @{ML_ind error}; for |
180 example: |
187 example: |
181 |
188 |
182 @{ML_response_fake [display,gray] "if 0=1 then true else (error \"foo\")" |
189 @{ML_response_fake [display,gray] |
|
190 "if 0=1 then true else (error \"foo\")" |
183 "Exception- ERROR \"foo\" raised |
191 "Exception- ERROR \"foo\" raised |
184 At command \"ML\"."} |
192 At command \"ML\"."} |
185 |
193 |
186 This function raises the exception @{text ERROR}, which will then |
194 This function raises the exception @{text ERROR}, which will then |
187 be displayed by the infrastructure. |
195 be displayed by the infrastructure. |
1216 ML{*val (bval, setup_bval) = Attrib.config_bool "bval" false |
1224 ML{*val (bval, setup_bval) = Attrib.config_bool "bval" false |
1217 val (ival, setup_ival) = Attrib.config_int "ival" 0 |
1225 val (ival, setup_ival) = Attrib.config_int "ival" 0 |
1218 val (sval, setup_sval) = Attrib.config_string "sval" "some string" *} |
1226 val (sval, setup_sval) = Attrib.config_string "sval" "some string" *} |
1219 |
1227 |
1220 text {* |
1228 text {* |
1221 where each value needs to be given a default. To enable these values, they need to |
1229 where each value needs to be given a default. To enable these values on the |
1222 be set up with |
1230 user-level, they need to be set up with |
1223 *} |
1231 *} |
1224 |
1232 |
1225 setup %gray {* |
1233 setup %gray {* |
1226 setup_bval #> |
1234 setup_bval #> |
1227 setup_ival |
1235 setup_ival #> |
|
1236 setup_sval |
1228 *} |
1237 *} |
1229 |
1238 |
1230 text {* |
1239 text {* |
1231 The user can now manipulate the values from the user-level of Isabelle |
1240 The user can now manipulate the values from the user-level of Isabelle |
1232 with the command |
1241 with the command |
1234 |
1243 |
1235 declare [[bval = true, ival = 3]] |
1244 declare [[bval = true, ival = 3]] |
1236 |
1245 |
1237 text {* |
1246 text {* |
1238 On the ML-level these values can be retrieved using the |
1247 On the ML-level these values can be retrieved using the |
1239 function @{ML Config.get}. |
1248 function @{ML_ind get in Config} from a proof context |
1240 |
1249 |
1241 @{ML_response [display,gray] "Config.get @{context} bval" "true"} |
1250 @{ML_response [display,gray] |
|
1251 "Config.get @{context} bval" |
|
1252 "true"} |
|
1253 |
|
1254 or from a theory using the function @{ML_ind get_thy in Config} |
|
1255 |
|
1256 @{ML_response [display,gray] |
|
1257 "Config.get_thy @{theory} bval" |
|
1258 "true"} |
|
1259 |
|
1260 It is also possible to manipulate the configuration values |
|
1261 from the ML-level with the function @{ML_ind put in Config} |
|
1262 or @{ML_ind put_thy in Config}. For example |
|
1263 |
|
1264 @{ML_response [display,gray] |
|
1265 "let |
|
1266 val ctxt = @{context} |
|
1267 val ctxt' = Config.put sval \"foo\" ctxt |
|
1268 in |
|
1269 (Config.get ctxt sval, Config.get ctxt' sval) |
|
1270 end" |
|
1271 "(\"some string\", \"foo\")"} |
1242 |
1272 |
1243 \begin{readmore} |
1273 \begin{readmore} |
1244 For more information about configuration values see |
1274 For more information about configuration values see |
1245 @{ML_file "Pure/Isar/attrib.ML"} and @{ML_file "Pure/config.ML"}. |
1275 the files @{ML_file "Pure/Isar/attrib.ML"} and |
|
1276 @{ML_file "Pure/config.ML"}. |
1246 \end{readmore} |
1277 \end{readmore} |
1247 |
|
1248 *} |
1278 *} |
1249 |
1279 |
1250 section {* Summary *} |
1280 section {* Summary *} |
1251 |
1281 |
1252 text {* |
1282 text {* |