# HG changeset patch
# User wenzelm
# Date 1142370402 -3600
# Node ID 967e6c2578f2b9d8cff03fb17b7d495d203db44e
# Parent  d928b5468c430e509b0e0b32303c58be87da0a34
turned string_of_mixfix into pretty_mixfix;

diff -r d928b5468c43 -r 967e6c2578f2 src/Pure/Syntax/mixfix.ML
--- a/src/Pure/Syntax/mixfix.ML	Tue Mar 14 22:06:40 2006 +0100
+++ b/src/Pure/Syntax/mixfix.ML	Tue Mar 14 22:06:42 2006 +0100
@@ -26,7 +26,7 @@
   include MIXFIX0
   val literal: string -> mixfix
   val no_syn: 'a * 'b -> 'a * 'b * mixfix
-  val string_of_mixfix: mixfix -> string
+  val pretty_mixfix: mixfix -> Pretty.T
   val type_name: string -> mixfix -> string
   val const_name: string -> mixfix -> string
   val fix_mixfix: string -> mixfix -> mixfix
@@ -66,25 +66,33 @@
 fun no_syn (x, y) = (x, y, NoSyn);
 
 
-(* string_of_mixfix *)
+(* pretty_mixfix *)
+
+local
 
-val parens = enclose "(" ")";
-val brackets = enclose "[" "]";
-val spaces = space_implode " ";
+val quoted = Pretty.quote o Pretty.str;
+val keyword = Pretty.keyword;
+val parens = Pretty.enclose "(" ")";
+val brackets = Pretty.enclose "[" "]";
+val int = Pretty.str o string_of_int;
+
+in
 
-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])
-  | string_of_mixfix (Binder (sy, p1, p2)) =
-      parens (spaces ["binder", quote sy, brackets (string_of_int p1), string_of_int p2])
-  | string_of_mixfix Structure = "(structure)";
+fun pretty_mixfix NoSyn = Pretty.str ""
+  | pretty_mixfix (Mixfix (s, ps, p)) =
+      parens (Pretty.breaks [quoted s, brackets (Pretty.commas (map int ps)), int p])
+  | pretty_mixfix (Delimfix s) = parens [quoted s]
+  | pretty_mixfix (InfixName (s, p)) = parens (Pretty.breaks [keyword "infix", quoted s, int p])
+  | pretty_mixfix (InfixlName (s, p)) = parens (Pretty.breaks [keyword "infixl", quoted s, int p])
+  | pretty_mixfix (InfixrName (s, p)) = parens (Pretty.breaks [keyword "infixl", quoted s, int p])
+  | pretty_mixfix (Infix p) = parens (Pretty.breaks [keyword "infix", int p])
+  | pretty_mixfix (Infixl p) = parens (Pretty.breaks [keyword "infixl", int p])
+  | pretty_mixfix (Infixr p) = parens (Pretty.breaks [keyword "infixr", int p])
+  | pretty_mixfix (Binder (s, p1, p2)) =
+      parens (Pretty.breaks [keyword "binder", quoted s, brackets [int p1], int p2])
+  | pretty_mixfix Structure = parens [keyword "structure"];
+
+end;
 
 
 (* syntax specifications *)