35 issuing @{command end} to get back to the empty toplevel. |
35 issuing @{command end} to get back to the empty toplevel. |
36 \<close> |
36 \<close> |
37 |
37 |
38 text %mlref \<open> |
38 text %mlref \<open> |
39 \begin{mldecls} |
39 \begin{mldecls} |
40 @{index_ML_type Toplevel.state} \\ |
40 @{define_ML_type Toplevel.state} \\ |
41 @{index_ML_exception Toplevel.UNDEF} \\ |
41 @{define_ML_exception Toplevel.UNDEF} \\ |
42 @{index_ML Toplevel.is_toplevel: "Toplevel.state -> bool"} \\ |
42 @{define_ML Toplevel.is_toplevel: "Toplevel.state -> bool"} \\ |
43 @{index_ML Toplevel.theory_of: "Toplevel.state -> theory"} \\ |
43 @{define_ML Toplevel.theory_of: "Toplevel.state -> theory"} \\ |
44 @{index_ML Toplevel.proof_of: "Toplevel.state -> Proof.state"} \\ |
44 @{define_ML Toplevel.proof_of: "Toplevel.state -> Proof.state"} \\ |
45 \end{mldecls} |
45 \end{mldecls} |
46 |
46 |
47 \<^descr> Type \<^ML_type>\<open>Toplevel.state\<close> represents Isar toplevel states, which are |
47 \<^descr> Type \<^ML_type>\<open>Toplevel.state\<close> represents Isar toplevel states, which are |
48 normally manipulated through the concept of toplevel transitions only |
48 normally manipulated through the concept of toplevel transitions only |
49 (\secref{sec:toplevel-transition}). |
49 (\secref{sec:toplevel-transition}). |
93 adjoins actual operations on a theory or proof state. |
93 adjoins actual operations on a theory or proof state. |
94 \<close> |
94 \<close> |
95 |
95 |
96 text %mlref \<open> |
96 text %mlref \<open> |
97 \begin{mldecls} |
97 \begin{mldecls} |
98 @{index_ML Toplevel.keep: "(Toplevel.state -> unit) -> |
98 @{define_ML Toplevel.keep: "(Toplevel.state -> unit) -> |
99 Toplevel.transition -> Toplevel.transition"} \\ |
99 Toplevel.transition -> Toplevel.transition"} \\ |
100 @{index_ML Toplevel.theory: "(theory -> theory) -> |
100 @{define_ML Toplevel.theory: "(theory -> theory) -> |
101 Toplevel.transition -> Toplevel.transition"} \\ |
101 Toplevel.transition -> Toplevel.transition"} \\ |
102 @{index_ML Toplevel.theory_to_proof: "(theory -> Proof.state) -> |
102 @{define_ML Toplevel.theory_to_proof: "(theory -> Proof.state) -> |
103 Toplevel.transition -> Toplevel.transition"} \\ |
103 Toplevel.transition -> Toplevel.transition"} \\ |
104 @{index_ML Toplevel.proof: "(Proof.state -> Proof.state) -> |
104 @{define_ML Toplevel.proof: "(Proof.state -> Proof.state) -> |
105 Toplevel.transition -> Toplevel.transition"} \\ |
105 Toplevel.transition -> Toplevel.transition"} \\ |
106 @{index_ML Toplevel.proofs: "(Proof.state -> Proof.state Seq.result Seq.seq) -> |
106 @{define_ML Toplevel.proofs: "(Proof.state -> Proof.state Seq.result Seq.seq) -> |
107 Toplevel.transition -> Toplevel.transition"} \\ |
107 Toplevel.transition -> Toplevel.transition"} \\ |
108 @{index_ML Toplevel.end_proof: "(bool -> Proof.state -> Proof.context) -> |
108 @{define_ML Toplevel.end_proof: "(bool -> Proof.state -> Proof.context) -> |
109 Toplevel.transition -> Toplevel.transition"} \\ |
109 Toplevel.transition -> Toplevel.transition"} \\ |
110 \end{mldecls} |
110 \end{mldecls} |
111 |
111 |
112 \<^descr> \<^ML>\<open>Toplevel.keep\<close>~\<open>tr\<close> adjoins a diagnostic function. |
112 \<^descr> \<^ML>\<open>Toplevel.keep\<close>~\<open>tr\<close> adjoins a diagnostic function. |
113 |
113 |
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 @{index_ML use_thy: "string -> unit"} \\ |
153 @{define_ML use_thy: "string -> unit"} \\ |
154 @{index_ML Thy_Info.get_theory: "string -> theory"} \\ |
154 @{define_ML Thy_Info.get_theory: "string -> theory"} \\ |
155 @{index_ML Thy_Info.remove_thy: "string -> unit"} \\ |
155 @{define_ML Thy_Info.remove_thy: "string -> unit"} \\ |
156 @{index_ML Thy_Info.register_thy: "theory -> unit"} \\ |
156 @{define_ML Thy_Info.register_thy: "theory -> unit"} \\ |
157 \end{mldecls} |
157 \end{mldecls} |
158 |
158 |
159 \<^descr> \<^ML>\<open>use_thy\<close>~\<open>A\<close> ensures that theory \<open>A\<close> is fully up-to-date wrt.\ the |
159 \<^descr> \<^ML>\<open>use_thy\<close>~\<open>A\<close> ensures that theory \<open>A\<close> is fully up-to-date wrt.\ the |
160 external file store; outdated ancestors are reloaded on demand. |
160 external file store; outdated ancestors are reloaded on demand. |
161 |
161 |