--- a/src/Pure/Proof/proof_syntax.ML Mon Sep 20 15:27:00 2021 +0200
+++ b/src/Pure/Proof/proof_syntax.ML Mon Sep 20 20:22:32 2021 +0200
@@ -46,7 +46,7 @@
|> Sign.add_nonterminals_global
[Binding.make ("param", \<^here>),
Binding.make ("params", \<^here>)]
- |> Sign.add_syntax Syntax.mode_default
+ |> Sign.syntax true Syntax.mode_default
[("_Lam", [paramsT, proofT] ---> proofT, mixfix ("(1\<^bold>\<lambda>_./ _)", [0, 3], 3)),
("_Lam0", [paramT, paramsT] ---> paramsT, mixfix ("_/ _", [1, 0], 0)),
("_Lam0", [idtT, paramsT] ---> paramsT, mixfix ("_/ _", [1, 0], 0)),
--- a/src/Pure/Pure.thy Mon Sep 20 15:27:00 2021 +0200
+++ b/src/Pure/Pure.thy Mon Sep 20 20:22:32 2021 +0200
@@ -386,12 +386,12 @@
val _ =
Outer_Syntax.command \<^command_keyword>\<open>syntax\<close> "add raw syntax clauses"
(Parse.syntax_mode -- Scan.repeat1 Parse.const_decl
- >> (Toplevel.theory o uncurry Sign.add_syntax_cmd));
+ >> (Toplevel.theory o uncurry (Sign.syntax_cmd true)));
val _ =
Outer_Syntax.command \<^command_keyword>\<open>no_syntax\<close> "delete raw syntax clauses"
(Parse.syntax_mode -- Scan.repeat1 Parse.const_decl
- >> (Toplevel.theory o uncurry Sign.del_syntax_cmd));
+ >> (Toplevel.theory o uncurry (Sign.syntax_cmd false)));
val trans_pat =
Scan.optional
--- a/src/Pure/pure_thy.ML Mon Sep 20 15:27:00 2021 +0200
+++ b/src/Pure/pure_thy.ML Mon Sep 20 20:22:32 2021 +0200
@@ -68,8 +68,8 @@
val old_appl_syntax_setup =
Old_Appl_Syntax.put true #>
- Sign.del_syntax Syntax.mode_default applC_syntax #>
- Sign.add_syntax Syntax.mode_default appl_syntax;
+ Sign.syntax false Syntax.mode_default applC_syntax #>
+ Sign.syntax true Syntax.mode_default appl_syntax;
(* main content *)
@@ -100,8 +100,8 @@
"tvar_position", "id_position", "longid_position", "var_position",
"str_position", "string_position", "cartouche_position", "type_name",
"class_name"]))
- #> Sign.add_syntax Syntax.mode_default (map (fn x => (x, typ "'a", NoSyn)) token_markers)
- #> Sign.add_syntax Syntax.mode_default
+ #> Sign.syntax true Syntax.mode_default (map (fn x => (x, typ "'a", NoSyn)) token_markers)
+ #> Sign.syntax true Syntax.mode_default
[("", typ "prop' \<Rightarrow> prop", Mixfix.mixfix "_"),
("", typ "logic \<Rightarrow> any", Mixfix.mixfix "_"),
("", typ "prop' \<Rightarrow> any", Mixfix.mixfix "_"),
@@ -197,8 +197,8 @@
("_sort_constraint", typ "type \<Rightarrow> prop", Mixfix.mixfix "(1SORT'_CONSTRAINT/(1'(_')))"),
(const "Pure.term", typ "logic \<Rightarrow> prop", Mixfix.mixfix "TERM _"),
(const "Pure.conjunction", typ "prop \<Rightarrow> prop \<Rightarrow> prop", infixr_ ("&&&", 2))]
- #> Sign.add_syntax Syntax.mode_default applC_syntax
- #> Sign.add_syntax (Print_Mode.ASCII, true)
+ #> Sign.syntax true Syntax.mode_default applC_syntax
+ #> Sign.syntax true (Print_Mode.ASCII, true)
[(tycon "fun", typ "type \<Rightarrow> type \<Rightarrow> type", mixfix ("(_/ => _)", [1, 0], 0)),
("_bracket", typ "types \<Rightarrow> type \<Rightarrow> type", mixfix ("([_]/ => _)", [0, 0], 0)),
("_lambda", typ "pttrns \<Rightarrow> 'a \<Rightarrow> logic", mixfix ("(3%_./ _)", [0, 3], 3)),
@@ -208,7 +208,7 @@
("_DDDOT", typ "aprop", Mixfix.mixfix "..."),
("_bigimpl", typ "asms \<Rightarrow> prop \<Rightarrow> prop", mixfix ("((3[| _ |])/ ==> _)", [0, 1], 1)),
("_DDDOT", typ "logic", Mixfix.mixfix "...")]
- #> Sign.add_syntax ("", false)
+ #> Sign.syntax true ("", false)
[(const "Pure.prop", typ "prop \<Rightarrow> prop", mixfix ("_", [0], 0))]
#> Sign.add_consts
[(qualify (Binding.make ("eq", \<^here>)), typ "'a \<Rightarrow> 'a \<Rightarrow> prop", infix_ ("\<equiv>", 2)),
--- a/src/Pure/sign.ML Mon Sep 20 15:27:00 2021 +0200
+++ b/src/Pure/sign.ML Mon Sep 20 20:22:32 2021 +0200
@@ -72,10 +72,8 @@
val add_nonterminals: Proof.context -> binding list -> theory -> theory
val add_nonterminals_global: binding list -> theory -> theory
val add_type_abbrev: Proof.context -> binding * string list * typ -> theory -> theory
- val add_syntax: Syntax.mode -> (string * typ * mixfix) list -> theory -> theory
- val add_syntax_cmd: Syntax.mode -> (string * string * mixfix) list -> theory -> theory
- val del_syntax: Syntax.mode -> (string * typ * mixfix) list -> theory -> theory
- val del_syntax_cmd: Syntax.mode -> (string * string * mixfix) list -> theory -> theory
+ val syntax: bool -> Syntax.mode -> (string * typ * mixfix) list -> theory -> theory
+ val syntax_cmd: bool -> Syntax.mode -> (string * string * mixfix) list -> theory -> theory
val type_notation: bool -> Syntax.mode -> (typ * mixfix) list -> theory -> theory
val notation: bool -> Syntax.mode -> (term * mixfix) list -> theory -> theory
val declare_const: Proof.context -> (binding * typ) * mixfix -> theory -> term * theory
@@ -369,19 +367,15 @@
(* modify syntax *)
-fun gen_syntax change_gram parse_typ mode args thy =
+fun gen_syntax parse_typ add mode args thy =
let
val ctxt = Type.set_mode Type.mode_syntax (Proof_Context.init_global thy);
fun prep (c, T, mx) = (c, certify_typ_mode Type.mode_syntax thy (parse_typ ctxt T), mx)
handle ERROR msg => cat_error msg ("in syntax declaration " ^ quote c);
- in thy |> map_syn (change_gram (logical_types thy) mode (map prep args)) end;
-
-fun gen_add_syntax x = gen_syntax (Syntax.update_const_gram true) x;
+ in thy |> map_syn (Syntax.update_const_gram add (logical_types thy) mode (map prep args)) end;
-val add_syntax = gen_add_syntax (K I);
-val add_syntax_cmd = gen_add_syntax Syntax.read_typ;
-val del_syntax = gen_syntax (Syntax.update_const_gram false) (K I);
-val del_syntax_cmd = gen_syntax (Syntax.update_const_gram false) Syntax.read_typ;
+val syntax = gen_syntax (K I);
+val syntax_cmd = gen_syntax Syntax.read_typ;
fun type_notation add mode args =
let
@@ -397,7 +391,7 @@
SOME T => SOME (Lexicon.mark_const c, T, mx)
| NONE => NONE)
| const_syntax _ = NONE;
- in gen_syntax (Syntax.update_const_gram add) (K I) mode (map_filter const_syntax args) thy end;
+ in syntax add mode (map_filter const_syntax args) thy end;
(* add constants *)
@@ -418,7 +412,7 @@
in
thy
|> map_consts (fold (Consts.declare (inherit_naming thy ctxt) o #1) args)
- |> add_syntax Syntax.mode_default (map #2 args)
+ |> syntax true Syntax.mode_default (map #2 args)
|> pair (map #3 args)
end;