equal
deleted
inserted
replaced
185 val intern = Name_Space.intern o locale_space; |
185 val intern = Name_Space.intern o locale_space; |
186 fun check thy = #1 o Name_Space.check (Context.Theory thy) (Locales.get thy); |
186 fun check thy = #1 o Name_Space.check (Context.Theory thy) (Locales.get thy); |
187 |
187 |
188 val _ = Theory.setup |
188 val _ = Theory.setup |
189 (ML_Antiquotation.inline_embedded \<^binding>\<open>locale\<close> |
189 (ML_Antiquotation.inline_embedded \<^binding>\<open>locale\<close> |
190 (Args.theory -- Scan.lift Args.embedded_position >> |
190 (Args.theory -- Scan.lift Parse.embedded_position >> |
191 (ML_Syntax.print_string o uncurry check))); |
191 (ML_Syntax.print_string o uncurry check))); |
192 |
192 |
193 fun extern thy = Name_Space.extern (Proof_Context.init_global thy) (locale_space thy); |
193 fun extern thy = Name_Space.extern (Proof_Context.init_global thy) (locale_space thy); |
194 |
194 |
195 fun markup_extern ctxt = |
195 fun markup_extern ctxt = |