194 values, without any special precautions for multithreading. Apart |
194 values, without any special precautions for multithreading. Apart |
195 from the fully general functors for theory and proof data (see |
195 from the fully general functors for theory and proof data (see |
196 \secref{sec:context-data}) there are drop-in replacements that |
196 \secref{sec:context-data}) there are drop-in replacements that |
197 emulate primitive references for common cases of \emph{configuration |
197 emulate primitive references for common cases of \emph{configuration |
198 options} for type @{ML_type "bool"}/@{ML_type "int"}/@{ML_type |
198 options} for type @{ML_type "bool"}/@{ML_type "int"}/@{ML_type |
199 "string"} (see structure @{ML_struct ConfigOption}) and lists of |
199 "string"} (see structure @{ML_struct Config} and @{ML |
200 theorems (see functor @{ML_functor NamedThmsFun}). |
200 Attrib.config_bool} etc.), and lists of theorems (see functor |
|
201 @{ML_functor NamedThmsFun}). |
201 |
202 |
202 \item Keep components with local state information |
203 \item Keep components with local state information |
203 \emph{re-entrant}. Instead of poking initial values into (private) |
204 \emph{re-entrant}. Instead of poking initial values into (private) |
204 global references, create a new state record on each invocation, and |
205 global references, create a new state record on each invocation, and |
205 pass that through any auxiliary functions of the component. The |
206 pass that through any auxiliary functions of the component. The |