# HG changeset patch # User wenzelm # Date 1302289889 -7200 # Node ID 140f283266b774cac15504ef8718b4caf4f77bc4 # Parent dcc08f2a86711877206c33c924193ede8d62b6af discontinued Syntax.max_pri, which is not really a symbolic parameter; diff -r dcc08f2a8671 -r 140f283266b7 src/HOL/Library/OptionalSugar.thy --- 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 ("\", [], Syntax.max_pri)), - ("_sort", classesT --> sortT, Mixfix ("'(_')", [], Syntax.max_pri)), - ("_classes", Lexicon.idT --> classesT --> classesT, Mixfix ("_ \ _", [], Syntax.max_pri)), - ("_classes", Lexicon.longidT --> classesT --> classesT, Mixfix ("_ \ _", [], Syntax.max_pri)) + ("_topsort", sortT, Mixfix ("\", [], 1000)), + ("_sort", classesT --> sortT, Mixfix ("'(_')", [], 1000)), + ("_classes", Lexicon.idT --> classesT --> classesT, Mixfix ("_ \ _", [], 1000)), + ("_classes", Lexicon.longidT --> classesT --> classesT, Mixfix ("_ \ _", [], 1000)) ] end *} diff -r dcc08f2a8671 -r 140f283266b7 src/HOL/Tools/Datatype/datatype_data.ML --- 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)) :: diff -r dcc08f2a8671 -r 140f283266b7 src/Pure/Isar/parse.ML --- 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); diff -r dcc08f2a8671 -r 140f283266b7 src/Pure/Syntax/mixfix.ML --- 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 diff -r dcc08f2a8671 -r 140f283266b7 src/Pure/Syntax/printer.ML --- 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)) diff -r dcc08f2a8671 -r 140f283266b7 src/Pure/Syntax/syntax.ML --- 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; diff -r dcc08f2a8671 -r 140f283266b7 src/Pure/Syntax/syntax_ext.ML --- 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 diff -r dcc08f2a8671 -r 140f283266b7 src/Pure/pure_thy.ML --- 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 "_,/ _"),