--- a/NEWS Sat Nov 30 16:01:58 2024 +0100
+++ b/NEWS Sat Nov 30 16:42:22 2024 +0100
@@ -81,12 +81,12 @@
* Command "unbundle b" and its variants like "context includes b" allow
an optional name prefix with the reserved word "no": "unbundle no b"
-etc. This inverts the polarity of bundled declarations like 'notation'
-vs. 'no_notation', and thus avoids redundant bundle definitions like
-"foobar_syntax" vs. "no_foobar_syntax", because "no foobar_syntax" may
-be used instead. Consequently, the syntax for multiple bundle names has
-been changed slightly, demanding an explicit 'and' keyword. Minor
-INCOMPATIBILITY.
+etc. This reverses both the order and polarity of bundled declarations
+like 'notation' vs. 'no_notation', and thus avoids redundant bundle
+definitions like "foobar_syntax" vs. "no_foobar_syntax", because "no
+foobar_syntax" may be used instead. Consequently, the syntax for
+multiple bundle names has been changed slightly, demanding an explicit
+'and' keyword. Minor INCOMPATIBILITY.
* Command "open_bundle b" is like "bundle b" followed by "unbundle b",
so its declarations are applied immediately, but also named for later
--- a/src/Doc/Isar_Ref/Spec.thy Sat Nov 30 16:01:58 2024 +0100
+++ b/src/Doc/Isar_Ref/Spec.thy Sat Nov 30 16:42:22 2024 +0100
@@ -297,7 +297,9 @@
\<^item> @{command type_notation} versus @{command no_type_notation}
This also works recursively for the @{command unbundle} command as
- declaration inside a @{command bundle} definition.
+ declaration inside a @{command bundle} definition: \<^verbatim>\<open>no\<close> means that
+ both the order and polarity of declarations is reversed (following
+ algebraic group laws).
Here is an artificial example of bundling various configuration options:
--- a/src/Pure/Isar/bundle.ML Sat Nov 30 16:01:58 2024 +0100
+++ b/src/Pure/Isar/bundle.ML Sat Nov 30 16:42:22 2024 +0100
@@ -126,10 +126,11 @@
val notes = if loc then Local_Theory.notes else Attrib.local_notes "";
val add0 = Syntax.get_polarity ctxt;
val add1 = Syntax.effective_polarity ctxt add;
+ val bundle' = if add1 then bundle else rev (map (apsnd rev) bundle);
in
ctxt
|> Context_Position.set_visible false
- |> notes [(Binding.empty_atts, polarity_decls add1 @ bundle @ polarity_decls add0)] |> snd
+ |> notes [(Binding.empty_atts, polarity_decls add1 @ bundle' @ polarity_decls add0)] |> snd
|> Context_Position.restore_visible ctxt
end;