equal
deleted
inserted
replaced
1376 |
1376 |
1377 @{ML_response [display,gray] |
1377 @{ML_response [display,gray] |
1378 "Config.get @{context} bval" |
1378 "Config.get @{context} bval" |
1379 "true"} |
1379 "true"} |
1380 |
1380 |
1381 or directly from a theory using the function @{ML_ind get_thy in Config} |
1381 or directly from a theory using the function @{ML_ind get_global in Config} |
1382 |
1382 |
1383 @{ML_response [display,gray] |
1383 @{ML_response [display,gray] |
1384 "Config.get_thy @{theory} bval" |
1384 "Config.get_global @{theory} bval" |
1385 "true"} |
1385 "true"} |
1386 |
1386 |
1387 It is also possible to manipulate the configuration values |
1387 It is also possible to manipulate the configuration values |
1388 from the ML-level with the functions @{ML_ind put in Config} |
1388 from the ML-level with the functions @{ML_ind put in Config} |
1389 and @{ML_ind put_thy in Config}. For example |
1389 and @{ML_ind put_global in Config}. For example |
1390 |
1390 |
1391 @{ML_response [display,gray] |
1391 @{ML_response [display,gray] |
1392 "let |
1392 "let |
1393 val ctxt = @{context} |
1393 val ctxt = @{context} |
1394 val ctxt' = Config.put sval \"foo\" ctxt |
1394 val ctxt' = Config.put sval \"foo\" ctxt |