--- 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 *)
--- 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
--- 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 *)
--- 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) *)
--- 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_ \<cdot>/ _)", [4, 5], 4)),
(Lexicon.mark_const "Pure.AppP", [proofT, proofT] ---> proofT, mixfix ("(1_ \<bullet>/ _)", [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"],
--- 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>\<open>translations\<close> "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>\<open>no_translations\<close> "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\<close>
--- 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 *)
--- 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 *)