# HG changeset patch # User wenzelm # Date 1395396399 -3600 # Node ID 938c6c7e10ebb29b8e59e26960a8975cde942045 # Parent 17df7145a871044e3467ff1aea5e7dd7f63f9dc4 tuned signature; diff -r 17df7145a871 -r 938c6c7e10eb src/Doc/Codegen/Setup.thy --- a/src/Doc/Codegen/Setup.thy Fri Mar 21 10:45:03 2014 +0100 +++ b/src/Doc/Codegen/Setup.thy Fri Mar 21 11:06:39 2014 +0100 @@ -19,10 +19,10 @@ let val typ = Simple_Syntax.read_typ; in - Sign.del_modesyntax (Symbol.xsymbolsN, false) + Sign.del_syntax (Symbol.xsymbolsN, false) [("_constrain", typ "logic => type => logic", Mixfix ("_\_", [4, 0], 3)), ("_constrain", typ "prop' => type => prop'", Mixfix ("_\_", [4, 0], 3))] #> - Sign.add_modesyntax (Symbol.xsymbolsN, false) + Sign.add_syntax (Symbol.xsymbolsN, false) [("_constrain", typ "logic => type => logic", Mixfix ("_ \ _", [4, 0], 3)), ("_constrain", typ "prop' => type => prop'", Mixfix ("_ \ _", [4, 0], 3))] end diff -r 17df7145a871 -r 938c6c7e10eb src/HOL/Imperative_HOL/Overview.thy --- a/src/HOL/Imperative_HOL/Overview.thy Fri Mar 21 10:45:03 2014 +0100 +++ b/src/HOL/Imperative_HOL/Overview.thy Fri Mar 21 11:06:39 2014 +0100 @@ -12,10 +12,10 @@ let val typ = Simple_Syntax.read_typ; in - Sign.del_modesyntax (Symbol.xsymbolsN, false) + Sign.del_syntax (Symbol.xsymbolsN, false) [("_constrain", typ "logic => type => logic", Mixfix ("_\_", [4, 0], 3)), ("_constrain", typ "prop' => type => prop'", Mixfix ("_\_", [4, 0], 3))] #> - Sign.add_modesyntax (Symbol.xsymbolsN, false) + Sign.add_syntax (Symbol.xsymbolsN, false) [("_constrain", typ "logic => type => logic", Mixfix ("_ \ _", [4, 0], 3)), ("_constrain", typ "prop' => type => prop'", Mixfix ("_ \ _", [4, 0], 3))] end diff -r 17df7145a871 -r 938c6c7e10eb src/Pure/Isar/isar_syn.ML --- a/src/Pure/Isar/isar_syn.ML Fri Mar 21 10:45:03 2014 +0100 +++ b/src/Pure/Isar/isar_syn.ML Fri Mar 21 11:06:39 2014 +0100 @@ -120,12 +120,12 @@ val _ = Outer_Syntax.command @{command_spec "syntax"} "add raw syntax clauses" (opt_mode -- Scan.repeat1 Parse.const_decl - >> (Toplevel.theory o uncurry Sign.add_modesyntax_cmd)); + >> (Toplevel.theory o uncurry Sign.add_syntax_cmd)); val _ = Outer_Syntax.command @{command_spec "no_syntax"} "delete raw syntax clauses" (opt_mode -- Scan.repeat1 Parse.const_decl - >> (Toplevel.theory o uncurry Sign.del_modesyntax_cmd)); + >> (Toplevel.theory o uncurry Sign.del_syntax_cmd)); (* translations *) diff -r 17df7145a871 -r 938c6c7e10eb src/Pure/Proof/proof_syntax.ML --- a/src/Pure/Proof/proof_syntax.ML Fri Mar 21 10:45:03 2014 +0100 +++ b/src/Pure/Proof/proof_syntax.ML Fri Mar 21 11:06:39 2014 +0100 @@ -54,7 +54,7 @@ ((Binding.name "OfClass", (Term.a_itselfT --> propT) --> proofT), NoSyn), ((Binding.name "MinProof", proofT), Delimfix "?")] |> Sign.add_nonterminals_global [Binding.name "param", Binding.name "params"] - |> Sign.add_syntax + |> Sign.add_syntax Syntax.mode_default [("_Lam", [paramsT, proofT] ---> proofT, Mixfix ("(1Lam _./ _)", [0, 3], 3)), ("_Lam0", [paramT, paramsT] ---> paramsT, Mixfix ("_/ _", [1, 0], 0)), ("_Lam0", [idtT, paramsT] ---> paramsT, Mixfix ("_/ _", [1, 0], 0)), @@ -62,7 +62,7 @@ ("", paramT --> paramT, Delimfix "'(_')"), ("", idtT --> paramsT, Delimfix "_"), ("", paramT --> paramsT, Delimfix "_")] - |> Sign.add_modesyntax (Symbol.xsymbolsN, true) + |> Sign.add_syntax (Symbol.xsymbolsN, true) [("_Lam", [paramsT, proofT] ---> proofT, Mixfix ("(1\<^bold>\_./ _)", [0, 3], 3)), (Lexicon.mark_const "Appt", [proofT, aT] ---> proofT, Mixfix ("(1_ \/ _)", [4, 5], 4)), (Lexicon.mark_const "AppP", [proofT, proofT] ---> proofT, Mixfix ("(1_ \/ _)", [4, 5], 4))] diff -r 17df7145a871 -r 938c6c7e10eb src/Pure/pure_thy.ML --- a/src/Pure/pure_thy.ML Fri Mar 21 10:45:03 2014 +0100 +++ b/src/Pure/pure_thy.ML Fri Mar 21 11:06:39 2014 +0100 @@ -49,8 +49,8 @@ val old_appl_syntax_setup = Old_Appl_Syntax.put true #> - Sign.del_modesyntax Syntax.mode_default applC_syntax #> - Sign.add_syntax appl_syntax; + Sign.del_syntax Syntax.mode_default applC_syntax #> + Sign.add_syntax Syntax.mode_default appl_syntax; (* main content *) @@ -75,8 +75,8 @@ "tvar_position", "id_position", "longid_position", "var_position", "str_position", "string_position", "cartouche_position", "type_name", "class_name"])) - #> Sign.add_syntax (map (fn x => (x, typ "'a", NoSyn)) token_markers) - #> Sign.add_syntax + #> Sign.add_syntax Syntax.mode_default (map (fn x => (x, typ "'a", NoSyn)) token_markers) + #> Sign.add_syntax Syntax.mode_default [("", typ "prop' => prop", Delimfix "_"), ("", typ "logic => any", Delimfix "_"), ("", typ "prop' => any", Delimfix "_"), @@ -174,8 +174,8 @@ ("_sort_constraint", typ "type => prop", Delimfix "(1SORT'_CONSTRAINT/(1'(_')))"), (const "Pure.term", typ "logic => prop", Delimfix "TERM _"), (const "Pure.conjunction", typ "prop => prop => prop", Infixr ("&&&", 2))] - #> Sign.add_syntax applC_syntax - #> Sign.add_modesyntax (Symbol.xsymbolsN, true) + #> Sign.add_syntax Syntax.mode_default applC_syntax + #> Sign.add_syntax (Symbol.xsymbolsN, true) [(tycon "fun", typ "type => type => type", Mixfix ("(_/ \\ _)", [1, 0], 0)), ("_bracket", typ "types => type => type", Mixfix ("([_]/ \\ _)", [0, 0], 0)), ("_ofsort", typ "tid_position => sort => type", Mixfix ("_\\_", [1000, 0], 1000)), @@ -190,9 +190,9 @@ ("_DDDOT", typ "aprop", Delimfix "\\"), ("_bigimpl", typ "asms => prop => prop", Mixfix ("((1\\_\\)/ \\ _)", [0, 1], 1)), ("_DDDOT", typ "logic", Delimfix "\\")] - #> Sign.add_modesyntax ("", false) + #> Sign.add_syntax ("", false) [(const "prop", typ "prop => prop", Mixfix ("_", [0], 0))] - #> Sign.add_modesyntax ("HTML", false) + #> Sign.add_syntax ("HTML", false) [("_lambda", typ "pttrns => 'a => logic", Mixfix ("(3\\_./ _)", [0, 3], 3))] #> Sign.add_consts [(Binding.name "==", typ "'a => 'a => prop", Infix ("==", 2)), diff -r 17df7145a871 -r 938c6c7e10eb src/Pure/sign.ML --- a/src/Pure/sign.ML Fri Mar 21 10:45:03 2014 +0100 +++ b/src/Pure/sign.ML Fri Mar 21 11:06:39 2014 +0100 @@ -73,12 +73,10 @@ 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: (string * typ * mixfix) list -> theory -> theory - val add_syntax_cmd: (string * string * mixfix) list -> theory -> theory - val add_modesyntax: Syntax.mode -> (string * typ * mixfix) list -> theory -> theory - val add_modesyntax_cmd: Syntax.mode -> (string * string * mixfix) list -> theory -> theory - val del_modesyntax: Syntax.mode -> (string * typ * mixfix) list -> theory -> theory - val del_modesyntax_cmd: Syntax.mode -> (string * string * mixfix) list -> 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 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 @@ -375,12 +373,10 @@ fun gen_add_syntax x = gen_syntax (Syntax.update_const_gram true) x; -val add_modesyntax = gen_add_syntax (K I); -val add_modesyntax_cmd = gen_add_syntax Syntax.read_typ; -val add_syntax = add_modesyntax Syntax.mode_default; -val add_syntax_cmd = add_modesyntax_cmd Syntax.mode_default; -val del_modesyntax = gen_syntax (Syntax.update_const_gram false) (K I); -val del_modesyntax_cmd = gen_syntax (Syntax.update_const_gram false) Syntax.read_typ; +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; fun type_notation add mode args = let @@ -417,7 +413,7 @@ in thy |> map_consts (fold (Consts.declare (inherit_naming thy ctxt) o #1) args) - |> add_syntax (map #2 args) + |> add_syntax Syntax.mode_default (map #2 args) |> pair (map #3 args) end;