equal
deleted
inserted
replaced
197 val _ = Theory.setup |
197 val _ = Theory.setup |
198 (ML_Antiquotation.inline_embedded \<^binding>\<open>locale\<close> |
198 (ML_Antiquotation.inline_embedded \<^binding>\<open>locale\<close> |
199 (Args.theory -- Scan.lift Parse.embedded_position >> |
199 (Args.theory -- Scan.lift Parse.embedded_position >> |
200 (ML_Syntax.print_string o uncurry check))); |
200 (ML_Syntax.print_string o uncurry check))); |
201 |
201 |
202 fun extern thy = Name_Space.extern (Proof_Context.init_global thy) (locale_space thy); |
202 fun extern thy = |
|
203 Name_Space.extern_generic (Context.Theory thy) (locale_space thy); |
203 |
204 |
204 fun markup_extern ctxt = |
205 fun markup_extern ctxt = |
205 Name_Space.markup_extern ctxt (locale_space (Proof_Context.theory_of ctxt)); |
206 Name_Space.markup_extern ctxt (locale_space (Proof_Context.theory_of ctxt)); |
206 |
207 |
207 fun markup_name ctxt name = markup_extern ctxt name |-> Markup.markup; |
208 fun markup_name ctxt name = markup_extern ctxt name |-> Markup.markup; |