--- a/NEWS Fri Jun 10 13:54:50 2016 +0100
+++ b/NEWS Fri Jun 10 16:36:24 2016 +0200
@@ -35,6 +35,16 @@
* Old 'header' command is no longer supported (legacy since
Isabelle2015).
+* Command 'bundle' provides a local theory target to define a bundle
+from the body of specification commands (such as 'declare',
+'declaration', 'notation', 'lemmas', 'lemma'). For example:
+
+bundle foo
+begin
+ declare a [simp]
+ declare b [intro]
+end
+
*** Prover IDE -- Isabelle/Scala/jEdit ***
--- a/src/Doc/Isar_Ref/Spec.thy Fri Jun 10 13:54:50 2016 +0100
+++ b/src/Doc/Isar_Ref/Spec.thy Fri Jun 10 16:36:24 2016 +0200
@@ -206,6 +206,7 @@
text \<open>
\begin{matharray}{rcl}
@{command_def "bundle"} & : & \<open>local_theory \<rightarrow> local_theory\<close> \\
+ @{command "bundle"} & : & \<open>theory \<rightarrow> local_theory\<close> \\
@{command_def "print_bundles"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\
@{command_def "include"} & : & \<open>proof(state) \<rightarrow> proof(state)\<close> \\
@{command_def "including"} & : & \<open>proof(prove) \<rightarrow> proof(prove)\<close> \\
@@ -226,7 +227,8 @@
(\secref{sec:locale}).
@{rail \<open>
- @@{command bundle} @{syntax name} '=' @{syntax thms} @{syntax for_fixes}
+ @@{command bundle} @{syntax name}
+ ( '=' @{syntax thms} @{syntax for_fixes} | @'begin')
;
@@{command print_bundles} ('!'?)
;
@@ -241,6 +243,13 @@
morphisms, when moved into different application contexts; this works
analogously to any other local theory specification.
+ \<^descr> \<^theory_text>\<open>bundle b begin body end\<close> defines a bundle of declarations from the
+ \<open>body\<close> of local theory specifications. It may consist of commands that are
+ technically equivalent to \<^theory_text>\<open>declare\<close> or \<^theory_text>\<open>declaration\<close>, which also includes
+ \<^theory_text>\<open>notation\<close>, for example. Named fact declarations like ``\<^theory_text>\<open>lemmas a [simp] =
+ b\<close>'' or ``\<^theory_text>\<open>lemma a [simp]: B \<proof>\<close>'' are also admitted, but the name
+ bindings are not recorded in the bundle.
+
\<^descr> \<^theory_text>\<open>print_bundles\<close> prints the named bundles that are available in the
current context; the ``\<open>!\<close>'' option indicates extra verbosity.
--- a/src/HOL/Library/FinFun.thy Fri Jun 10 13:54:50 2016 +0100
+++ b/src/HOL/Library/FinFun.thy Fri Jun 10 16:36:24 2016 +0200
@@ -189,12 +189,19 @@
thus "curry f a \<in> finfun" unfolding finfun_def by auto
qed
-bundle finfun =
- fst_finfun[simp] snd_finfun[simp] Abs_finfun_inverse[simp]
- finfun_apply_inverse[simp] Abs_finfun_inject[simp] finfun_apply_inject[simp]
- Diag_finfun[simp] finfun_curry[simp]
- const_finfun[iff] fun_upd_finfun[iff] finfun_apply[iff] map_of_finfun[iff]
- finfun_left_compose[intro] fst_finfun[intro] snd_finfun[intro]
+bundle finfun
+begin
+
+lemmas [simp] =
+ fst_finfun snd_finfun Abs_finfun_inverse
+ finfun_apply_inverse Abs_finfun_inject finfun_apply_inject
+ Diag_finfun finfun_curry
+lemmas [iff] =
+ const_finfun fun_upd_finfun finfun_apply map_of_finfun
+lemmas [intro] =
+ finfun_left_compose fst_finfun snd_finfun
+
+end
lemma Abs_finfun_inject_finite:
fixes x y :: "'a \<Rightarrow> 'b"
@@ -730,8 +737,8 @@
"finite (UNIV :: 'a set) \<Longrightarrow> Finite_Set.fold (\<lambda>a. upd a b') (cnst b) (UNIV :: 'a set) = cnst b'"
begin
-lemma finfun_rec_const [simp]: includes finfun shows
- "finfun_rec cnst upd (K$ c) = cnst c"
+lemma finfun_rec_const [simp]: "finfun_rec cnst upd (K$ c) = cnst c"
+ including finfun
proof(cases "finite (UNIV :: 'a set)")
case False
hence "finfun_default ((K$ c) :: 'a \<Rightarrow>f 'b) = c" by(simp add: finfun_default_const)
@@ -980,9 +987,9 @@
by(simp add: finfun_comp2_def finfun_const_def comp_def)
lemma finfun_comp2_update:
- includes finfun
assumes inj: "inj f"
shows "finfun_comp2 (g(b $:= c)) f = (if b \<in> range f then (finfun_comp2 g f)(inv f b $:= c) else finfun_comp2 g f)"
+ including finfun
proof(cases "b \<in> range f")
case True
from inj have "\<And>x. (op $ g)(f x := c) \<circ> f = (op $ g \<circ> f)(x := c)" by(auto intro!: ext dest: injD)
--- a/src/Pure/Isar/attrib.ML Fri Jun 10 13:54:50 2016 +0100
+++ b/src/Pure/Isar/attrib.ML Fri Jun 10 16:36:24 2016 +0200
@@ -33,11 +33,12 @@
val map_facts_refs: ('a list -> 'att list) -> ('b -> 'fact) ->
(('c * 'a list) * ('b * 'a list) list) list ->
(('c * 'att list) * ('fact * 'att list) list) list
- val global_notes: string -> (binding * (thm list * Token.src list) list) list ->
+ type thms = (thm list * Token.src list) list
+ val global_notes: string -> (binding * thms) list ->
theory -> (string * thm list) list * theory
- val local_notes: string -> (binding * (thm list * Token.src list) list) list ->
+ val local_notes: string -> (binding * thms) list ->
Proof.context -> (string * thm list) list * Proof.context
- val generic_notes: string -> (binding * (thm list * Token.src list) list) list ->
+ val generic_notes: string -> (binding * thms) list ->
Context.generic -> (string * thm list) list * Context.generic
val eval_thms: Proof.context -> (Facts.ref * Token.src list) list -> thm list
val attribute_syntax: attribute context_parser -> Token.src -> attribute
@@ -47,16 +48,13 @@
val attribute_setup: bstring * Position.T -> Input.source -> string ->
local_theory -> local_theory
val internal: (morphism -> attribute) -> Token.src
+ val internal_declaration: declaration -> thms
val add_del: attribute -> attribute -> attribute context_parser
val thm: thm context_parser
val thms: thm list context_parser
val multi_thm: thm list context_parser
- val transform_facts: morphism ->
- (Attrib.binding * (thm list * Token.src list) list) list ->
- (Attrib.binding * (thm list * Token.src list) list) list
- val partial_evaluation: Proof.context ->
- (binding * (thm list * Token.src list) list) list ->
- (binding * (thm list * Token.src list) list) list
+ val transform_facts: morphism -> (Attrib.binding * thms) list -> (Attrib.binding * thms) list
+ val partial_evaluation: Proof.context -> (binding * thms) list -> (binding * thms) list
val print_options: bool -> Proof.context -> unit
val config_bool: Binding.binding ->
(Context.generic -> bool) -> bool Config.T * (theory -> theory)
@@ -194,6 +192,8 @@
(* fact expressions *)
+type thms = (thm list * Token.src list) list;
+
fun global_notes kind facts thy = thy |>
Global_Theory.note_thmss kind (map_facts (map (attribute_global thy)) facts);
@@ -243,6 +243,9 @@
internal_attribute_name ::
[Token.make_string ("<attribute>", Position.none) |> Token.assign (SOME (Token.Attribute att))];
+fun internal_declaration decl =
+ [([Drule.dummy_thm], [internal (fn phi => Thm.declaration_attribute (K (decl phi)))])];
+
(* add/del syntax *)
--- a/src/Pure/Isar/bundle.ML Fri Jun 10 13:54:50 2016 +0100
+++ b/src/Pure/Isar/bundle.ML Fri Jun 10 16:36:24 2016 +0200
@@ -6,14 +6,15 @@
signature BUNDLE =
sig
- type bundle = (thm list * Token.src list) list
val check: Proof.context -> xstring * Position.T -> string
- val get_bundle: Proof.context -> string -> bundle
- val get_bundle_cmd: Proof.context -> xstring * Position.T -> bundle
- val bundle: binding * (thm list * Token.src list) list ->
+ val get_bundle: Proof.context -> string -> Attrib.thms
+ val get_bundle_cmd: Proof.context -> xstring * Position.T -> Attrib.thms
+ val print_bundles: bool -> Proof.context -> unit
+ val bundle: binding * Attrib.thms ->
(binding * typ option * mixfix) list -> local_theory -> local_theory
val bundle_cmd: binding * (Facts.ref * Token.src list) list ->
(binding * string option * mixfix) list -> local_theory -> local_theory
+ val init: binding -> theory -> local_theory
val includes: string list -> Proof.context -> Proof.context
val includes_cmd: (xstring * Position.T) list -> Proof.context -> Proof.context
val include_: string list -> Proof.state -> Proof.state
@@ -24,36 +25,82 @@
generic_theory -> Binding.scope * local_theory
val context_cmd: (xstring * Position.T) list -> Element.context list ->
generic_theory -> Binding.scope * local_theory
- val print_bundles: bool -> Proof.context -> unit
end;
structure Bundle: BUNDLE =
struct
-(* maintain bundles *)
-
-type bundle = (thm list * Token.src list) list;
-
-fun transform_bundle phi : bundle -> bundle =
- map (fn (fact, atts) => (Morphism.fact phi fact, (map o map) (Token.transform phi) atts));
+(** context data **)
structure Data = Generic_Data
(
- type T = bundle Name_Space.table;
- val empty : T = Name_Space.empty_table "bundle";
+ type T = Attrib.thms Name_Space.table * Attrib.thms option;
+ val empty : T = (Name_Space.empty_table "bundle", NONE);
val extend = I;
- val merge = Name_Space.merge_tables;
+ fun merge ((tab1, target1), (tab2, target2)) =
+ (Name_Space.merge_tables (tab1, tab2), merge_options (target1, target2));
);
-val get_bundles = Data.get o Context.Proof;
+
+(* bundles *)
+
+val get_bundles_generic = #1 o Data.get;
+val get_bundles = get_bundles_generic o Context.Proof;
fun check ctxt = #1 o Name_Space.check (Context.Proof ctxt) (get_bundles ctxt);
-val get_bundle = Name_Space.get o get_bundles;
+val get_bundle_generic = Name_Space.get o get_bundles_generic;
+val get_bundle = get_bundle_generic o Context.Proof;
fun get_bundle_cmd ctxt = get_bundle ctxt o check ctxt;
+fun define_bundle def context =
+ let
+ val (name, bundles') = Name_Space.define context true def (get_bundles_generic context);
+ val context' = (Data.map o apfst o K) bundles' context;
+ in (name, context') end;
-(* define bundle *)
+
+(* target -- bundle under construction *)
+
+fun the_target thy =
+ (case #2 (Data.get (Context.Theory thy)) of
+ SOME thms => thms
+ | NONE => error "Missing bundle target");
+
+val reset_target = (Context.theory_map o Data.map o apsnd o K) NONE;
+val set_target = Context.theory_map o Data.map o apsnd o K o SOME;
+
+fun augment_target thms =
+ Local_Theory.background_theory (fn thy => set_target (the_target thy @ thms) thy);
+
+
+(* print bundles *)
+
+fun pretty_bundle ctxt (markup_name, bundle) =
+ let
+ val prt_thm = Pretty.cartouche o Thm.pretty_thm ctxt;
+ fun prt_thm_attribs atts th =
+ Pretty.block (Pretty.breaks (prt_thm th :: Attrib.pretty_attribs ctxt atts));
+ fun prt_thms (ths, []) = map prt_thm ths
+ | prt_thms (ths, atts) = map (prt_thm_attribs atts) ths;
+ in
+ Pretty.block ([Pretty.keyword1 "bundle", Pretty.str " ", Pretty.mark_str markup_name] @
+ (if null bundle then [] else Pretty.fbreaks (Pretty.str " =" :: maps prt_thms bundle)))
+ end;
+
+fun print_bundles verbose ctxt =
+ Pretty.writeln_chunks
+ (map (pretty_bundle ctxt) (Name_Space.markup_table verbose ctxt (get_bundles ctxt)));
+
+
+
+(** define bundle **)
+
+fun transform_bundle phi =
+ map (fn (fact, atts) => (Morphism.fact phi fact, (map o map) (Token.transform phi) atts));
+
+
+(* command *)
local
@@ -67,10 +114,7 @@
|> transform_bundle (Proof_Context.export_morphism ctxt' lthy);
in
lthy |> Local_Theory.declaration {syntax = false, pervasive = true}
- (fn phi => fn context =>
- context |> Data.map
- (#2 o Name_Space.define context true
- (Morphism.binding phi binding, transform_bundle phi bundle)))
+ (fn phi => #2 o define_bundle (Morphism.binding phi binding, transform_bundle phi bundle))
end;
in
@@ -81,7 +125,72 @@
end;
-(* include bundles *)
+(* target *)
+
+local
+
+fun bad_operation _ = error "Not possible in bundle target";
+
+fun conclude invisible binding =
+ Local_Theory.background_theory_result (fn thy =>
+ thy
+ |> invisible ? Context_Position.set_visible_global false
+ |> Context.Theory
+ |> define_bundle (binding, the_target thy)
+ ||> (Context.the_theory
+ #> invisible ? Context_Position.restore_visible_global thy
+ #> reset_target));
+
+fun pretty binding lthy =
+ let
+ val bundle = the_target (Proof_Context.theory_of lthy);
+ val (name, lthy') = lthy
+ |> Local_Theory.raw_theory (Context_Position.set_visible_global false)
+ |> conclude true binding;
+ val thy_ctxt' = Proof_Context.init_global (Proof_Context.theory_of lthy');
+ val markup_name =
+ Name_Space.markup_extern thy_ctxt' (Name_Space.space_of_table (get_bundles thy_ctxt')) name;
+ in [pretty_bundle lthy' (markup_name, bundle)] end;
+
+fun bundle_notes kind facts lthy =
+ let
+ val bundle = facts
+ |> maps (fn ((_, more_atts), thms) => map (fn (ths, atts) => (ths, atts @ more_atts)) thms);
+ in
+ lthy
+ |> augment_target (transform_bundle (Local_Theory.standard_morphism_theory lthy) bundle)
+ |> Generic_Target.standard_notes (op <>) kind facts
+ |> Attrib.local_notes kind facts
+ end;
+
+fun bundle_declaration decl lthy =
+ lthy
+ |> (augment_target o Attrib.internal_declaration)
+ (Morphism.transform (Local_Theory.standard_morphism_theory lthy) decl)
+ |> Generic_Target.standard_declaration (K true) decl;
+
+in
+
+fun init binding thy =
+ thy
+ |> Sign.change_begin
+ |> set_target []
+ |> Proof_Context.init_global
+ |> Local_Theory.init (Sign.naming_of thy)
+ {define = bad_operation,
+ notes = bundle_notes,
+ abbrev = bad_operation,
+ declaration = K bundle_declaration,
+ theory_registration = bad_operation,
+ locale_dependency = bad_operation,
+ pretty = pretty binding,
+ exit = conclude false binding #> #2 #> Local_Theory.target_of #> Sign.change_end_local}
+
+end;
+
+
+
+(** include bundles **)
local
@@ -123,22 +232,4 @@
end;
-
-(* print_bundles *)
-
-fun print_bundles verbose ctxt =
- let
- val prt_thm = Pretty.cartouche o Thm.pretty_thm ctxt;
-
- fun prt_fact (ths, []) = map prt_thm ths
- | prt_fact (ths, atts) = Pretty.enclose "(" ")"
- (Pretty.breaks (map prt_thm ths)) :: Attrib.pretty_attribs ctxt atts;
-
- fun prt_bundle (name, bundle) =
- Pretty.block (Pretty.keyword1 "bundle" :: Pretty.str " " :: Pretty.mark_str name ::
- Pretty.breaks (Pretty.str " =" :: maps prt_fact bundle));
- in
- map prt_bundle (Name_Space.markup_table verbose ctxt (get_bundles ctxt))
- end |> Pretty.writeln_chunks;
-
end;
--- a/src/Pure/Isar/class_declaration.ML Fri Jun 10 13:54:50 2016 +0100
+++ b/src/Pure/Isar/class_declaration.ML Fri Jun 10 16:36:24 2016 +0200
@@ -348,9 +348,10 @@
let
val thy = Proof_Context.theory_of lthy;
val proto_sup = prep_class thy raw_sup;
- val proto_sub = case Named_Target.class_of lthy of
+ val proto_sub =
+ (case Named_Target.class_of lthy of
SOME class => class
- | NONE => error "Not in a class target";
+ | NONE => error "Not in a class target");
val (sub, sup) = Axclass.cert_classrel thy (proto_sub, proto_sup);
val expr = ([(sup, (("", false), Expression.Positional []))], []);
--- a/src/Pure/Isar/generic_target.ML Fri Jun 10 13:54:50 2016 +0100
+++ b/src/Pure/Isar/generic_target.ML Fri Jun 10 16:36:24 2016 +0200
@@ -20,6 +20,12 @@
val background_abbrev: binding * term -> term list -> local_theory -> (term * term) * local_theory
(*nested local theories primitives*)
+ val standard_facts: local_theory -> Proof.context ->
+ (Attrib.binding * Attrib.thms) list -> (Attrib.binding * Attrib.thms) list
+ val standard_notes: (int * int -> bool) -> string -> (Attrib.binding * Attrib.thms) list ->
+ local_theory -> local_theory
+ val standard_declaration: (int * int -> bool) ->
+ (morphism -> Context.generic -> Context.generic) -> local_theory -> local_theory
val standard_const: (int * int -> bool) -> Syntax.mode -> (binding * mixfix) * term ->
local_theory -> local_theory
@@ -29,9 +35,9 @@
bool -> (binding * mixfix) * (Attrib.binding * term) -> local_theory ->
(term * (string * thm)) * local_theory
val notes:
- (string -> (Attrib.binding * (thm list * Token.src list) list) list ->
- (Attrib.binding * (thm list * Token.src list) list) list -> local_theory -> local_theory) ->
- string -> (Attrib.binding * (thm list * Token.src list) list) list -> local_theory ->
+ (string -> (Attrib.binding * Attrib.thms) list ->
+ (Attrib.binding * Attrib.thms) list -> local_theory -> local_theory) ->
+ string -> (Attrib.binding * Attrib.thms) list -> local_theory ->
(string * thm list) list * local_theory
val abbrev: (Syntax.mode -> binding * mixfix -> term ->
term list * term list -> local_theory -> local_theory) ->
@@ -40,10 +46,8 @@
(*theory target primitives*)
val theory_target_foundation: ((binding * typ) * mixfix) * (binding * term) ->
term list * term list -> local_theory -> (term * thm) * local_theory
- val theory_target_notes: string ->
- (Attrib.binding * (thm list * Token.src list) list) list ->
- (Attrib.binding * (thm list * Token.src list) list) list ->
- local_theory -> local_theory
+ val theory_target_notes: string -> (Attrib.binding * Attrib.thms) list ->
+ (Attrib.binding * Attrib.thms) list -> local_theory -> local_theory
val theory_target_abbrev: Syntax.mode -> (binding * mixfix) -> term -> term list * term list ->
local_theory -> local_theory
@@ -55,10 +59,8 @@
local_theory -> local_theory
(*locale target primitives*)
- val locale_target_notes: string -> string ->
- (Attrib.binding * (thm list * Token.src list) list) list ->
- (Attrib.binding * (thm list * Token.src list) list) list ->
- local_theory -> local_theory
+ val locale_target_notes: string -> string -> (Attrib.binding * Attrib.thms) list ->
+ (Attrib.binding * Attrib.thms) list -> local_theory -> local_theory
val locale_target_abbrev: string -> Syntax.mode -> (binding * mixfix) -> term -> term list * term list ->
local_theory -> local_theory
val locale_target_declaration: string -> bool -> declaration -> local_theory -> local_theory
--- a/src/Pure/Isar/local_theory.ML Fri Jun 10 13:54:50 2016 +0100
+++ b/src/Pure/Isar/local_theory.ML Fri Jun 10 16:36:24 2016 +0200
@@ -10,6 +10,7 @@
structure Attrib =
struct
type binding = binding * Token.src list;
+ type thms = (thm list * Token.src list) list;
end;
signature LOCAL_THEORY =
@@ -30,6 +31,7 @@
val new_group: local_theory -> local_theory
val reset_group: local_theory -> local_theory
val standard_morphism: local_theory -> Proof.context -> morphism
+ val standard_morphism_theory: local_theory -> morphism
val standard_form: local_theory -> Proof.context -> (morphism -> 'a) -> 'a
val raw_theory_result: (theory -> 'a * theory) -> local_theory -> 'a * local_theory
val raw_theory: (theory -> theory) -> local_theory -> local_theory
@@ -45,10 +47,10 @@
val define_internal: (binding * mixfix) * (Attrib.binding * term) -> local_theory ->
(term * (string * thm)) * local_theory
val note: Attrib.binding * thm list -> local_theory -> (string * thm list) * local_theory
- val notes: (Attrib.binding * (thm list * Token.src list) list) list ->
- local_theory -> (string * thm list) list * local_theory
- val notes_kind: string -> (Attrib.binding * (thm list * Token.src list) list) list ->
- local_theory -> (string * thm list) list * local_theory
+ val notes: (Attrib.binding * Attrib.thms) list -> local_theory ->
+ (string * thm list) list * local_theory
+ val notes_kind: string -> (Attrib.binding * Attrib.thms) list -> local_theory ->
+ (string * thm list) list * local_theory
val abbrev: Syntax.mode -> (binding * mixfix) * term -> local_theory ->
(term * term) * local_theory
val declaration: {syntax: bool, pervasive: bool} -> declaration -> local_theory -> local_theory
@@ -85,9 +87,8 @@
type operations =
{define: bool -> (binding * mixfix) * (Attrib.binding * term) -> local_theory ->
(term * (string * thm)) * local_theory,
- notes: string ->
- (Attrib.binding * (thm list * Token.src list) list) list ->
- local_theory -> (string * thm list) list * local_theory,
+ notes: string -> (Attrib.binding * Attrib.thms) list -> local_theory ->
+ (string * thm list) list * local_theory,
abbrev: Syntax.mode -> (binding * mixfix) * term -> local_theory ->
(term * term) * local_theory,
declaration: {syntax: bool, pervasive: bool} -> declaration -> local_theory -> local_theory,
@@ -195,6 +196,9 @@
Morphism.binding_morphism "Local_Theory.standard_binding"
(Name_Space.transform_binding (Proof_Context.naming_of lthy));
+fun standard_morphism_theory lthy =
+ standard_morphism lthy (Proof_Context.init_global (Proof_Context.theory_of lthy));
+
fun standard_form lthy ctxt x =
Morphism.form (Morphism.transform (standard_morphism lthy ctxt) x);
--- a/src/Pure/Isar/locale.ML Fri Jun 10 13:54:50 2016 +0100
+++ b/src/Pure/Isar/locale.ML Fri Jun 10 16:36:24 2016 +0200
@@ -35,7 +35,7 @@
thm option * thm option -> thm list ->
Element.context_i list ->
declaration list ->
- (string * (Attrib.binding * (thm list * Token.src list) list) list) list ->
+ (string * (Attrib.binding * Attrib.thms) list) list ->
(string * morphism) list -> theory -> theory
val intern: theory -> xstring -> string
val check: theory -> xstring * Position.T -> string
@@ -50,7 +50,7 @@
val specification_of: theory -> string -> term option * term list
(* Storing results *)
- val add_thmss: string -> string -> (Attrib.binding * (thm list * Token.src list) list) list ->
+ val add_thmss: string -> string -> (Attrib.binding * Attrib.thms) list ->
Proof.context -> Proof.context
val add_declaration: string -> bool -> declaration -> Proof.context -> Proof.context
@@ -135,7 +135,7 @@
(*syntax declarations*)
syntax_decls: (declaration * serial) list,
(*theorem declarations*)
- notes: ((string * (Attrib.binding * (thm list * Token.src list) list) list) * serial) list,
+ notes: ((string * (Attrib.binding * Attrib.thms) list) * serial) list,
(*locale dependencies (sublocale relation) in reverse order*)
dependencies: ((string * (morphism * morphism)) * serial) list,
(*mixin part of dependencies*)
@@ -612,21 +612,10 @@
(* Declarations *)
-local
-
-fun add_decl loc decl =
- add_thmss loc ""
- [((Binding.empty, [Attrib.internal (fn phi => Thm.declaration_attribute (K (decl phi)))]),
- [([Drule.dummy_thm], [])])];
-
-in
-
fun add_declaration loc syntax decl =
syntax ?
Proof_Context.background_theory ((change_locale loc o apfst o apfst) (cons (decl, serial ())))
- #> add_decl loc decl;
-
-end;
+ #> add_thmss loc "" [(Attrib.empty_binding, Attrib.internal_declaration decl)];
(*** Reasoning about locales ***)
--- a/src/Pure/Isar/named_target.ML Fri Jun 10 13:54:50 2016 +0100
+++ b/src/Pure/Isar/named_target.ML Fri Jun 10 16:36:24 2016 +0200
@@ -40,14 +40,14 @@
else NONE;
fun is_theory lthy =
- case get_data lthy of
+ (case get_data lthy of
SOME ("", _) => true
- | _ => false;
+ | _ => false);
fun target_of lthy =
- case get_data lthy of
+ (case get_data lthy of
NONE => error "Not in a named target"
- | SOME (target, _) => target;
+ | SOME (target, _) => target);
fun locale_name_of NONE = NONE
| locale_name_of (SOME ("", _)) = NONE
@@ -58,9 +58,9 @@
val bottom_locale_of = locale_name_of o get_bottom_data;
fun class_of lthy =
- case get_data lthy of
+ (case get_data lthy of
SOME (class, true) => SOME class
- | _ => NONE;
+ | _ => NONE);
(* operations *)
--- a/src/Pure/Isar/outer_syntax.ML Fri Jun 10 13:54:50 2016 +0100
+++ b/src/Pure/Isar/outer_syntax.ML Fri Jun 10 16:36:24 2016 +0200
@@ -11,6 +11,8 @@
type command_keyword = string * Position.T
val command: command_keyword -> string ->
(Toplevel.transition -> Toplevel.transition) parser -> unit
+ val maybe_begin_local_theory: command_keyword -> string ->
+ (local_theory -> local_theory) parser -> (theory -> local_theory) parser -> unit
val local_theory': command_keyword -> string ->
(bool -> local_theory -> local_theory) parser -> unit
val local_theory: command_keyword -> string ->
@@ -25,7 +27,7 @@
val parse_spans: Token.T list -> Command_Span.span list
val side_comments: Token.T list -> Token.T list
val command_reports: theory -> Token.T -> Position.report_text list
- val check_command: Proof.context -> string * Position.T -> string
+ val check_command: Proof.context -> command_keyword -> string
end;
structure Outer_Syntax: OUTER_SYNTAX =
@@ -148,6 +150,14 @@
fun command (name, pos) comment parse =
raw_command (name, pos) comment (Parser parse);
+fun maybe_begin_local_theory command_keyword comment parse_local parse_global =
+ raw_command command_keyword comment
+ (Restricted_Parser (fn restricted =>
+ Parse.opt_target -- parse_local
+ >> (fn (target, f) => Toplevel.local_theory restricted target f) ||
+ (if is_some restricted then Scan.fail
+ else parse_global >> Toplevel.begin_local_theory true)));
+
fun local_theory_command trans command_keyword comment parse =
raw_command command_keyword comment
(Restricted_Parser (fn restricted =>
--- a/src/Pure/Isar/specification.ML Fri Jun 10 13:54:50 2016 +0100
+++ b/src/Pure/Isar/specification.ML Fri Jun 10 16:36:24 2016 +0200
@@ -51,7 +51,7 @@
val notation: bool -> Syntax.mode -> (term * mixfix) list -> local_theory -> local_theory
val notation_cmd: bool -> Syntax.mode -> (string * mixfix) list -> local_theory -> local_theory
val theorems: string ->
- (Attrib.binding * (thm list * Token.src list) list) list ->
+ (Attrib.binding * Attrib.thms) list ->
(binding * typ option * mixfix) list ->
bool -> local_theory -> (string * thm list) list * local_theory
val theorems_cmd: string ->
--- a/src/Pure/Pure.thy Fri Jun 10 13:54:50 2016 +0100
+++ b/src/Pure/Pure.thy Fri Jun 10 16:36:24 2016 +0200
@@ -31,7 +31,7 @@
"declaration" "syntax_declaration"
"parse_ast_translation" "parse_translation" "print_translation"
"typed_print_translation" "print_ast_translation" "oracle" :: thy_decl % "ML"
- and "bundle" :: thy_decl
+ and "bundle" :: thy_decl_block
and "include" "including" :: prf_decl
and "print_bundles" :: diag
and "context" "locale" "experiment" :: thy_decl_block
@@ -491,9 +491,11 @@
local
val _ =
- Outer_Syntax.local_theory @{command_keyword bundle} "define bundle of declarations"
+ Outer_Syntax.maybe_begin_local_theory @{command_keyword bundle}
+ "define bundle of declarations"
((Parse.binding --| @{keyword "="}) -- Parse.thms1 -- Parse.for_fixes
- >> (uncurry Bundle.bundle_cmd));
+ >> (uncurry Bundle.bundle_cmd))
+ (Parse.binding --| Parse.begin >> Bundle.init);
val _ =
Outer_Syntax.command @{command_keyword include}