# HG changeset patch # User wenzelm # Date 1728133116 -7200 # Node ID 0fb1e2dd412211b9bce3222a7f255a4ca0707cb4 # Parent 7b3b27576f45cbc3ac7e0d8bc1fd5fb4e9febdde first-class support for "unbundle no foobar_syntax" -- avoid redundant "bundle no_foobar_syntax" definitions; diff -r 7b3b27576f45 -r 0fb1e2dd4122 NEWS --- a/NEWS Fri Oct 04 23:38:04 2024 +0200 +++ b/NEWS Sat Oct 05 14:58:36 2024 +0200 @@ -9,12 +9,18 @@ *** General *** +* 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. + * Command "open_bundle b" is like "bundle b" followed by "unbundle b", so its declarations are applied immediately, but also named for later -re-use. - -* The syntax of opnening bundles has changed slightly: multiple bundles -need to be separated by the keyword 'and'. Minor INCOMPATIBILITY. +re-use: "unbundle no b" etc. * Inner syntax translations now support formal dependencies via commands 'syntax_types' or 'syntax_consts'. This is essentially an abstract @@ -53,11 +59,11 @@ * Various declaration bundles support adhoc modification of notation, notably like this: - unbundle no_list_syntax - unbundle no_listcompr_syntax - unbundle no_rtrancl_syntax - unbundle no_trancl_syntax - unbundle no_reflcl_syntax + unbundle no list_syntax + unbundle no listcompr_syntax + unbundle no rtrancl_syntax + unbundle no trancl_syntax + unbundle no reflcl_syntax This is more robust than individual 'no_syntax' / 'no_notation' commands, which need to copy mixfix declarations from elsewhere and thus diff -r 7b3b27576f45 -r 0fb1e2dd4122 src/Doc/Datatypes/Datatypes.thy --- a/src/Doc/Datatypes/Datatypes.thy Fri Oct 04 23:38:04 2024 +0200 +++ b/src/Doc/Datatypes/Datatypes.thy Sat Oct 05 14:58:36 2024 +0200 @@ -453,7 +453,7 @@ Incidentally, this is how the traditional syntax can be set up: \ (*<*) -unbundle no_list_syntax +unbundle no list_syntax (*>*) syntax "_list" :: "args \ 'a list" (\[(_)]\) diff -r 7b3b27576f45 -r 0fb1e2dd4122 src/Doc/Implementation/Local_Theory.thy --- a/src/Doc/Implementation/Local_Theory.thy Fri Oct 04 23:38:04 2024 +0200 +++ b/src/Doc/Implementation/Local_Theory.thy Sat Oct 05 14:58:36 2024 +0200 @@ -91,7 +91,7 @@ text %mlref \ \begin{mldecls} @{define_ML_type local_theory = Proof.context} \\ - @{define_ML Named_Target.init: "string list -> string -> theory -> local_theory"} \\[1ex] + @{define_ML Named_Target.init: "Bundle.name list -> string -> theory -> local_theory"} \\[1ex] @{define_ML Local_Theory.define: "(binding * mixfix) * (Attrib.binding * term) -> local_theory -> (term * (string * thm)) * local_theory"} \\ @{define_ML Local_Theory.note: "Attrib.binding * thm list -> diff -r 7b3b27576f45 -r 0fb1e2dd4122 src/Doc/Isar_Ref/Spec.thy --- a/src/Doc/Isar_Ref/Spec.thy Fri Oct 04 23:38:04 2024 +0200 +++ b/src/Doc/Isar_Ref/Spec.thy Sat Oct 05 14:58:36 2024 +0200 @@ -246,7 +246,7 @@ ; @{syntax_def "opening"}: @'opening' @{syntax bundles} ; - @{syntax bundles}: @{syntax name} + @'and' + @{syntax bundles}: ('no')? @{syntax name} + @'and' \ \<^descr> \<^theory_text>\bundle b = decls\ defines a bundle of declarations in the current @@ -289,6 +289,17 @@ effect is confined to the surface context within the specification block itself and the corresponding \<^theory_text>\begin\ / \<^theory_text>\end\ block. + \<^descr> Bundle names may be prefixed by the reserved word \<^verbatim>\no\ to indicate that + the polarity of certain declaration commands should be inverted, notably: + + \<^item> @{command syntax} versus @{command no_syntax} + \<^item> @{command notation} versus @{command no_notation} + \<^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. + + Here is an artificial example of bundling various configuration options: \ diff -r 7b3b27576f45 -r 0fb1e2dd4122 src/HOL/Analysis/Cross3.thy --- a/src/HOL/Analysis/Cross3.thy Fri Oct 04 23:38:04 2024 +0200 +++ b/src/HOL/Analysis/Cross3.thy Sat Oct 05 14:58:36 2024 +0200 @@ -10,7 +10,7 @@ imports Determinants Cartesian_Euclidean_Space begin -context includes no_set_product_syntax +context includes no set_product_syntax begin \\locally disable syntax for set product, to avoid warnings\ definition\<^marker>\tag important\ cross3 :: "[real^3, real^3] \ real^3" (infixr \\\ 80) @@ -24,14 +24,9 @@ open_bundle cross3_syntax begin notation cross3 (infixr \\\ 80) -unbundle no_set_product_syntax +unbundle no set_product_syntax end -bundle no_cross3_syntax -begin -no_notation cross3 (infixr \\\ 80) -unbundle set_product_syntax -end subsection\ Basic lemmas\ @@ -221,7 +216,7 @@ shows "\continuous_on S f; continuous_on S g\ \ continuous_on S (\x. (f x) \ (g x))" by (simp add: continuous_on_eq_continuous_within continuous_cross) -unbundle no_cross3_syntax +unbundle no cross3_syntax end diff -r 7b3b27576f45 -r 0fb1e2dd4122 src/HOL/Analysis/Finite_Cartesian_Product.thy --- a/src/HOL/Analysis/Finite_Cartesian_Product.thy Fri Oct 04 23:38:04 2024 +0200 +++ b/src/HOL/Analysis/Finite_Cartesian_Product.thy Sat Oct 05 14:58:36 2024 +0200 @@ -25,11 +25,6 @@ notation vec_nth (infixl \$\ 90) and vec_lambda (binder \\\ 10) end -bundle no_vec_syntax -begin -no_notation vec_nth (infixl \$\ 90) and vec_lambda (binder \\\ 10) -end - text \ Concrete syntax for \('a, 'b) vec\: \<^item> \'a^'b\ becomes \('a, 'b::finite) vec\ diff -r 7b3b27576f45 -r 0fb1e2dd4122 src/HOL/Analysis/Inner_Product.thy --- a/src/HOL/Analysis/Inner_Product.thy Fri Oct 04 23:38:04 2024 +0200 +++ b/src/HOL/Analysis/Inner_Product.thy Sat Oct 05 14:58:36 2024 +0200 @@ -466,9 +466,4 @@ notation inner (infix \\\ 70) end -bundle no_inner_syntax -begin -no_notation inner (infix \\\ 70) end - -end diff -r 7b3b27576f45 -r 0fb1e2dd4122 src/HOL/Analysis/Lipschitz.thy --- a/src/HOL/Analysis/Lipschitz.thy Fri Oct 04 23:38:04 2024 +0200 +++ b/src/HOL/Analysis/Lipschitz.thy Sat Oct 05 14:58:36 2024 +0200 @@ -17,11 +17,6 @@ notation\<^marker>\tag important\ lipschitz_on (\_-lipschitz'_on\ [1000]) end -bundle no_lipschitz_syntax -begin -no_notation lipschitz_on (\_-lipschitz'_on\ [1000]) -end - lemma lipschitz_onI: "L-lipschitz_on X f" if "\x y. x \ X \ y \ X \ dist (f x) (f y) \ L * dist x y" "0 \ L" using that by (auto simp: lipschitz_on_def) diff -r 7b3b27576f45 -r 0fb1e2dd4122 src/HOL/Combinatorics/Perm.thy --- a/src/HOL/Combinatorics/Perm.thy Fri Oct 04 23:38:04 2024 +0200 +++ b/src/HOL/Combinatorics/Perm.thy Sat Oct 05 14:58:36 2024 +0200 @@ -792,18 +792,13 @@ subsection \Syntax\ -open_bundle no_permutation_syntax +bundle permutation_syntax begin -no_notation swap (\\_ \ _\\) -no_notation cycle (\\_\\) -no_notation "apply" (infixl \\$\\ 999) +notation swap (\\_ \ _\\) +notation cycle (\\_\\) +notation "apply" (infixl \\$\\ 999) end -bundle permutation_syntax -begin -notation swap (\\_ \ _\\) -notation cycle (\\_\\) -notation "apply" (infixl \\$\\ 999) -end +unbundle no permutation_syntax end diff -r 7b3b27576f45 -r 0fb1e2dd4122 src/HOL/Decision_Procs/Approximation.thy --- a/src/HOL/Decision_Procs/Approximation.thy Fri Oct 04 23:38:04 2024 +0200 +++ b/src/HOL/Decision_Procs/Approximation.thy Sat Oct 05 14:58:36 2024 +0200 @@ -1145,7 +1145,6 @@ bundle floatarith_syntax begin - notation Add (\Add\) notation Minus (\Minus\) notation Mult (\Mult\) @@ -1164,31 +1163,6 @@ notation Floor (\Floor\) notation Var (\Var\) notation Num (\Num\) - -end - -bundle no_floatarith_syntax -begin - -no_notation Add (\Add\) -no_notation Minus (\Minus\) -no_notation Mult (\Mult\) -no_notation Inverse (\Inverse\) -no_notation Cos (\Cos\) -no_notation Arctan (\Arctan\) -no_notation Abs (\Abs\) -no_notation Max (\Max\) -no_notation Min (\Min\) -no_notation Pi (\Pi\) -no_notation Sqrt (\Sqrt\) -no_notation Exp (\Exp\) -no_notation Powr (\Powr\) -no_notation Ln (\Ln\) -no_notation Power (\Power\) -no_notation Floor (\Floor\) -no_notation Var (\Var\) -no_notation Num (\Num\) - end hide_const (open) diff -r 7b3b27576f45 -r 0fb1e2dd4122 src/HOL/Library/Option_ord.thy --- a/src/HOL/Library/Option_ord.thy Fri Oct 04 23:38:04 2024 +0200 +++ b/src/HOL/Library/Option_ord.thy Sat Oct 05 14:58:36 2024 +0200 @@ -449,6 +449,6 @@ instance option :: (complete_linorder) complete_linorder .. -unbundle no_lattice_syntax +unbundle no lattice_syntax end diff -r 7b3b27576f45 -r 0fb1e2dd4122 src/HOL/List.thy --- a/src/HOL/List.thy Fri Oct 04 23:38:04 2024 +0200 +++ b/src/HOL/List.thy Sat Oct 05 14:58:36 2024 +0200 @@ -51,9 +51,9 @@ "[x, xs]" \ "x#[xs]" "[x]" \ "x#[]" -bundle no_list_syntax +bundle list_syntax begin -no_syntax +syntax "_list" :: "args \ 'a list" (\(\indent=1 notation=\mixfix list enumeration\\[_])\) end @@ -457,9 +457,9 @@ syntax (ASCII) "_lc_gen" :: "'a \ 'a list \ lc_qual" (\_ <- _\) -bundle no_listcompr_syntax +bundle listcompr_syntax begin -no_syntax +syntax "_listcompr" :: "'a \ lc_qual \ lc_quals \ 'a list" (\[_ . __\) "_lc_end" :: "lc_quals" (\]\) end diff -r 7b3b27576f45 -r 0fb1e2dd4122 src/HOL/Main.thy --- a/src/HOL/Main.thy Fri Oct 04 23:38:04 2024 +0200 +++ b/src/HOL/Main.thy Sat Oct 05 14:58:36 2024 +0200 @@ -69,8 +69,8 @@ begin notation - bot (\\\) and - top (\\\) and + bot (\\\) and + top (\\\) and inf (infixl \\\ 70) and sup (infixl \\\ 65) and Inf (\\ _\ [900] 900) and @@ -84,25 +84,6 @@ end -bundle no_lattice_syntax -begin - -no_notation - bot (\\\) and - top (\\\) and - inf (infixl \\\ 70) and - sup (infixl \\\ 65) and - Inf (\\ _\ [900] 900) and - Sup (\\ _\ [900] 900) - -no_syntax - "_INF1" :: "pttrns \ 'b \ 'b" (\(\indent=3 notation=\binder \\\\_./ _)\ [0, 10] 10) - "_INF" :: "pttrn \ 'a set \ 'b \ 'b" (\(\indent=3 notation=\binder \\\\_\_./ _)\ [0, 0, 10] 10) - "_SUP1" :: "pttrns \ 'b \ 'b" (\(\indent=3 notation=\binder \\\\_./ _)\ [0, 10] 10) - "_SUP" :: "pttrn \ 'a set \ 'b \ 'b" (\(\indent=3 notation=\binder \\\\_\_./ _)\ [0, 0, 10] 10) +unbundle no lattice_syntax end - -unbundle no_lattice_syntax - -end diff -r 7b3b27576f45 -r 0fb1e2dd4122 src/HOL/Product_Type.thy --- a/src/HOL/Product_Type.thy Fri Oct 04 23:38:04 2024 +0200 +++ b/src/HOL/Product_Type.thy Sat Oct 05 14:58:36 2024 +0200 @@ -1008,11 +1008,6 @@ notation Product_Type.Times (infixr \\\ 80) end -bundle no_set_product_syntax -begin -no_notation Product_Type.Times (infixr \\\ 80) -end - syntax "_Sigma" :: "pttrn \ 'a set \ 'b set \ ('a \ 'b) set" (\(\indent=3 notation=\binder SIGMA\\SIGMA _:_./ _)\ [0, 0, 10] 10) diff -r 7b3b27576f45 -r 0fb1e2dd4122 src/HOL/Set.thy --- a/src/HOL/Set.thy Fri Oct 04 23:38:04 2024 +0200 +++ b/src/HOL/Set.thy Sat Oct 05 14:58:36 2024 +0200 @@ -38,15 +38,6 @@ not_member (\(\notation=\infix ~:\\_/ ~: _)\ [51, 51] 50) end -bundle no_member_ASCII_syntax -begin -no_notation (ASCII) - member (\'(:')\) and - member (\(\notation=\infix :\\_/ : _)\ [51, 51] 50) and - not_member (\'(~:')\) and - not_member (\(\notation=\infix ~:\\_/ ~: _)\ [51, 51] 50) -end - text \Set comprehensions\ diff -r 7b3b27576f45 -r 0fb1e2dd4122 src/HOL/Tools/Lifting/lifting_def_code_dt.ML --- a/src/HOL/Tools/Lifting/lifting_def_code_dt.ML Fri Oct 04 23:38:04 2024 +0200 +++ b/src/HOL/Tools/Lifting/lifting_def_code_dt.ML Sat Oct 05 14:58:36 2024 +0200 @@ -272,7 +272,9 @@ |> Lifting_Info.lookup_quot_thm_quotients lthy2 |> is_some val qty_code_dt_bundle_name = bundle_name_of_rep_isom_data rep_isom_data val rep_isom = mk_rep_isom_of_code_dt qty_ret code_dt |> the - val lthy3 = if quot_active then lthy2 else Bundle.includes [qty_code_dt_bundle_name] lthy2 + val lthy3 = + if quot_active then lthy2 + else Bundle.includes [(true, qty_code_dt_bundle_name)] lthy2 fun qty_isom_of_rep_isom rep = domain_type (dest_Const_type rep) val qty_isom = qty_isom_of_rep_isom rep_isom val f'_var = (Binding.suffix_name "_aux" (fst var), NoSyn); diff -r 7b3b27576f45 -r 0fb1e2dd4122 src/HOL/Tools/Lifting/lifting_setup.ML --- a/src/HOL/Tools/Lifting/lifting_setup.ML Fri Oct 04 23:38:04 2024 +0200 +++ b/src/HOL/Tools/Lifting/lifting_setup.ML Sat Oct 05 14:58:36 2024 +0200 @@ -959,7 +959,7 @@ fun pointer_of_bundle_name bundle_name ctxt = let - val bundle = Bundle.read ctxt bundle_name + val bundle = Bundle.get ctxt (Bundle.check ctxt bundle_name) fun err () = error "The provided bundle is not a lifting bundle" in (case bundle of diff -r 7b3b27576f45 -r 0fb1e2dd4122 src/HOL/Transitive_Closure.thy --- a/src/HOL/Transitive_Closure.thy Fri Oct 04 23:38:04 2024 +0200 +++ b/src/HOL/Transitive_Closure.thy Sat Oct 05 14:58:36 2024 +0200 @@ -64,32 +64,32 @@ tranclp (\(\notation=\postfix ++\\_^++)\ [1000] 1000) and reflclp (\(\notation=\postfix ==\\_^==)\ [1000] 1000) -bundle no_rtrancl_syntax +bundle rtrancl_syntax begin -no_notation +notation rtrancl (\(\notation=\postfix *\\_\<^sup>*)\ [1000] 999) and rtranclp (\(\notation=\postfix **\\_\<^sup>*\<^sup>*)\ [1000] 1000) -no_notation (ASCII) +notation (ASCII) rtrancl (\(\notation=\postfix *\\_^*)\ [1000] 999) and rtranclp (\(\notation=\postfix **\\_^**)\ [1000] 1000) end -bundle no_trancl_syntax +bundle trancl_syntax begin -no_notation +notation trancl (\(\notation=\postfix +\\_\<^sup>+)\ [1000] 999) and tranclp (\(\notation=\postfix ++\\_\<^sup>+\<^sup>+)\ [1000] 1000) -no_notation (ASCII) +notation (ASCII) trancl (\(\notation=\postfix +\\_^+)\ [1000] 999) and tranclp (\(\notation=\postfix ++\\_^++)\ [1000] 1000) end -bundle no_reflcl_syntax +bundle reflcl_syntax begin -no_notation +notation reflcl (\(\notation=\postfix =\\_\<^sup>=)\ [1000] 999) and reflclp (\(\notation=\postfix ==\\_\<^sup>=\<^sup>=)\ [1000] 1000) -no_notation (ASCII) +notation (ASCII) reflcl (\(\notation=\postfix =\\_^=)\ [1000] 999) and reflclp (\(\notation=\postfix ==\\_^==)\ [1000] 1000) end diff -r 7b3b27576f45 -r 0fb1e2dd4122 src/Pure/Isar/bundle.ML --- a/src/Pure/Isar/bundle.ML Fri Oct 04 23:38:04 2024 +0200 +++ b/src/Pure/Isar/bundle.ML Sat Oct 05 14:58:36 2024 +0200 @@ -6,21 +6,22 @@ signature BUNDLE = sig - type name = string + type name = bool * string + type xname = (bool * Position.T) * (xstring * Position.T) val bundle_space: Context.generic -> Name_Space.T val check: Proof.context -> xstring * Position.T -> string - val get: Proof.context -> name -> Attrib.thms - val read: Proof.context -> xstring * Position.T -> Attrib.thms + val check_name: Proof.context -> xname -> name + val get: Proof.context -> string -> Attrib.thms val extern: Proof.context -> string -> xstring val print_bundles: bool -> Proof.context -> unit val unbundle: name list -> local_theory -> local_theory - val unbundle_cmd: (xstring * Position.T) list -> local_theory -> local_theory + val unbundle_cmd: xname list -> local_theory -> local_theory val includes: name list -> Proof.context -> Proof.context - val includes_cmd: (xstring * Position.T) list -> Proof.context -> Proof.context + val includes_cmd: xname list -> Proof.context -> Proof.context val include_: name list -> Proof.state -> Proof.state - val include_cmd: (xstring * Position.T) list -> Proof.state -> Proof.state + val include_cmd: xname list -> Proof.state -> Proof.state val including: name list -> Proof.state -> Proof.state - val including_cmd: (xstring * Position.T) list -> Proof.state -> Proof.state + val including_cmd: xname list -> Proof.state -> Proof.state val bundle: {open_bundle: bool} -> binding * Attrib.thms -> (binding * typ option * mixfix) list -> local_theory -> local_theory val bundle_cmd: {open_bundle: bool} -> binding * (Facts.ref * Token.src list) list -> @@ -44,7 +45,8 @@ (* bundles *) -type name = string +type name = bool * string; +type xname = (bool * Position.T) * (xstring * Position.T); val get_all_generic = #1 o Data.get; val get_all = get_all_generic o Context.Proof; @@ -53,11 +55,12 @@ fun check ctxt = #1 o Name_Space.check (Context.Proof ctxt) (get_all ctxt); +fun check_name ctxt ((b: bool, pos), arg) = + (Context_Position.report ctxt pos Markup.quasi_keyword; (b, check ctxt arg)); + val get_global = Name_Space.get o get_all_generic o Context.Theory; val get = Name_Space.get o get_all_generic o Context.Proof; -fun read ctxt = get ctxt o check ctxt; - fun extern ctxt = Name_Space.extern ctxt (Name_Space.space_of_table (get_all ctxt)); @@ -109,11 +112,19 @@ (** open bundles **) -fun apply_bundle loc bundle ctxt = - let val notes = if loc then Local_Theory.notes else Attrib.local_notes "" in +fun polarity_decls b = + [([Drule.dummy_thm], + [Attrib.internal \<^here> (K (Thm.declaration_attribute (K (Syntax.set_polarity_generic b))))])]; + +fun apply_bundle loc (add, bundle) ctxt = + let + 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; + in ctxt |> Context_Position.set_visible false - |> notes [(Binding.empty_atts, bundle)] |> snd + |> notes [(Binding.empty_atts, polarity_decls add1 @ bundle @ polarity_decls add0)] |> snd |> Context_Position.restore_visible ctxt end; @@ -122,8 +133,8 @@ fun gen_unbundle loc prep args ctxt = let val thy = Proof_Context.theory_of ctxt; - val bundle = maps (prep ctxt) args |> transfer_bundle thy; - in apply_bundle loc bundle ctxt end; + val bundles = map (prep ctxt #> apsnd (get ctxt #> transfer_bundle thy)) args; + in fold (apply_bundle loc) bundles ctxt end; fun gen_includes prep = gen_unbundle false prep; @@ -135,17 +146,17 @@ in -val unbundle = gen_unbundle true get; -val unbundle_cmd = gen_unbundle true read; +val unbundle = gen_unbundle true (K I); +val unbundle_cmd = gen_unbundle true check_name; -val includes = gen_includes get; -val includes_cmd = gen_includes read; +val includes = gen_includes (K I); +val includes_cmd = gen_includes check_name; -val include_ = gen_include get; -val include_cmd = gen_include read; +val include_ = gen_include (K I); +val include_cmd = gen_include check_name; -val including = gen_including get; -val including_cmd = gen_including read; +val including = gen_including (K I); +val including_cmd = gen_including check_name; end; @@ -180,7 +191,7 @@ (fn phi => fn context => let val psi = Morphism.set_trim_context'' context phi in #2 (define_bundle (Morphism.binding psi binding, transform_bundle psi bundle) context) end) - |> open_bundle ? apply_bundle true bundle + |> open_bundle ? apply_bundle true (true, bundle) end; in diff -r 7b3b27576f45 -r 0fb1e2dd4122 src/Pure/Isar/class_declaration.ML --- a/src/Pure/Isar/class_declaration.ML Fri Oct 04 23:38:04 2024 +0200 +++ b/src/Pure/Isar/class_declaration.ML Sat Oct 05 14:58:36 2024 +0200 @@ -8,7 +8,7 @@ sig val class: binding -> Bundle.name list -> class list -> Element.context_i list -> theory -> string * local_theory - val class_cmd: binding -> (xstring * Position.T) list -> xstring list -> + val class_cmd: binding -> Bundle.xname list -> xstring list -> Element.context list -> theory -> string * local_theory val prove_subclass: tactic -> class -> local_theory -> local_theory @@ -263,7 +263,7 @@ in (((sups, supparam_names), (sup_sort, base_sort, supexpr)), (includes, elems, global_syntax)) end; val cert_class_spec = prep_class_spec (K I) (K I) cert_class_elems; -val read_class_spec = prep_class_spec Proof_Context.read_class Bundle.check read_class_elems; +val read_class_spec = prep_class_spec Proof_Context.read_class Bundle.check_name read_class_elems; (* class establishment *) diff -r 7b3b27576f45 -r 0fb1e2dd4122 src/Pure/Isar/expression.ML --- a/src/Pure/Isar/expression.ML Fri Oct 04 23:38:04 2024 +0200 +++ b/src/Pure/Isar/expression.ML Sat Oct 05 14:58:36 2024 +0200 @@ -34,7 +34,7 @@ * Element.context_i list * Proof.context) * ((string * typ) list * Proof.context) val add_locale: binding -> binding -> Bundle.name list -> expression_i -> Element.context_i list -> theory -> string * local_theory - val add_locale_cmd: binding -> binding -> (xstring * Position.T) list -> + val add_locale_cmd: binding -> binding -> Bundle.xname list -> expression -> Element.context list -> theory -> string * local_theory (* Processing of locale expressions *) @@ -874,7 +874,7 @@ in val add_locale = gen_add_locale (K I) cert_declaration; -val add_locale_cmd = gen_add_locale Bundle.check read_declaration; +val add_locale_cmd = gen_add_locale Bundle.check_name read_declaration; end; diff -r 7b3b27576f45 -r 0fb1e2dd4122 src/Pure/Isar/parse_spec.ML --- a/src/Pure/Isar/parse_spec.ML Fri Oct 04 23:38:04 2024 +0200 +++ b/src/Pure/Isar/parse_spec.ML Sat Oct 05 14:58:36 2024 +0200 @@ -17,9 +17,9 @@ val specification: ((binding * string option * mixfix) list * Specification.multi_specs_cmd) parser val constdecl: (binding * string option * mixfix) parser - val bundles: (xstring * Position.T) list parser - val includes: (xstring * Position.T) list parser - val opening: (xstring * Position.T) list parser + val bundles: Bundle.xname list parser + val includes: Bundle.xname list parser + val opening: Bundle.xname list parser val locale_fixes: (binding * string option * mixfix) list parser val locale_insts: (string option list * (Attrib.binding * string) list) parser val class_expression: string list parser @@ -84,7 +84,11 @@ (* bundles *) -val bundles = Parse.and_list1 Parse.name_position; +val bundle_polarity = + Scan.optional (Parse.position (Parse.reserved "no") >> (pair false o snd)) + (true, Position.none); + +val bundles = Parse.and_list1 (bundle_polarity -- Parse.name_position); val includes = Parse.$$$ "includes" |-- Parse.!!! bundles; diff -r 7b3b27576f45 -r 0fb1e2dd4122 src/Pure/Isar/proof_context.ML --- a/src/Pure/Isar/proof_context.ML Fri Oct 04 23:38:04 2024 +0200 +++ b/src/Pure/Isar/proof_context.ML Sat Oct 05 14:58:36 2024 +0200 @@ -1140,8 +1140,10 @@ else error ("Unknown syntax const: " ^ quote c ^ Position.here pos); fun syntax add mode args ctxt = - let val args' = map (pair Local_Syntax.Const) args - in ctxt |> map_syntax (#2 o Local_Syntax.update_modesyntax ctxt add mode args') end; + let + val add' = Syntax.effective_polarity ctxt add; + val args' = map (pair Local_Syntax.Const) args; + in ctxt |> map_syntax (#2 o Local_Syntax.update_modesyntax ctxt add' mode args') end; fun generic_syntax add mode args = Context.mapping (Sign.syntax_global add mode args) (syntax add mode args); @@ -1163,8 +1165,10 @@ | const_syntax _ _ = NONE; fun gen_notation make_syntax add mode args ctxt = - ctxt |> map_syntax_idents - (Local_Syntax.update_modesyntax ctxt add mode (map_filter (make_syntax ctxt) args)); + let + val add' = Syntax.effective_polarity ctxt add; + val args' = map_filter (make_syntax ctxt) args; + in ctxt |> map_syntax_idents (Local_Syntax.update_modesyntax ctxt add' mode args') end; in diff -r 7b3b27576f45 -r 0fb1e2dd4122 src/Pure/Isar/specification.ML --- a/src/Pure/Isar/specification.ML Fri Oct 04 23:38:04 2024 +0200 +++ b/src/Pure/Isar/specification.ML Sat Oct 05 14:58:36 2024 +0200 @@ -56,19 +56,19 @@ bool -> local_theory -> (string * thm list) list * local_theory val theorem: bool -> string -> Method.text option -> (thm list list -> local_theory -> local_theory) -> Attrib.binding -> - string list -> Element.context_i list -> Element.statement_i -> + Bundle.name list -> Element.context_i list -> Element.statement_i -> bool -> local_theory -> Proof.state val theorem_cmd: bool -> string -> Method.text option -> (thm list list -> local_theory -> local_theory) -> Attrib.binding -> - (xstring * Position.T) list -> Element.context list -> Element.statement -> + Bundle.xname list -> Element.context list -> Element.statement -> bool -> local_theory -> Proof.state val schematic_theorem: bool -> string -> Method.text option -> (thm list list -> local_theory -> local_theory) -> Attrib.binding -> - string list -> Element.context_i list -> Element.statement_i -> + Bundle.name list -> Element.context_i list -> Element.statement_i -> bool -> local_theory -> Proof.state val schematic_theorem_cmd: bool -> string -> Method.text option -> (thm list list -> local_theory -> local_theory) -> Attrib.binding -> - (xstring * Position.T) list -> Element.context list -> Element.statement -> + Bundle.xname list -> Element.context list -> Element.statement -> bool -> local_theory -> Proof.state end; diff -r 7b3b27576f45 -r 0fb1e2dd4122 src/Pure/Isar/target_context.ML --- a/src/Pure/Isar/target_context.ML Fri Oct 04 23:38:04 2024 +0200 +++ b/src/Pure/Isar/target_context.ML Sat Oct 05 14:58:36 2024 +0200 @@ -6,12 +6,12 @@ signature TARGET_CONTEXT = sig - val context_begin_named_cmd: (xstring * Position.T) list -> xstring * Position.T -> + val context_begin_named_cmd: Bundle.xname list -> xstring * Position.T -> theory -> local_theory val end_named_cmd: local_theory -> Context.generic val switch_named_cmd: (xstring * Position.T) option -> Context.generic -> (local_theory -> Context.generic) * local_theory - val context_begin_nested_cmd: (xstring * Position.T) list -> Element.context list -> + val context_begin_nested_cmd: Bundle.xname list -> Element.context list -> Context.generic -> local_theory val end_nested_cmd: local_theory -> Context.generic end; @@ -20,7 +20,7 @@ struct fun prep_includes thy = - map (Bundle.check (Proof_Context.init_global thy)); + map (Bundle.check_name (Proof_Context.init_global thy)); fun context_begin_named_cmd raw_includes ("-", _) thy = Named_Target.init (prep_includes thy raw_includes) "" thy @@ -44,7 +44,7 @@ end; fun includes raw_includes lthy = - Bundle.includes (map (Bundle.check lthy) raw_includes) lthy; + Bundle.includes (map (Bundle.check_name lthy) raw_includes) lthy; fun context_begin_nested_cmd raw_includes raw_elems gthy = gthy diff -r 7b3b27576f45 -r 0fb1e2dd4122 src/Pure/Syntax/syntax.ML --- a/src/Pure/Syntax/syntax.ML Fri Oct 04 23:38:04 2024 +0200 +++ b/src/Pure/Syntax/syntax.ML Sat Oct 05 14:58:36 2024 +0200 @@ -116,6 +116,10 @@ val update_consts: Proof.context -> (string * string list) list -> syntax -> syntax val update_trrules: Proof.context -> Ast.ast trrule list -> syntax -> syntax val remove_trrules: Proof.context -> Ast.ast trrule list -> syntax -> syntax + val get_polarity: Proof.context -> bool + val set_polarity: bool -> Proof.context -> Proof.context + val set_polarity_generic: bool -> Context.generic -> Context.generic + val effective_polarity: Proof.context -> bool -> bool val const: string -> term val free: string -> term val var: indexname -> term @@ -708,6 +712,8 @@ (** modify syntax **) +(* updates *) + fun update_trfuns ctxt = update_syntax mode_default o Syntax_Ext.syn_ext_trfuns ctxt; fun update_type_gram ctxt add prmode decls = @@ -723,6 +729,17 @@ fun remove_trrules ctxt = remove_syntax mode_default o Syntax_Ext.syn_ext_rules ctxt o check_rules; +(* polarity of declarations: true = add, false = del *) + +val polarity = Config.declare_bool ("polarity", Position.none) (K true); + +fun get_polarity ctxt = Config.get ctxt polarity; +val set_polarity = Config.put polarity; +val set_polarity_generic = Config.put_generic polarity; + +fun effective_polarity ctxt add = get_polarity ctxt = add; + + open Lexicon.Syntax; end; diff -r 7b3b27576f45 -r 0fb1e2dd4122 src/Pure/sign.ML --- a/src/Pure/sign.ML Fri Oct 04 23:38:04 2024 +0200 +++ b/src/Pure/sign.ML Sat Oct 05 14:58:36 2024 +0200 @@ -393,27 +393,32 @@ in thy |> map_syn (Syntax.update_const_gram ctxt add (logical_types thy) mode (map prep args)) end; fun syntax_global add mode args thy = - syntax (Proof_Context.init_global thy) add mode args thy; + let + val thy_ctxt = Proof_Context.init_global thy; + val add' = Syntax.effective_polarity thy_ctxt add; + in syntax thy_ctxt add' mode args thy end; val syntax_deps = update_syn_global Syntax.update_consts; fun type_notation_global add mode args thy = let val thy_ctxt = Proof_Context.init_global thy; + val add' = Syntax.effective_polarity thy_ctxt add; fun type_syntax (Type (c, args), mx) = SOME (Lexicon.mark_type c, Mixfix.make_type (length args), mx) | type_syntax _ = NONE; - in map_syn (Syntax.update_type_gram thy_ctxt add mode (map_filter type_syntax args)) thy end; + in map_syn (Syntax.update_type_gram thy_ctxt add' mode (map_filter type_syntax args)) thy end; fun notation_global add mode args thy = let val thy_ctxt = Proof_Context.init_global thy; + val add' = Syntax.effective_polarity thy_ctxt add; fun const_syntax (Const (c, _), mx) = (case try (Consts.type_scheme (consts_of thy)) c of SOME T => SOME (Lexicon.mark_const c, T, mx) | NONE => NONE) | const_syntax _ = NONE; - in syntax thy_ctxt add mode (map_filter const_syntax args) thy end; + in syntax thy_ctxt add' mode (map_filter const_syntax args) thy end; (* add constants *)