equal
deleted
inserted
replaced
567 "theory -> theory"}. More than one such setup function can be composed with |
567 "theory -> theory"}. More than one such setup function can be composed with |
568 @{ML "#>"}. For example |
568 @{ML "#>"}. For example |
569 *} |
569 *} |
570 |
570 |
571 setup %gray {* let |
571 setup %gray {* let |
572 val (ival1, setup_ival1) = Attrib.config_int "ival1" 1 |
572 val (ival1, setup_ival1) = Attrib.config_int "ival1" (K 1) |
573 val (ival2, setup_ival2) = Attrib.config_int "ival2" 2 |
573 val (ival2, setup_ival2) = Attrib.config_int "ival2" (K 2) |
574 in |
574 in |
575 setup_ival1 #> |
575 setup_ival1 #> |
576 setup_ival2 |
576 setup_ival2 |
577 end *} |
577 end *} |
578 |
578 |
1329 user to control three values, say @{text bval} containing a boolean, @{text |
1329 user to control three values, say @{text bval} containing a boolean, @{text |
1330 ival} containing an integer and @{text sval} containing a string. These |
1330 ival} containing an integer and @{text sval} containing a string. These |
1331 values can be declared by |
1331 values can be declared by |
1332 *} |
1332 *} |
1333 |
1333 |
1334 ML{*val (bval, setup_bval) = Attrib.config_bool "bval" false |
1334 ML{*val (bval, setup_bval) = Attrib.config_bool "bval" (K false) |
1335 val (ival, setup_ival) = Attrib.config_int "ival" 0 |
1335 val (ival, setup_ival) = Attrib.config_int "ival" (K 0) |
1336 val (sval, setup_sval) = Attrib.config_string "sval" "some string" *} |
1336 val (sval, setup_sval) = Attrib.config_string "sval" (K "some string") *} |
1337 |
1337 |
1338 text {* |
1338 text {* |
1339 where each value needs to be given a default. To enable these values on the |
1339 where each value needs to be given a default. To enable these values on the |
1340 user-level, they need to be set up with |
1340 user-level, they need to be set up with |
1341 *} |
1341 *} |