--- a/src/Pure/Syntax/mixfix.ML Wed Jan 04 00:52:47 2006 +0100
+++ b/src/Pure/Syntax/mixfix.ML Wed Jan 04 00:52:48 2006 +0100
@@ -14,9 +14,9 @@
InfixName of string * int |
InfixlName of string * int |
InfixrName of string * int |
- Infix of int |
- Infixl of int |
- Infixr of int |
+ Infix of int | (*obsolete*)
+ Infixl of int | (*obsolete*)
+ Infixr of int | (*obsolete*)
Binder of string * int * int
end;
@@ -29,6 +29,7 @@
val type_name: string -> mixfix -> string
val const_name: string -> mixfix -> string
val fix_mixfix: string -> mixfix -> mixfix
+ val unlocalize_mixfix: mixfix -> mixfix
val mixfix_args: mixfix -> int
val pure_nonterms: string list
val pure_syntax: (string * string * mixfix) list
@@ -58,9 +59,9 @@
InfixName of string * int |
InfixlName of string * int |
InfixrName of string * int |
- Infix of int |
- Infixl of int |
- Infixr of int |
+ Infix of int | (*obsolete*)
+ Infixl of int | (*obsolete*)
+ Infixr of int | (*obsolete*)
Binder of string * int * int;
val literal = Delimfix o SynExt.escape_mfix;
@@ -120,6 +121,17 @@
| fix_mixfix c (Infixr p) = (deprecated (strip_esc c); InfixrName (c, p))
| fix_mixfix _ mx = mx;
+fun map_mixfix _ NoSyn = NoSyn
+ | map_mixfix f (Mixfix (sy, ps, p)) = Mixfix (f sy, ps, p)
+ | map_mixfix f (Delimfix sy) = Delimfix (f sy)
+ | map_mixfix f (InfixName (sy, p)) = InfixName (f sy, p)
+ | map_mixfix f (InfixlName (sy, p)) = InfixlName (f sy, p)
+ | map_mixfix f (InfixrName (sy, p)) = InfixrName (f sy, p)
+ | map_mixfix f (Binder (sy, p, q)) = Binder (f sy, p, q)
+ | map_mixfix _ _ = raise Fail ("map_mixfix: illegal occurrence of unnamed infix");
+
+val unlocalize_mixfix = map_mixfix SynExt.unlocalize_mfix;
+
fun mixfix_args NoSyn = 0
| mixfix_args (Mixfix (sy, _, _)) = SynExt.mfix_args sy
| mixfix_args (Delimfix sy) = SynExt.mfix_args sy