535 then increment-by-two, followed by increment-by-three. Again, the reverse |
535 then increment-by-two, followed by increment-by-three. Again, the reverse |
536 function composition allows you to read the code top-down. This combinator |
536 function composition allows you to read the code top-down. This combinator |
537 is often used for setup functions inside the |
537 is often used for setup functions inside the |
538 \isacommand{setup}-command. These functions have to be of type @{ML_type |
538 \isacommand{setup}-command. These functions have to be of type @{ML_type |
539 "theory -> theory"}. More than one such setup function can be composed with |
539 "theory -> theory"}. More than one such setup function can be composed with |
540 @{ML "#>"}. For example |
540 @{ML "#>"}.\footnote{give example} |
541 *} |
|
542 |
|
543 setup %gray {* let |
|
544 val (ival1, setup_ival1) = Attrib.config_int "ival1" (K 1) |
|
545 val (ival2, setup_ival2) = Attrib.config_int "ival2" (K 2) |
|
546 in |
|
547 setup_ival1 #> |
|
548 setup_ival2 |
|
549 end *} |
|
550 |
|
551 text {* |
|
552 after this the configuration values @{text ival1} and @{text ival2} are known |
|
553 in the current theory and can be manipulated by the user (for more information |
|
554 about configuration values see Section~\ref{sec:storing}, for more about setup |
|
555 functions see Section~\ref{sec:theories}). |
|
556 |
541 |
557 The remaining combinators we describe in this section add convenience for the |
542 The remaining combinators we describe in this section add convenience for the |
558 ``waterfall method'' of writing functions. The combinator @{ML_ind tap in |
543 ``waterfall method'' of writing functions. The combinator @{ML_ind tap in |
559 Basics} allows you to get hold of an intermediate result (to do some |
544 Basics} allows you to get hold of an intermediate result (to do some |
560 side-calculations for instance). The function |
545 side-calculations for instance). The function |
1306 user to control three values, say @{text bval} containing a boolean, @{text |
1291 user to control three values, say @{text bval} containing a boolean, @{text |
1307 ival} containing an integer and @{text sval} containing a string. These |
1292 ival} containing an integer and @{text sval} containing a string. These |
1308 values can be declared by |
1293 values can be declared by |
1309 *} |
1294 *} |
1310 |
1295 |
1311 ML{*val (bval, setup_bval) = Attrib.config_bool "bval" (K false) |
1296 ML{*val bval = Attrib.setup_config_bool @{binding "bval"} (K false) |
1312 val (ival, setup_ival) = Attrib.config_int "ival" (K 0) |
1297 val ival = Attrib.setup_config_int @{binding "ival"} (K 0) |
1313 val (sval, setup_sval) = Attrib.config_string "sval" (K "some string") *} |
1298 val sval = Attrib.setup_config_string @{binding "sval"} (K "some string") *} |
1314 |
1299 |
1315 text {* |
1300 text {* |
1316 where each value needs to be given a default. To enable these values on the |
1301 where each value needs to be given a default. |
1317 user-level, they need to be set up with |
|
1318 *} |
|
1319 |
|
1320 setup %gray {* |
|
1321 setup_bval #> |
|
1322 setup_ival #> |
|
1323 setup_sval |
|
1324 *} |
|
1325 |
|
1326 text {* |
|
1327 The user can now manipulate the values from the user-level of Isabelle |
1302 The user can now manipulate the values from the user-level of Isabelle |
1328 with the command |
1303 with the command |
1329 *} |
1304 *} |
1330 |
1305 |
1331 declare [[bval = true, ival = 3]] |
1306 declare [[bval = true, ival = 3]] |