--- 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 ("_\<Colon>_", [4, 0], 3)),
("_constrain", typ "prop' => type => prop'", Mixfix ("_\<Colon>_", [4, 0], 3))] #>
- Sign.add_modesyntax (Symbol.xsymbolsN, false)
+ Sign.add_syntax (Symbol.xsymbolsN, false)
[("_constrain", typ "logic => type => logic", Mixfix ("_ \<Colon> _", [4, 0], 3)),
("_constrain", typ "prop' => type => prop'", Mixfix ("_ \<Colon> _", [4, 0], 3))]
end
--- 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 ("_\<Colon>_", [4, 0], 3)),
("_constrain", typ "prop' => type => prop'", Mixfix ("_\<Colon>_", [4, 0], 3))] #>
- Sign.add_modesyntax (Symbol.xsymbolsN, false)
+ Sign.add_syntax (Symbol.xsymbolsN, false)
[("_constrain", typ "logic => type => logic", Mixfix ("_ \<Colon> _", [4, 0], 3)),
("_constrain", typ "prop' => type => prop'", Mixfix ("_ \<Colon> _", [4, 0], 3))]
end
--- 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 *)
--- 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>\<lambda>_./ _)", [0, 3], 3)),
(Lexicon.mark_const "Appt", [proofT, aT] ---> proofT, Mixfix ("(1_ \<cdot>/ _)", [4, 5], 4)),
(Lexicon.mark_const "AppP", [proofT, proofT] ---> proofT, Mixfix ("(1_ \<bullet>/ _)", [4, 5], 4))]
--- 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 ("(_/ \\<Rightarrow> _)", [1, 0], 0)),
("_bracket", typ "types => type => type", Mixfix ("([_]/ \\<Rightarrow> _)", [0, 0], 0)),
("_ofsort", typ "tid_position => sort => type", Mixfix ("_\\<Colon>_", [1000, 0], 1000)),
@@ -190,9 +190,9 @@
("_DDDOT", typ "aprop", Delimfix "\\<dots>"),
("_bigimpl", typ "asms => prop => prop", Mixfix ("((1\\<lbrakk>_\\<rbrakk>)/ \\<Longrightarrow> _)", [0, 1], 1)),
("_DDDOT", typ "logic", Delimfix "\\<dots>")]
- #> 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\\<lambda>_./ _)", [0, 3], 3))]
#> Sign.add_consts
[(Binding.name "==", typ "'a => 'a => prop", Infix ("==", 2)),
--- 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;