discontinued Syntax.max_pri, which is not really a symbolic parameter;
authorwenzelm
Fri Apr 08 21:11:29 2011 +0200 (2011-04-08)
changeset 42297140f283266b7
parent 42296 dcc08f2a8671
child 42298 d622145603ee
discontinued Syntax.max_pri, which is not really a symbolic parameter;
src/HOL/Library/OptionalSugar.thy
src/HOL/Tools/Datatype/datatype_data.ML
src/Pure/Isar/parse.ML
src/Pure/Syntax/mixfix.ML
src/Pure/Syntax/printer.ML
src/Pure/Syntax/syntax.ML
src/Pure/Syntax/syntax_ext.ML
src/Pure/pure_thy.ML
     1.1 --- a/src/HOL/Library/OptionalSugar.thy	Fri Apr 08 21:03:20 2011 +0200
     1.2 +++ b/src/HOL/Library/OptionalSugar.thy	Fri Apr 08 21:11:29 2011 +0200
     1.3 @@ -68,10 +68,10 @@
     1.4    val classesT = Type ("classes", []); (*FIXME*)
     1.5  in
     1.6    Sign.add_modesyntax_i (Symbol.xsymbolsN, false) [
     1.7 -    ("_topsort", sortT, Mixfix ("\<top>", [], Syntax.max_pri)),
     1.8 -    ("_sort", classesT --> sortT, Mixfix ("'(_')", [], Syntax.max_pri)),
     1.9 -    ("_classes", Lexicon.idT --> classesT --> classesT, Mixfix ("_ \<inter> _", [], Syntax.max_pri)),
    1.10 -    ("_classes", Lexicon.longidT --> classesT --> classesT, Mixfix ("_ \<inter> _", [], Syntax.max_pri))
    1.11 +    ("_topsort", sortT, Mixfix ("\<top>", [], 1000)),
    1.12 +    ("_sort", classesT --> sortT, Mixfix ("'(_')", [], 1000)),
    1.13 +    ("_classes", Lexicon.idT --> classesT --> classesT, Mixfix ("_ \<inter> _", [], 1000)),
    1.14 +    ("_classes", Lexicon.longidT --> classesT --> classesT, Mixfix ("_ \<inter> _", [], 1000))
    1.15    ]
    1.16  end
    1.17  *}
     2.1 --- a/src/HOL/Tools/Datatype/datatype_data.ML	Fri Apr 08 21:03:20 2011 +0200
     2.2 +++ b/src/HOL/Tools/Datatype/datatype_data.ML	Fri Apr 08 21:11:29 2011 +0200
     2.3 @@ -243,8 +243,7 @@
     2.4        val thy = ProofContext.theory_of ctxt;
     2.5        val (vs, cos) = the_spec thy dtco;
     2.6        val ty = Type (dtco, map TFree vs);
     2.7 -      val pretty_typ_bracket =
     2.8 -        Syntax.pretty_typ (Config.put pretty_priority (Syntax.max_pri + 1) ctxt);
     2.9 +      val pretty_typ_bracket = Syntax.pretty_typ (Config.put pretty_priority 1001 ctxt);
    2.10        fun pretty_constr (co, tys) =
    2.11          Pretty.block (Pretty.breaks
    2.12            (Syntax.pretty_term ctxt (Const (co, tys ---> ty)) ::
     3.1 --- a/src/Pure/Isar/parse.ML	Fri Apr 08 21:03:20 2011 +0200
     3.2 +++ b/src/Pure/Isar/parse.ML	Fri Apr 08 21:11:29 2011 +0200
     3.3 @@ -272,7 +272,7 @@
     3.4  
     3.5  val mfix = string --
     3.6    !!! (Scan.optional ($$$ "[" |-- !!! (list nat --| $$$ "]")) [] --
     3.7 -    Scan.optional nat Syntax.max_pri) >> (Mixfix o triple2);
     3.8 +    Scan.optional nat 1000) >> (Mixfix o triple2);
     3.9  
    3.10  val infx = $$$ "infix" |-- !!! (string -- nat >> Infix);
    3.11  val infxl = $$$ "infixl" |-- !!! (string -- nat >> Infixl);
     4.1 --- a/src/Pure/Syntax/mixfix.ML	Fri Apr 08 21:03:20 2011 +0200
     4.2 +++ b/src/Pure/Syntax/mixfix.ML	Fri Apr 08 21:11:29 2011 +0200
     4.3 @@ -97,7 +97,7 @@
     4.4  
     4.5      fun mfix_of (_, _, NoSyn) = NONE
     4.6        | mfix_of (t, ty, Mixfix (sy, ps, p)) = SOME (Syntax_Ext.Mfix (sy, ty, t, ps, p))
     4.7 -      | mfix_of (t, ty, Delimfix sy) = SOME (Syntax_Ext.Mfix (sy, ty, t, [], Syntax_Ext.max_pri))
     4.8 +      | mfix_of (t, ty, Delimfix sy) = SOME (Syntax_Ext.Mfix (sy, ty, t, [], 1000))
     4.9        | mfix_of (t, ty, Infix (sy, p)) = SOME (mk_infix sy ty t (p + 1) (p + 1) p)
    4.10        | mfix_of (t, ty, Infixl (sy, p)) = SOME (mk_infix sy ty t p (p + 1) p)
    4.11        | mfix_of (t, ty, Infixr (sy, p)) = SOME (mk_infix sy ty t (p + 1) p p)
    4.12 @@ -122,7 +122,7 @@
    4.13  fun syn_ext_consts is_logtype const_decls =
    4.14    let
    4.15      fun mk_infix sy ty c p1 p2 p3 =
    4.16 -      [Syntax_Ext.Mfix ("op " ^ sy, ty, c, [], Syntax_Ext.max_pri),
    4.17 +      [Syntax_Ext.Mfix ("op " ^ sy, ty, c, [], 1000),
    4.18         Syntax_Ext.Mfix ("(_ " ^ sy ^ "/ _)", ty, c, [p1, p2], p3)];
    4.19  
    4.20      fun binder_typ _ (Type ("fun", [Type ("fun", [_, ty2]), ty3])) =
    4.21 @@ -131,7 +131,7 @@
    4.22  
    4.23      fun mfix_of (_, _, NoSyn) = []
    4.24        | mfix_of (c, ty, Mixfix (sy, ps, p)) = [Syntax_Ext.Mfix (sy, ty, c, ps, p)]
    4.25 -      | mfix_of (c, ty, Delimfix sy) = [Syntax_Ext.Mfix (sy, ty, c, [], Syntax_Ext.max_pri)]
    4.26 +      | mfix_of (c, ty, Delimfix sy) = [Syntax_Ext.Mfix (sy, ty, c, [], 1000)]
    4.27        | mfix_of (c, ty, Infix (sy, p)) = mk_infix sy ty c (p + 1) (p + 1) p
    4.28        | mfix_of (c, ty, Infixl (sy, p)) = mk_infix sy ty c p (p + 1) p
    4.29        | mfix_of (c, ty, Infixr (sy, p)) = mk_infix sy ty c (p + 1) p p
     5.1 --- a/src/Pure/Syntax/printer.ML	Fri Apr 08 21:03:20 2011 +0200
     5.2 +++ b/src/Pure/Syntax/printer.ML	Fri Apr 08 21:11:29 2011 +0200
     5.3 @@ -98,7 +98,7 @@
     5.4        let
     5.5          fun arg (s, p) =
     5.6            (if s = "type" then TypArg else Arg)
     5.7 -          (if Lexicon.is_terminal s then Syntax_Ext.max_pri else p);
     5.8 +          (if Lexicon.is_terminal s then 1000 else p);
     5.9  
    5.10          fun xsyms_to_syms (Syntax_Ext.Delim s :: xsyms) =
    5.11                apfst (cons (String s)) (xsyms_to_syms xsyms)
    5.12 @@ -210,10 +210,8 @@
    5.13              val T = if i < 0 then Pretty.fbrk else Pretty.brk i;
    5.14            in (T :: Ts, args') end
    5.15  
    5.16 -    and parT m (pr, args, p, p': int) =
    5.17 -      #1 (synT m
    5.18 -          (if p > p' orelse
    5.19 -            (show_brackets andalso p' <> Syntax_Ext.max_pri andalso not (is_chain pr))
    5.20 +    and parT m (pr, args, p, p': int) = #1 (synT m
    5.21 +          (if p > p' orelse (show_brackets andalso p' <> 1000 andalso not (is_chain pr))
    5.22             then [Block (1, Space "(" :: pr @ [Space ")"])]
    5.23             else pr, args))
    5.24  
     6.1 --- a/src/Pure/Syntax/syntax.ML	Fri Apr 08 21:03:20 2011 +0200
     6.2 +++ b/src/Pure/Syntax/syntax.ML	Fri Apr 08 21:11:29 2011 +0200
     6.3 @@ -7,7 +7,6 @@
     6.4  
     6.5  signature SYNTAX =
     6.6  sig
     6.7 -  val max_pri: int
     6.8    val const: string -> term
     6.9    val free: string -> term
    6.10    val var: indexname -> term
    6.11 @@ -144,8 +143,6 @@
    6.12  structure Syntax: SYNTAX =
    6.13  struct
    6.14  
    6.15 -val max_pri = Syntax_Ext.max_pri;
    6.16 -
    6.17  val const = Lexicon.const;
    6.18  val free = Lexicon.free;
    6.19  val var = Lexicon.var;
     7.1 --- a/src/Pure/Syntax/syntax_ext.ML	Fri Apr 08 21:03:20 2011 +0200
     7.2 +++ b/src/Pure/Syntax/syntax_ext.ML	Fri Apr 08 21:11:29 2011 +0200
     7.3 @@ -7,7 +7,6 @@
     7.4  signature SYNTAX_EXT =
     7.5  sig
     7.6    val dddot_indexname: indexname
     7.7 -  val max_pri: int
     7.8    datatype mfix = Mfix of string * typ * string * int list * int
     7.9    val err_in_mfix: string -> mfix -> 'a
    7.10    val typ_to_nonterm: typ -> string
    7.11 @@ -107,7 +106,6 @@
    7.12  
    7.13  datatype xprod = XProd of string * xsymb list * string * int;
    7.14  
    7.15 -val max_pri = 1000;   (*maximum legal priority*)
    7.16  val chain_pri = ~1;   (*dummy for chain productions*)
    7.17  
    7.18  fun delims_of xprods =
    7.19 @@ -195,7 +193,7 @@
    7.20  fun mfix_to_xprod is_logtype (mfix as Mfix (sy, typ, const, pris, pri)) =
    7.21    let
    7.22      fun check_pri p =
    7.23 -      if p >= 0 andalso p <= max_pri then ()
    7.24 +      if p >= 0 andalso p <= 1000 then ()
    7.25        else err_in_mfix ("Precedence out of range: " ^ string_of_int p) mfix;
    7.26  
    7.27      fun blocks_ok [] 0 = true
     8.1 --- a/src/Pure/pure_thy.ML	Fri Apr 08 21:03:20 2011 +0200
     8.2 +++ b/src/Pure/pure_thy.ML	Fri Apr 08 21:11:29 2011 +0200
     8.3 @@ -75,9 +75,9 @@
     8.4      ("",            typ "type_name => type",           Delimfix "_"),
     8.5      ("_type_name",  typ "id => type_name",             Delimfix "_"),
     8.6      ("_type_name",  typ "longid => type_name",         Delimfix "_"),
     8.7 -    ("_ofsort",     typ "tid => sort => type",         Mixfix ("_::_", [Syntax.max_pri, 0], Syntax.max_pri)),
     8.8 -    ("_ofsort",     typ "tvar => sort => type",        Mixfix ("_::_", [Syntax.max_pri, 0], Syntax.max_pri)),
     8.9 -    ("_dummy_ofsort", typ "sort => type",              Mixfix ("'_()::_", [0], Syntax.max_pri)),
    8.10 +    ("_ofsort",     typ "tid => sort => type",         Mixfix ("_::_", [1000, 0], 1000)),
    8.11 +    ("_ofsort",     typ "tvar => sort => type",        Mixfix ("_::_", [1000, 0], 1000)),
    8.12 +    ("_dummy_ofsort", typ "sort => type",              Mixfix ("'_()::_", [0], 1000)),
    8.13      ("",            typ "class_name => sort",          Delimfix "_"),
    8.14      ("_class_name", typ "id => class_name",            Delimfix "_"),
    8.15      ("_class_name", typ "longid => class_name",        Delimfix "_"),
    8.16 @@ -85,7 +85,7 @@
    8.17      ("_sort",       typ "classes => sort",             Delimfix "{_}"),
    8.18      ("",            typ "class_name => classes",       Delimfix "_"),
    8.19      ("_classes",    typ "class_name => classes => classes", Delimfix "_,_"),
    8.20 -    ("_tapp",       typ "type => type_name => type",   Mixfix ("_ _", [Syntax.max_pri, 0], Syntax.max_pri)),
    8.21 +    ("_tapp",       typ "type => type_name => type",   Mixfix ("_ _", [1000, 0], 1000)),
    8.22      ("_tappl",      typ "type => types => type_name => type", Delimfix "((1'(_,/ _')) _)"),
    8.23      ("",            typ "type => types",               Delimfix "_"),
    8.24      ("_types",      typ "type => types => types",      Delimfix "_,/ _"),