equal
deleted
inserted
replaced
163 (*\\-----------------------------------------------------------------------------------------//*) |
163 (*\\-----------------------------------------------------------------------------------------//*) |
164 begin |
164 begin |
165 ML \<open> |
165 ML \<open> |
166 \<close> ML \<open> |
166 \<close> ML \<open> |
167 \<close> ML \<open> |
167 \<close> ML \<open> |
168 \<close> ML \<open> (*\<longrightarrow> ThyC*) |
|
169 fun get_theory_PIDE ctxt thy_id = |
|
170 let |
|
171 val known_thys = Theory.nodes_of (Proof_Context.theory_of ctxt) |
|
172 in |
|
173 (find_first (fn thy => Context.theory_name thy = thy_id) known_thys |
|
174 |> the) |
|
175 handle Option.Option => raise ERROR ("get_theory fails with " ^ quote thy_id) |
|
176 end |
|
177 \<close> ML \<open> |
|
178 get_theory_PIDE: Proof.context -> ThyC.id -> theory |
|
179 \<close> ML \<open> |
|
180 the |
|
181 \<close> ML \<open> |
168 \<close> ML \<open> |
182 \<close> ML \<open> |
169 \<close> ML \<open> |
183 \<close> |
170 \<close> |
184 |
171 |
185 text \<open> |
172 text \<open> |