equal
deleted
inserted
replaced
73 val ctxt = Config.map ival (fn i => i + 1) @{context} |
73 val ctxt = Config.map ival (fn i => i + 1) @{context} |
74 in |
74 in |
75 Config.get ctxt ival |
75 Config.get ctxt ival |
76 end" "4"} |
76 end" "4"} |
77 |
77 |
78 \begin{readmore} |
78 \begin{readmore} |
79 For more information see @{ML_file "Pure/Isar/attrib.ML"} and @{ML_file "Pure/config.ML"}. |
79 For more information see @{ML_file "Pure/Isar/attrib.ML"} and @{ML_file "Pure/config.ML"}. |
80 \end{readmore} |
80 \end{readmore} |
81 |
81 |
82 *} |
82 There are many good reasons to control parameters in this way. One is |
83 |
83 that it avoid global references, which cause many headaches with the |
84 |
84 multithreaded execution of Isabelle. |
85 text {* |
85 |
86 |
|
87 Note: Avoid to use references for this purpose! |
|
88 *} |
86 *} |
89 |
87 |
90 end |
88 end |