doc-src/IsarImplementation/Thy/integration.thy
changeset 24173 4ba00a972eb8
parent 22095 07875394618e
child 26409 1ceabad5a2c8
equal deleted inserted replaced
24172:06e42cf7df4e 24173:4ba00a972eb8
   370 
   370 
   371 text %mlref {*
   371 text %mlref {*
   372   \begin{mldecls}
   372   \begin{mldecls}
   373   @{index_ML theory: "string -> theory"} \\
   373   @{index_ML theory: "string -> theory"} \\
   374   @{index_ML use_thy: "string -> unit"} \\
   374   @{index_ML use_thy: "string -> unit"} \\
   375   @{index_ML update_thy: "string -> unit"} \\
   375   @{index_ML use_thys: "string list -> unit"} \\
   376   @{index_ML touch_thy: "string -> unit"} \\
   376   @{index_ML touch_thy: "string -> unit"} \\
   377   @{index_ML remove_thy: "string -> unit"} \\[1ex]
   377   @{index_ML remove_thy: "string -> unit"} \\[1ex]
   378   @{index_ML ThyInfo.begin_theory}@{verbatim ": ... -> bool -> theory"} \\
   378   @{index_ML ThyInfo.begin_theory}@{verbatim ": ... -> bool -> theory"} \\
   379   @{index_ML ThyInfo.end_theory: "theory -> theory"} \\
   379   @{index_ML ThyInfo.end_theory: "theory -> theory"} \\
   380   @{index_ML ThyInfo.register_theory: "theory -> unit"} \\[1ex]
   380   @{index_ML ThyInfo.register_theory: "theory -> unit"} \\[1ex]
   386 
   386 
   387   \item @{ML theory}~@{text A} retrieves the theory value presently
   387   \item @{ML theory}~@{text A} retrieves the theory value presently
   388   associated with name @{text A}.  Note that the result might be
   388   associated with name @{text A}.  Note that the result might be
   389   outdated.
   389   outdated.
   390 
   390 
   391   \item @{ML use_thy}~@{text A} loads theory @{text A} if it is absent
   391   \item @{ML use_thy}~@{text A} ensures that theory @{text A} is fully
   392   or out-of-date.  It ensures that all parent theories are available
   392   up-to-date wrt.\ the external file store, reloading outdated
   393   as well, but does not reload them if older versions are already
   393   ancestors as required.
   394   present.
   394 
   395 
   395   \item @{ML use_thys} is similar to @{ML use_thy}, but handles
   396   \item @{ML update_thy} is similar to @{ML use_thy}, but ensures that
   396   several theories simultaneously.  Thus it acts like processing the
   397   theory @{text A} and all ancestors are fully up-to-date.
   397   import header of a theory, without performing the merge of the
       
   398   result, though.
   398 
   399 
   399   \item @{ML touch_thy}~@{text A} performs and @{text outdate} action
   400   \item @{ML touch_thy}~@{text A} performs and @{text outdate} action
   400   on theory @{text A} and all descendants.
   401   on theory @{text A} and all descendants.
   401 
   402 
   402   \item @{ML remove_thy}~@{text A} deletes theory @{text A} and all
   403   \item @{ML remove_thy}~@{text A} deletes theory @{text A} and all
   403   descendants from the theory database.
   404   descendants from the theory database.
   404 
   405 
   405   \item @{ML ThyInfo.begin_theory} is the basic operation behind a
   406   \item @{ML ThyInfo.begin_theory} is the basic operation behind a
   406   @{text \<THEORY>} header declaration.  The boolean argument
   407   @{text \<THEORY>} header declaration.  This is {\ML} functions is
   407   indicates the strictness of treating ancestors: for @{ML true} (as
       
   408   in interactive mode) like @{ML update_thy}, and for @{ML false} (as
       
   409   in batch mode) like @{ML use_thy}.  This is {\ML} functions is
       
   410   normally not invoked directly.
   408   normally not invoked directly.
   411 
   409 
   412   \item @{ML ThyInfo.end_theory} concludes the loading of a theory
   410   \item @{ML ThyInfo.end_theory} concludes the loading of a theory
   413   proper.  An attached theory {\ML} file may be still loaded later on.
   411   proper.  An attached theory {\ML} file may be still loaded later on.
   414   This is function is normally not invoked directly.
   412   This is function is normally not invoked directly.