removed fix_mixfix;
authorwenzelm
Sat Apr 08 22:51:31 2006 +0200 (2006-04-08)
changeset 19373f2446ce04590
parent 19372 3ff5f1777743
child 19374 ae4a225e0c1f
removed fix_mixfix;
added const_mixfix, mixfix_const;
src/Pure/Syntax/mixfix.ML
     1.1 --- a/src/Pure/Syntax/mixfix.ML	Sat Apr 08 22:51:30 2006 +0200
     1.2 +++ b/src/Pure/Syntax/mixfix.ML	Sat Apr 08 22:51:31 2006 +0200
     1.3 @@ -29,7 +29,8 @@
     1.4    val pretty_mixfix: mixfix -> Pretty.T
     1.5    val type_name: string -> mixfix -> string
     1.6    val const_name: string -> mixfix -> string
     1.7 -  val fix_mixfix: string -> mixfix -> mixfix
     1.8 +  val const_mixfix: string -> mixfix -> string * mixfix
     1.9 +  val mixfix_const: string -> mixfix -> string * bool
    1.10    val unlocalize_mixfix: mixfix -> mixfix
    1.11    val mixfix_args: mixfix -> int
    1.12    val mixfix_content: mixfix -> string list list
    1.13 @@ -122,11 +123,16 @@
    1.14    | const_name c (Infixr _) = "op " ^ deprecated (strip_esc c)
    1.15    | const_name c _ = c;
    1.16  
    1.17 -fun fix_mixfix c (Infix p) = (deprecated (strip_esc c); InfixName (c, p))
    1.18 -  | fix_mixfix c (Infixl p) = (deprecated (strip_esc c); InfixlName (c, p))
    1.19 -  | fix_mixfix c (Infixr p) = (deprecated (strip_esc c); InfixrName (c, p))
    1.20 +fun fix_mixfix c (Infix p) = InfixName (c, p)
    1.21 +  | fix_mixfix c (Infixl p) = InfixlName (c, p)
    1.22 +  | fix_mixfix c (Infixr p) = InfixrName (c, p)
    1.23    | fix_mixfix _ mx = mx;
    1.24  
    1.25 +fun const_mixfix c mx = (const_name c mx, fix_mixfix c mx);
    1.26 +
    1.27 +fun mixfix_const c NoSyn = (c, true)
    1.28 +  | mixfix_const c _ = (Lexicon.constN ^ c, false);
    1.29 +
    1.30  fun map_mixfix _ NoSyn = NoSyn
    1.31    | map_mixfix f (Mixfix (sy, ps, p)) = Mixfix (f sy, ps, p)
    1.32    | map_mixfix f (Delimfix sy) = Delimfix (f sy)