# HG changeset patch
# User wenzelm
# Date 1003937518 -7200
# Node ID 6833cadb4062e0b6c7cbaa071f4b8fac38cf8c40
# Parent  68b2578d4592eefc2b91469a44846fd9402cd6fb
added string_of_mixfix;

diff -r 68b2578d4592 -r 6833cadb4062 src/Pure/Syntax/mixfix.ML
--- a/src/Pure/Syntax/mixfix.ML	Wed Oct 24 17:31:20 2001 +0200
+++ b/src/Pure/Syntax/mixfix.ML	Wed Oct 24 17:31:58 2001 +0200
@@ -24,6 +24,7 @@
 sig
   include MIXFIX0
   val no_syn: 'a * 'b -> 'a * 'b * mixfix
+  val string_of_mixfix: mixfix -> string
   val type_name: string -> mixfix -> string
   val const_name: string -> mixfix -> string
   val fix_mixfix: string -> mixfix -> mixfix
@@ -67,6 +68,24 @@
 fun no_syn (x, y) = (x, y, NoSyn);
 
 
+(* string_of_mixfix *)
+
+val parens = enclose "(" ")";
+val brackets = enclose "[" "]";
+val spaces = space_implode " ";
+
+fun string_of_mixfix NoSyn = ""
+  | string_of_mixfix (Mixfix (sy, ps, p)) =
+      parens (spaces [quote sy, brackets (commas (map string_of_int ps)), string_of_int p])
+  | string_of_mixfix (Delimfix sy) = parens (quote sy)
+  | string_of_mixfix (InfixName (sy, p)) = parens (spaces ["infix", quote sy, string_of_int p])
+  | string_of_mixfix (InfixlName (sy, p)) = parens (spaces ["infixl", quote sy, string_of_int p])
+  | string_of_mixfix (InfixrName (sy, p)) = parens (spaces ["infixl", quote sy, string_of_int p])
+  | string_of_mixfix (Infix p) = parens (spaces ["infix", string_of_int p])
+  | string_of_mixfix (Infixl p) = parens (spaces ["infixl", string_of_int p])
+  | string_of_mixfix (Infixr p) = parens (spaces ["infixr", string_of_int p]);
+
+
 (* type / const names *)
 
 fun strip ("'" :: c :: cs) = c :: strip cs