# HG changeset patch # User wenzelm # Date 1632162152 -7200 # Node ID d882abae33790ec0ff229fc99422349f60af6519 # Parent 9dca3df78b6af1512228165217dd863ba9335e5a clarified signature; diff -r 9dca3df78b6a -r d882abae3379 src/Pure/Proof/proof_syntax.ML --- 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>\_./ _)", [0, 3], 3)), ("_Lam0", [paramT, paramsT] ---> paramsT, mixfix ("_/ _", [1, 0], 0)), ("_Lam0", [idtT, paramsT] ---> paramsT, mixfix ("_/ _", [1, 0], 0)), diff -r 9dca3df78b6a -r d882abae3379 src/Pure/Pure.thy --- 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>\syntax\ "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>\no_syntax\ "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 diff -r 9dca3df78b6a -r d882abae3379 src/Pure/pure_thy.ML --- 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' \ prop", Mixfix.mixfix "_"), ("", typ "logic \ any", Mixfix.mixfix "_"), ("", typ "prop' \ any", Mixfix.mixfix "_"), @@ -197,8 +197,8 @@ ("_sort_constraint", typ "type \ prop", Mixfix.mixfix "(1SORT'_CONSTRAINT/(1'(_')))"), (const "Pure.term", typ "logic \ prop", Mixfix.mixfix "TERM _"), (const "Pure.conjunction", typ "prop \ prop \ 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 \ type \ type", mixfix ("(_/ => _)", [1, 0], 0)), ("_bracket", typ "types \ type \ type", mixfix ("([_]/ => _)", [0, 0], 0)), ("_lambda", typ "pttrns \ 'a \ logic", mixfix ("(3%_./ _)", [0, 3], 3)), @@ -208,7 +208,7 @@ ("_DDDOT", typ "aprop", Mixfix.mixfix "..."), ("_bigimpl", typ "asms \ prop \ prop", mixfix ("((3[| _ |])/ ==> _)", [0, 1], 1)), ("_DDDOT", typ "logic", Mixfix.mixfix "...")] - #> Sign.add_syntax ("", false) + #> Sign.syntax true ("", false) [(const "Pure.prop", typ "prop \ prop", mixfix ("_", [0], 0))] #> Sign.add_consts [(qualify (Binding.make ("eq", \<^here>)), typ "'a \ 'a \ prop", infix_ ("\", 2)), diff -r 9dca3df78b6a -r d882abae3379 src/Pure/sign.ML --- 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;