--- a/NEWS Thu Jun 09 17:14:13 2016 +0200
+++ b/NEWS Fri Jun 10 12:45:34 2016 +0200
@@ -35,9 +35,15 @@
* Old 'header' command is no longer supported (legacy since
Isabelle2015).
-* Command 'bundle_definition' provides a local theory target to define a
-bundle from the body of specification commands (e.g. 'declare',
-'declaration', 'notation', 'lemmas', 'lemma').
+* 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 Thu Jun 09 17:14:13 2016 +0200
+++ b/src/Doc/Isar_Ref/Spec.thy Fri Jun 10 12:45:34 2016 +0200
@@ -206,7 +206,7 @@
text \<open>
\begin{matharray}{rcl}
@{command_def "bundle"} & : & \<open>local_theory \<rightarrow> local_theory\<close> \\
- @{command_def "bundle_definition"} & : & \<open>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> \\
@@ -227,9 +227,8 @@
(\secref{sec:locale}).
@{rail \<open>
- @@{command bundle} @{syntax name} '=' @{syntax thms} @{syntax for_fixes}
- ;
- @@{command bundle_definition} @{syntax name} @'begin'
+ @@{command bundle} @{syntax name}
+ ( '=' @{syntax thms} @{syntax for_fixes} | @'begin')
;
@@{command print_bundles} ('!'?)
;
@@ -244,12 +243,12 @@
morphisms, when moved into different application contexts; this works
analogously to any other local theory specification.
- \<^descr> \<^theory_text>\<open>bundle_definition 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>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/Pure/Isar/outer_syntax.ML Thu Jun 09 17:14:13 2016 +0200
+++ b/src/Pure/Isar/outer_syntax.ML Fri Jun 10 12:45:34 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 ->
@@ -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/Pure.thy Thu Jun 09 17:14:13 2016 +0200
+++ b/src/Pure/Pure.thy Fri Jun 10 12:45:34 2016 +0200
@@ -31,8 +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_definition" :: thy_decl_block
+ and "bundle" :: thy_decl_block
and "include" "including" :: prf_decl
and "print_bundles" :: diag
and "context" "locale" "experiment" :: thy_decl_block
@@ -492,14 +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));
-
-val _ =
- Outer_Syntax.command @{command_keyword bundle_definition}
- "define bundle of declarations (local theory target)"
- (Parse.binding --| Parse.begin >> (Toplevel.begin_local_theory true o Bundle.init));
+ >> (uncurry Bundle.bundle_cmd))
+ (Parse.binding --| Parse.begin >> Bundle.init);
val _ =
Outer_Syntax.command @{command_keyword include}