equal
deleted
inserted
replaced
148 as the relative location to refer to other files from that theory. |
148 as the relative location to refer to other files from that theory. |
149 \<close> |
149 \<close> |
150 |
150 |
151 text %mlref \<open> |
151 text %mlref \<open> |
152 \begin{mldecls} |
152 \begin{mldecls} |
153 @{define_ML use_thy: "string -> unit"} \\ |
|
154 @{define_ML Thy_Info.get_theory: "string -> theory"} \\ |
153 @{define_ML Thy_Info.get_theory: "string -> theory"} \\ |
155 @{define_ML Thy_Info.remove_thy: "string -> unit"} \\ |
154 @{define_ML Thy_Info.remove_thy: "string -> unit"} \\ |
156 \end{mldecls} |
155 \end{mldecls} |
157 |
|
158 \<^descr> \<^ML>\<open>use_thy\<close>~\<open>A\<close> ensures that theory \<open>A\<close> is fully up-to-date wrt.\ the |
|
159 external file store; outdated ancestors are reloaded on demand. |
|
160 |
156 |
161 \<^descr> \<^ML>\<open>Thy_Info.get_theory\<close>~\<open>A\<close> retrieves the theory value presently |
157 \<^descr> \<^ML>\<open>Thy_Info.get_theory\<close>~\<open>A\<close> retrieves the theory value presently |
162 associated with name \<open>A\<close>. Note that the result might be outdated wrt.\ the |
158 associated with name \<open>A\<close>. Note that the result might be outdated wrt.\ the |
163 file-system content. |
159 file-system content. |
164 |
160 |