added unlocalize_mixfix;
authorwenzelm
Wed Jan 04 00:52:48 2006 +0100 (2006-01-04)
changeset 18565818a24371de9
parent 18564 2b8ac8bc9719
child 18566 20dd2f7dca4b
added unlocalize_mixfix;
src/Pure/Syntax/mixfix.ML
     1.1 --- a/src/Pure/Syntax/mixfix.ML	Wed Jan 04 00:52:47 2006 +0100
     1.2 +++ b/src/Pure/Syntax/mixfix.ML	Wed Jan 04 00:52:48 2006 +0100
     1.3 @@ -14,9 +14,9 @@
     1.4      InfixName of string * int |
     1.5      InfixlName of string * int |
     1.6      InfixrName of string * int |
     1.7 -    Infix of int |
     1.8 -    Infixl of int |
     1.9 -    Infixr of int |
    1.10 +    Infix of int |    (*obsolete*)
    1.11 +    Infixl of int |   (*obsolete*)
    1.12 +    Infixr of int |   (*obsolete*)
    1.13      Binder of string * int * int
    1.14  end;
    1.15  
    1.16 @@ -29,6 +29,7 @@
    1.17    val type_name: string -> mixfix -> string
    1.18    val const_name: string -> mixfix -> string
    1.19    val fix_mixfix: string -> mixfix -> mixfix
    1.20 +  val unlocalize_mixfix: mixfix -> mixfix
    1.21    val mixfix_args: mixfix -> int
    1.22    val pure_nonterms: string list
    1.23    val pure_syntax: (string * string * mixfix) list
    1.24 @@ -58,9 +59,9 @@
    1.25    InfixName of string * int |
    1.26    InfixlName of string * int |
    1.27    InfixrName of string * int |
    1.28 -  Infix of int |
    1.29 -  Infixl of int |
    1.30 -  Infixr of int |
    1.31 +  Infix of int |      (*obsolete*)
    1.32 +  Infixl of int |     (*obsolete*)
    1.33 +  Infixr of int |     (*obsolete*)
    1.34    Binder of string * int * int;
    1.35  
    1.36  val literal = Delimfix o SynExt.escape_mfix;
    1.37 @@ -120,6 +121,17 @@
    1.38    | fix_mixfix c (Infixr p) = (deprecated (strip_esc c); InfixrName (c, p))
    1.39    | fix_mixfix _ mx = mx;
    1.40  
    1.41 +fun map_mixfix _ NoSyn = NoSyn
    1.42 +  | map_mixfix f (Mixfix (sy, ps, p)) = Mixfix (f sy, ps, p)
    1.43 +  | map_mixfix f (Delimfix sy) = Delimfix (f sy)
    1.44 +  | map_mixfix f (InfixName (sy, p)) = InfixName (f sy, p)
    1.45 +  | map_mixfix f (InfixlName (sy, p)) = InfixlName (f sy, p)
    1.46 +  | map_mixfix f (InfixrName (sy, p)) = InfixrName (f sy, p)
    1.47 +  | map_mixfix f (Binder (sy, p, q)) = Binder (f sy, p, q)
    1.48 +  | map_mixfix _ _ = raise Fail ("map_mixfix: illegal occurrence of unnamed infix");
    1.49 +
    1.50 +val unlocalize_mixfix = map_mixfix SynExt.unlocalize_mfix;
    1.51 +
    1.52  fun mixfix_args NoSyn = 0
    1.53    | mixfix_args (Mixfix (sy, _, _)) = SynExt.mfix_args sy
    1.54    | mixfix_args (Delimfix sy) = SynExt.mfix_args sy