equal
deleted
inserted
replaced
25 val _ = |
25 val _ = |
26 OuterSyntax.command "locale" "define named proof context" K.thy_decl |
26 OuterSyntax.command "locale" "define named proof context" K.thy_decl |
27 (P.name -- Scan.optional (P.$$$ "=" |-- P.!!! locale_val) (([], []), []) -- P.opt_begin |
27 (P.name -- Scan.optional (P.$$$ "=" |-- P.!!! locale_val) (([], []), []) -- P.opt_begin |
28 >> (fn ((name, (expr, elems)), begin) => |
28 >> (fn ((name, (expr, elems)), begin) => |
29 (begin ? Toplevel.print) o Toplevel.begin_local_theory begin |
29 (begin ? Toplevel.print) o Toplevel.begin_local_theory begin |
30 (Expression.add_locale_cmd name name expr elems #-> TheoryTarget.begin))); |
30 (Expression.add_locale_cmd name name expr elems #> |
|
31 (fn ((target, notes), ctxt) => TheoryTarget.begin target ctxt |> |
|
32 fold (fn (kind, facts) => LocalTheory.notes kind facts #> snd) notes)))); |
31 |
33 |
32 val _ = |
34 val _ = |
33 OuterSyntax.improper_command "print_locales" "print locales of this theory" K.diag |
35 OuterSyntax.improper_command "print_locales" "print locales of this theory" K.diag |
34 (Scan.succeed (Toplevel.no_timing o (Toplevel.unknown_theory o |
36 (Scan.succeed (Toplevel.no_timing o (Toplevel.unknown_theory o |
35 Toplevel.keep (NewLocale.print_locales o Toplevel.theory_of)))); |
37 Toplevel.keep (NewLocale.print_locales o Toplevel.theory_of)))); |