--- a/src/HOL/Library/OptionalSugar.thy Fri Apr 08 21:03:20 2011 +0200
+++ b/src/HOL/Library/OptionalSugar.thy Fri Apr 08 21:11:29 2011 +0200
@@ -68,10 +68,10 @@
val classesT = Type ("classes", []); (*FIXME*)
in
Sign.add_modesyntax_i (Symbol.xsymbolsN, false) [
- ("_topsort", sortT, Mixfix ("\<top>", [], Syntax.max_pri)),
- ("_sort", classesT --> sortT, Mixfix ("'(_')", [], Syntax.max_pri)),
- ("_classes", Lexicon.idT --> classesT --> classesT, Mixfix ("_ \<inter> _", [], Syntax.max_pri)),
- ("_classes", Lexicon.longidT --> classesT --> classesT, Mixfix ("_ \<inter> _", [], Syntax.max_pri))
+ ("_topsort", sortT, Mixfix ("\<top>", [], 1000)),
+ ("_sort", classesT --> sortT, Mixfix ("'(_')", [], 1000)),
+ ("_classes", Lexicon.idT --> classesT --> classesT, Mixfix ("_ \<inter> _", [], 1000)),
+ ("_classes", Lexicon.longidT --> classesT --> classesT, Mixfix ("_ \<inter> _", [], 1000))
]
end
*}
--- a/src/HOL/Tools/Datatype/datatype_data.ML Fri Apr 08 21:03:20 2011 +0200
+++ b/src/HOL/Tools/Datatype/datatype_data.ML Fri Apr 08 21:11:29 2011 +0200
@@ -243,8 +243,7 @@
val thy = ProofContext.theory_of ctxt;
val (vs, cos) = the_spec thy dtco;
val ty = Type (dtco, map TFree vs);
- val pretty_typ_bracket =
- Syntax.pretty_typ (Config.put pretty_priority (Syntax.max_pri + 1) ctxt);
+ val pretty_typ_bracket = Syntax.pretty_typ (Config.put pretty_priority 1001 ctxt);
fun pretty_constr (co, tys) =
Pretty.block (Pretty.breaks
(Syntax.pretty_term ctxt (Const (co, tys ---> ty)) ::
--- a/src/Pure/Isar/parse.ML Fri Apr 08 21:03:20 2011 +0200
+++ b/src/Pure/Isar/parse.ML Fri Apr 08 21:11:29 2011 +0200
@@ -272,7 +272,7 @@
val mfix = string --
!!! (Scan.optional ($$$ "[" |-- !!! (list nat --| $$$ "]")) [] --
- Scan.optional nat Syntax.max_pri) >> (Mixfix o triple2);
+ Scan.optional nat 1000) >> (Mixfix o triple2);
val infx = $$$ "infix" |-- !!! (string -- nat >> Infix);
val infxl = $$$ "infixl" |-- !!! (string -- nat >> Infixl);
--- a/src/Pure/Syntax/mixfix.ML Fri Apr 08 21:03:20 2011 +0200
+++ b/src/Pure/Syntax/mixfix.ML Fri Apr 08 21:11:29 2011 +0200
@@ -97,7 +97,7 @@
fun mfix_of (_, _, NoSyn) = NONE
| mfix_of (t, ty, Mixfix (sy, ps, p)) = SOME (Syntax_Ext.Mfix (sy, ty, t, ps, p))
- | mfix_of (t, ty, Delimfix sy) = SOME (Syntax_Ext.Mfix (sy, ty, t, [], Syntax_Ext.max_pri))
+ | mfix_of (t, ty, Delimfix sy) = SOME (Syntax_Ext.Mfix (sy, ty, t, [], 1000))
| mfix_of (t, ty, Infix (sy, p)) = SOME (mk_infix sy ty t (p + 1) (p + 1) p)
| mfix_of (t, ty, Infixl (sy, p)) = SOME (mk_infix sy ty t p (p + 1) p)
| mfix_of (t, ty, Infixr (sy, p)) = SOME (mk_infix sy ty t (p + 1) p p)
@@ -122,7 +122,7 @@
fun syn_ext_consts is_logtype const_decls =
let
fun mk_infix sy ty c p1 p2 p3 =
- [Syntax_Ext.Mfix ("op " ^ sy, ty, c, [], Syntax_Ext.max_pri),
+ [Syntax_Ext.Mfix ("op " ^ sy, ty, c, [], 1000),
Syntax_Ext.Mfix ("(_ " ^ sy ^ "/ _)", ty, c, [p1, p2], p3)];
fun binder_typ _ (Type ("fun", [Type ("fun", [_, ty2]), ty3])) =
@@ -131,7 +131,7 @@
fun mfix_of (_, _, NoSyn) = []
| mfix_of (c, ty, Mixfix (sy, ps, p)) = [Syntax_Ext.Mfix (sy, ty, c, ps, p)]
- | mfix_of (c, ty, Delimfix sy) = [Syntax_Ext.Mfix (sy, ty, c, [], Syntax_Ext.max_pri)]
+ | mfix_of (c, ty, Delimfix sy) = [Syntax_Ext.Mfix (sy, ty, c, [], 1000)]
| mfix_of (c, ty, Infix (sy, p)) = mk_infix sy ty c (p + 1) (p + 1) p
| mfix_of (c, ty, Infixl (sy, p)) = mk_infix sy ty c p (p + 1) p
| mfix_of (c, ty, Infixr (sy, p)) = mk_infix sy ty c (p + 1) p p
--- a/src/Pure/Syntax/printer.ML Fri Apr 08 21:03:20 2011 +0200
+++ b/src/Pure/Syntax/printer.ML Fri Apr 08 21:11:29 2011 +0200
@@ -98,7 +98,7 @@
let
fun arg (s, p) =
(if s = "type" then TypArg else Arg)
- (if Lexicon.is_terminal s then Syntax_Ext.max_pri else p);
+ (if Lexicon.is_terminal s then 1000 else p);
fun xsyms_to_syms (Syntax_Ext.Delim s :: xsyms) =
apfst (cons (String s)) (xsyms_to_syms xsyms)
@@ -210,10 +210,8 @@
val T = if i < 0 then Pretty.fbrk else Pretty.brk i;
in (T :: Ts, args') end
- and parT m (pr, args, p, p': int) =
- #1 (synT m
- (if p > p' orelse
- (show_brackets andalso p' <> Syntax_Ext.max_pri andalso not (is_chain pr))
+ and parT m (pr, args, p, p': int) = #1 (synT m
+ (if p > p' orelse (show_brackets andalso p' <> 1000 andalso not (is_chain pr))
then [Block (1, Space "(" :: pr @ [Space ")"])]
else pr, args))
--- a/src/Pure/Syntax/syntax.ML Fri Apr 08 21:03:20 2011 +0200
+++ b/src/Pure/Syntax/syntax.ML Fri Apr 08 21:11:29 2011 +0200
@@ -7,7 +7,6 @@
signature SYNTAX =
sig
- val max_pri: int
val const: string -> term
val free: string -> term
val var: indexname -> term
@@ -144,8 +143,6 @@
structure Syntax: SYNTAX =
struct
-val max_pri = Syntax_Ext.max_pri;
-
val const = Lexicon.const;
val free = Lexicon.free;
val var = Lexicon.var;
--- a/src/Pure/Syntax/syntax_ext.ML Fri Apr 08 21:03:20 2011 +0200
+++ b/src/Pure/Syntax/syntax_ext.ML Fri Apr 08 21:11:29 2011 +0200
@@ -7,7 +7,6 @@
signature SYNTAX_EXT =
sig
val dddot_indexname: indexname
- val max_pri: int
datatype mfix = Mfix of string * typ * string * int list * int
val err_in_mfix: string -> mfix -> 'a
val typ_to_nonterm: typ -> string
@@ -107,7 +106,6 @@
datatype xprod = XProd of string * xsymb list * string * int;
-val max_pri = 1000; (*maximum legal priority*)
val chain_pri = ~1; (*dummy for chain productions*)
fun delims_of xprods =
@@ -195,7 +193,7 @@
fun mfix_to_xprod is_logtype (mfix as Mfix (sy, typ, const, pris, pri)) =
let
fun check_pri p =
- if p >= 0 andalso p <= max_pri then ()
+ if p >= 0 andalso p <= 1000 then ()
else err_in_mfix ("Precedence out of range: " ^ string_of_int p) mfix;
fun blocks_ok [] 0 = true
--- a/src/Pure/pure_thy.ML Fri Apr 08 21:03:20 2011 +0200
+++ b/src/Pure/pure_thy.ML Fri Apr 08 21:11:29 2011 +0200
@@ -75,9 +75,9 @@
("", typ "type_name => type", Delimfix "_"),
("_type_name", typ "id => type_name", Delimfix "_"),
("_type_name", typ "longid => type_name", Delimfix "_"),
- ("_ofsort", typ "tid => sort => type", Mixfix ("_::_", [Syntax.max_pri, 0], Syntax.max_pri)),
- ("_ofsort", typ "tvar => sort => type", Mixfix ("_::_", [Syntax.max_pri, 0], Syntax.max_pri)),
- ("_dummy_ofsort", typ "sort => type", Mixfix ("'_()::_", [0], Syntax.max_pri)),
+ ("_ofsort", typ "tid => sort => type", Mixfix ("_::_", [1000, 0], 1000)),
+ ("_ofsort", typ "tvar => sort => type", Mixfix ("_::_", [1000, 0], 1000)),
+ ("_dummy_ofsort", typ "sort => type", Mixfix ("'_()::_", [0], 1000)),
("", typ "class_name => sort", Delimfix "_"),
("_class_name", typ "id => class_name", Delimfix "_"),
("_class_name", typ "longid => class_name", Delimfix "_"),
@@ -85,7 +85,7 @@
("_sort", typ "classes => sort", Delimfix "{_}"),
("", typ "class_name => classes", Delimfix "_"),
("_classes", typ "class_name => classes => classes", Delimfix "_,_"),
- ("_tapp", typ "type => type_name => type", Mixfix ("_ _", [Syntax.max_pri, 0], Syntax.max_pri)),
+ ("_tapp", typ "type => type_name => type", Mixfix ("_ _", [1000, 0], 1000)),
("_tappl", typ "type => types => type_name => type", Delimfix "((1'(_,/ _')) _)"),
("", typ "type => types", Delimfix "_"),
("_types", typ "type => types => types", Delimfix "_,/ _"),