# HG changeset patch # User wenzelm # Date 1734194153 -3600 # Node ID e656c5edc35223214cdf3540a14726e761c983b4 # Parent fcf44ef51057269c2574b6dcca8f0c6ed373f0db clarified signature; diff -r fcf44ef51057 -r e656c5edc352 src/HOL/HOLCF/Tools/Domain/domain_constructors.ML --- a/src/HOL/HOLCF/Tools/Domain/domain_constructors.ML Sat Dec 14 16:58:53 2024 +0100 +++ b/src/HOL/HOLCF/Tools/Domain/domain_constructors.ML Sat Dec 14 17:35:53 2024 +0100 @@ -488,7 +488,7 @@ Syntax.Parse_Rule (case_trans true false) :: abscon_trans false @ abscon_trans true in - val thy = Sign.add_trrules trans_rules thy + val thy = Sign.translations_global true trans_rules thy end (* prove beta reduction rule for case combinator *) diff -r fcf44ef51057 -r e656c5edc352 src/HOL/HOLCF/Tools/cont_consts.ML --- a/src/HOL/HOLCF/Tools/cont_consts.ML Sat Dec 14 16:58:53 2024 +0100 +++ b/src/HOL/HOLCF/Tools/cont_consts.ML Sat Dec 14 17:35:53 2024 +0100 @@ -57,7 +57,7 @@ thy |> Sign.add_consts (normal_decls @ map #1 transformed_decls) |> Sign.syntax_global true Syntax.mode_default (map #2 transformed_decls) - |> Sign.add_trrules (maps #3 transformed_decls) + |> Sign.translations_global true (maps #3 transformed_decls) end val add_consts = gen_add_consts Sign.certify_typ diff -r fcf44ef51057 -r e656c5edc352 src/HOL/HOLCF/ex/Pattern_Match.thy --- a/src/HOL/HOLCF/ex/Pattern_Match.thy Sat Dec 14 16:58:53 2024 +0100 +++ b/src/HOL/HOLCF/ex/Pattern_Match.thy Sat Dec 14 17:35:53 2024 +0100 @@ -522,7 +522,7 @@ val trans_rules : Ast.ast Syntax.trrule list = maps one_case_trans (pat_consts ~~ spec); in - val thy = Sign.add_trrules trans_rules thy; + val thy = Sign.translations_global true trans_rules thy; end; (* prove strictness and reduction rules of pattern combinators *) diff -r fcf44ef51057 -r e656c5edc352 src/Pure/Isar/isar_cmd.ML --- a/src/Pure/Isar/isar_cmd.ML Sat Dec 14 16:58:53 2024 +0100 +++ b/src/Pure/Isar/isar_cmd.ML Sat Dec 14 17:35:53 2024 +0100 @@ -13,8 +13,7 @@ val print_translation: Input.source -> theory -> theory val typed_print_translation: Input.source -> theory -> theory val print_ast_translation: Input.source -> theory -> theory - val translations: (xstring * string) Syntax.trrule list -> theory -> theory - val no_translations: (xstring * string) Syntax.trrule list -> theory -> theory + val translations: bool -> (string * string) Syntax.trrule list -> theory -> theory val syntax_consts: ((string * Position.T) list * (xstring * Position.T) list) list -> theory -> theory val syntax_types: ((string * Position.T) list * (xstring * Position.T) list) list -> @@ -98,10 +97,11 @@ (* translation rules *) -val read_trrules = map o Syntax.parse_trrule o Proof_Context.init_global; - -fun translations args thy = Sign.add_trrules (read_trrules thy args) thy; -fun no_translations args thy = Sign.del_trrules (read_trrules thy args) thy; +fun translations add raw_rules thy = + let + val thy_ctxt = Proof_Context.init_global thy; + val rules = map (Syntax.parse_trrule thy_ctxt) raw_rules; + in Sign.translations_global add rules thy end; (* syntax consts/types (after translation) *) diff -r fcf44ef51057 -r e656c5edc352 src/Pure/Proof/proof_syntax.ML --- a/src/Pure/Proof/proof_syntax.ML Sat Dec 14 16:58:53 2024 +0100 +++ b/src/Pure/Proof/proof_syntax.ML Sat Dec 14 17:35:53 2024 +0100 @@ -57,7 +57,7 @@ (Lexicon.mark_const "Pure.Appt", [proofT, aT] ---> proofT, mixfix ("(1_ \/ _)", [4, 5], 4)), (Lexicon.mark_const "Pure.AppP", [proofT, proofT] ---> proofT, mixfix ("(1_ \/ _)", [4, 5], 4)), (Lexicon.mark_const "Pure.MinProof", proofT, Mixfix.mixfix "\<^bold>?")] - |> Sign.add_trrules (map Syntax.Parse_Print_Rule + |> Sign.translations_global true (map Syntax.Parse_Print_Rule [(Ast.mk_appl (Ast.Constant "_Lam") [Ast.mk_appl (Ast.Constant "_Lam0") [Ast.Variable "l", Ast.Variable "m"], Ast.Variable "A"], diff -r fcf44ef51057 -r e656c5edc352 src/Pure/Pure.thy --- a/src/Pure/Pure.thy Sat Dec 14 16:58:53 2024 +0100 +++ b/src/Pure/Pure.thy Sat Dec 14 17:35:53 2024 +0100 @@ -431,11 +431,11 @@ val _ = Outer_Syntax.command \<^command_keyword>\translations\ "add syntax translation rules" - (Scan.repeat1 trans_line >> (Toplevel.theory o Isar_Cmd.translations)); + (Scan.repeat1 trans_line >> (Toplevel.theory o Isar_Cmd.translations true)); val _ = Outer_Syntax.command \<^command_keyword>\no_translations\ "delete syntax translation rules" - (Scan.repeat1 trans_line >> (Toplevel.theory o Isar_Cmd.no_translations)); + (Scan.repeat1 trans_line >> (Toplevel.theory o Isar_Cmd.translations false)); in end\ diff -r fcf44ef51057 -r e656c5edc352 src/Pure/Syntax/syntax.ML --- a/src/Pure/Syntax/syntax.ML Sat Dec 14 16:58:53 2024 +0100 +++ b/src/Pure/Syntax/syntax.ML Sat Dec 14 17:35:53 2024 +0100 @@ -116,8 +116,7 @@ val update_const_gram: Proof.context -> bool -> string list -> mode -> (string * typ * mixfix) list -> syntax -> syntax 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 update_trrules: Proof.context -> bool -> 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 @@ -774,8 +773,9 @@ val update_consts = update_syntax mode_default oo Syntax_Ext.syn_ext_consts; -fun update_trrules ctxt = update_syntax mode_default o Syntax_Ext.syn_ext_rules ctxt o check_rules; -fun remove_trrules ctxt = remove_syntax mode_default o Syntax_Ext.syn_ext_rules ctxt o check_rules; +fun update_trrules ctxt add = + (if add then update_syntax else remove_syntax) mode_default o + Syntax_Ext.syn_ext_rules ctxt o check_rules; (* polarity of declarations: true = add, false = del *) diff -r fcf44ef51057 -r e656c5edc352 src/Pure/sign.ML --- a/src/Pure/sign.ML Sat Dec 14 16:58:53 2024 +0100 +++ b/src/Pure/sign.ML Sat Dec 14 17:35:53 2024 +0100 @@ -102,8 +102,7 @@ (string * (Proof.context -> typ -> term list -> term)) list -> theory -> theory val print_ast_translation: (string * (Proof.context -> Ast.ast list -> Ast.ast)) list -> theory -> theory - val add_trrules: Ast.ast Syntax.trrule list -> theory -> theory - val del_trrules: Ast.ast Syntax.trrule list -> theory -> theory + val translations_global: bool -> Ast.ast Syntax.trrule list -> theory -> theory val get_scope: theory -> Binding.scope option val new_scope: theory -> Binding.scope * theory val new_group: theory -> theory @@ -519,8 +518,7 @@ (* translation rules *) -val add_trrules = update_syn_global Syntax.update_trrules; -val del_trrules = update_syn_global Syntax.remove_trrules; +fun translations_global add = update_syn_global (fn ctxt => Syntax.update_trrules ctxt add); (* naming *)