equal
deleted
inserted
replaced
1 theory Config |
1 theory Config |
2 imports "../Base" |
2 imports "../Base" |
3 begin |
3 begin |
4 |
4 |
5 section {* Configuration Options\label{rec:config} *} |
5 section {* Configuration Options\label{rec:config} *} |
6 |
|
7 |
6 |
8 text {* |
7 text {* |
9 {\bf Problem:} |
8 {\bf Problem:} |
10 You would like to enhance your tool with options that can be changed |
9 You would like to enhance your tool with options that can be changed |
11 by the user without having to resort to the ML-level.\smallskip |
10 by the user without having to resort to the ML-level.\smallskip |
27 *} |
26 *} |
28 |
27 |
29 setup {* setup_bval *} |
28 setup {* setup_bval *} |
30 setup {* setup_ival *} |
29 setup {* setup_ival *} |
31 |
30 |
32 text {* or on the ML-level *} |
31 text {* or on the ML-level with *} |
33 |
32 |
34 ML{*setup_sval @{theory} *} |
33 ML{*setup_sval @{theory} *} |
35 |
34 |
36 text {* |
35 text {* |
37 The user can now manipulate the values from within Isabelle with the command |
36 The user can now manipulate the values from within Isabelle with the command |
55 *} |
54 *} |
56 |
55 |
57 setup {* Config.put_thy sval "bar" *} |
56 setup {* Config.put_thy sval "bar" *} |
58 |
57 |
59 text {* |
58 text {* |
60 Now the retrival of this value yields: |
59 Now the retrieval of this value yields: |
61 |
60 |
62 @{ML_response [display,gray] "Config.get @{context} sval" "\"bar\""} |
61 @{ML_response [display,gray] "Config.get @{context} sval" "\"bar\""} |
63 |
62 |
64 We can apply a function to a value using @{ML Config.map}. For example incrementing |
63 We can apply a function to a value using @{ML Config.map}. For example incrementing |
65 @{ML ival} can be done by: |
64 @{ML ival} can be done by: |
66 |
65 |
67 @{ML_response [display,gray] |
66 @{ML_response [display,gray] |
68 "let |
67 "let |
69 val ctxt = Config.map ival (fn i => i + 1) @{context} |
68 val ctxt' = Config.map ival (fn i => i + 1) @{context} |
70 in |
69 in |
71 Config.get ctxt ival |
70 Config.get ctxt' ival |
72 end" "4"} |
71 end" "4"} |
73 |
72 |
74 \begin{readmore} |
73 \begin{readmore} |
75 For more information see @{ML_file "Pure/Isar/attrib.ML"} and @{ML_file "Pure/config.ML"}. |
74 For more information see @{ML_file "Pure/Isar/attrib.ML"} and @{ML_file "Pure/config.ML"}. |
76 \end{readmore} |
75 \end{readmore} |
77 |
76 |
78 There are many good reasons to control parameters in this way. One is |
77 There are many good reasons to control parameters in this way. One is |
79 that it avoid global references, which cause many headaches with the |
78 that no global reference is needed, which would cause many headaches |
80 multithreaded execution of Isabelle. |
79 with the multithreaded execution of Isabelle. |
81 |
80 *} |
82 *} |
81 |
83 end |
82 end |