366 text %mlref {* |
366 text %mlref {* |
367 \begin{mldecls} |
367 \begin{mldecls} |
368 @{index_ML theory: "string -> theory"} \\ |
368 @{index_ML theory: "string -> theory"} \\ |
369 @{index_ML use_thy: "string -> unit"} \\ |
369 @{index_ML use_thy: "string -> unit"} \\ |
370 @{index_ML use_thys: "string list -> unit"} \\ |
370 @{index_ML use_thys: "string list -> unit"} \\ |
371 @{index_ML ThyInfo.touch_thy: "string -> unit"} \\ |
371 @{index_ML Thy_Info.touch_thy: "string -> unit"} \\ |
372 @{index_ML ThyInfo.remove_thy: "string -> unit"} \\[1ex] |
372 @{index_ML Thy_Info.remove_thy: "string -> unit"} \\[1ex] |
373 @{index_ML ThyInfo.begin_theory}@{verbatim ": ... -> bool -> theory"} \\ |
373 @{index_ML Thy_Info.begin_theory}@{verbatim ": ... -> bool -> theory"} \\ |
374 @{index_ML ThyInfo.end_theory: "theory -> unit"} \\ |
374 @{index_ML Thy_Info.end_theory: "theory -> unit"} \\ |
375 @{index_ML ThyInfo.register_theory: "theory -> unit"} \\[1ex] |
375 @{index_ML Thy_Info.register_theory: "theory -> unit"} \\[1ex] |
376 @{verbatim "datatype action = Update | Outdate | Remove"} \\ |
376 @{verbatim "datatype action = Update | Outdate | Remove"} \\ |
377 @{index_ML ThyInfo.add_hook: "(ThyInfo.action -> string -> unit) -> unit"} \\ |
377 @{index_ML Thy_Info.add_hook: "(Thy_Info.action -> string -> unit) -> unit"} \\ |
378 \end{mldecls} |
378 \end{mldecls} |
379 |
379 |
380 \begin{description} |
380 \begin{description} |
381 |
381 |
382 \item @{ML theory}~@{text A} retrieves the theory value presently |
382 \item @{ML theory}~@{text A} retrieves the theory value presently |
393 import header of a theory, without performing the merge of the |
393 import header of a theory, without performing the merge of the |
394 result. By loading a whole sub-graph of theories like that, the |
394 result. By loading a whole sub-graph of theories like that, the |
395 intrinsic parallelism can be exploited by the system, to speedup |
395 intrinsic parallelism can be exploited by the system, to speedup |
396 loading. |
396 loading. |
397 |
397 |
398 \item @{ML ThyInfo.touch_thy}~@{text A} performs and @{text outdate} action |
398 \item @{ML Thy_Info.touch_thy}~@{text A} performs and @{text outdate} action |
399 on theory @{text A} and all descendants. |
399 on theory @{text A} and all descendants. |
400 |
400 |
401 \item @{ML ThyInfo.remove_thy}~@{text A} deletes theory @{text A} and all |
401 \item @{ML Thy_Info.remove_thy}~@{text A} deletes theory @{text A} and all |
402 descendants from the theory database. |
402 descendants from the theory database. |
403 |
403 |
404 \item @{ML ThyInfo.begin_theory} is the basic operation behind a |
404 \item @{ML Thy_Info.begin_theory} is the basic operation behind a |
405 @{text \<THEORY>} header declaration. This {\ML} function is |
405 @{text \<THEORY>} header declaration. This {\ML} function is |
406 normally not invoked directly. |
406 normally not invoked directly. |
407 |
407 |
408 \item @{ML ThyInfo.end_theory} concludes the loading of a theory |
408 \item @{ML Thy_Info.end_theory} concludes the loading of a theory |
409 proper and stores the result in the theory database. |
409 proper and stores the result in the theory database. |
410 |
410 |
411 \item @{ML ThyInfo.register_theory}~@{text "text thy"} registers an |
411 \item @{ML Thy_Info.register_theory}~@{text "text thy"} registers an |
412 existing theory value with the theory loader database. There is no |
412 existing theory value with the theory loader database. There is no |
413 management of associated sources. |
413 management of associated sources. |
414 |
414 |
415 \item @{ML "ThyInfo.add_hook"}~@{text f} registers function @{text |
415 \item @{ML "Thy_Info.add_hook"}~@{text f} registers function @{text |
416 f} as a hook for theory database actions. The function will be |
416 f} as a hook for theory database actions. The function will be |
417 invoked with the action and theory name being involved; thus derived |
417 invoked with the action and theory name being involved; thus derived |
418 actions may be performed in associated system components, e.g.\ |
418 actions may be performed in associated system components, e.g.\ |
419 maintaining the state of an editor for the theory sources. |
419 maintaining the state of an editor for the theory sources. |
420 |
420 |