turned string_of_mixfix into pretty_mixfix;
authorwenzelm
Tue Mar 14 22:06:42 2006 +0100 (2006-03-14)
changeset 19271967e6c2578f2
parent 19270 d928b5468c43
child 19272 5f376320109a
turned string_of_mixfix into pretty_mixfix;
src/Pure/Syntax/mixfix.ML
     1.1 --- a/src/Pure/Syntax/mixfix.ML	Tue Mar 14 22:06:40 2006 +0100
     1.2 +++ b/src/Pure/Syntax/mixfix.ML	Tue Mar 14 22:06:42 2006 +0100
     1.3 @@ -26,7 +26,7 @@
     1.4    include MIXFIX0
     1.5    val literal: string -> mixfix
     1.6    val no_syn: 'a * 'b -> 'a * 'b * mixfix
     1.7 -  val string_of_mixfix: mixfix -> string
     1.8 +  val pretty_mixfix: mixfix -> Pretty.T
     1.9    val type_name: string -> mixfix -> string
    1.10    val const_name: string -> mixfix -> string
    1.11    val fix_mixfix: string -> mixfix -> mixfix
    1.12 @@ -66,25 +66,33 @@
    1.13  fun no_syn (x, y) = (x, y, NoSyn);
    1.14  
    1.15  
    1.16 -(* string_of_mixfix *)
    1.17 +(* pretty_mixfix *)
    1.18 +
    1.19 +local
    1.20  
    1.21 -val parens = enclose "(" ")";
    1.22 -val brackets = enclose "[" "]";
    1.23 -val spaces = space_implode " ";
    1.24 +val quoted = Pretty.quote o Pretty.str;
    1.25 +val keyword = Pretty.keyword;
    1.26 +val parens = Pretty.enclose "(" ")";
    1.27 +val brackets = Pretty.enclose "[" "]";
    1.28 +val int = Pretty.str o string_of_int;
    1.29 +
    1.30 +in
    1.31  
    1.32 -fun string_of_mixfix NoSyn = ""
    1.33 -  | string_of_mixfix (Mixfix (sy, ps, p)) =
    1.34 -      parens (spaces [quote sy, brackets (commas (map string_of_int ps)), string_of_int p])
    1.35 -  | string_of_mixfix (Delimfix sy) = parens (quote sy)
    1.36 -  | string_of_mixfix (InfixName (sy, p)) = parens (spaces ["infix", quote sy, string_of_int p])
    1.37 -  | string_of_mixfix (InfixlName (sy, p)) = parens (spaces ["infixl", quote sy, string_of_int p])
    1.38 -  | string_of_mixfix (InfixrName (sy, p)) = parens (spaces ["infixl", quote sy, string_of_int p])
    1.39 -  | string_of_mixfix (Infix p) = parens (spaces ["infix", string_of_int p])
    1.40 -  | string_of_mixfix (Infixl p) = parens (spaces ["infixl", string_of_int p])
    1.41 -  | string_of_mixfix (Infixr p) = parens (spaces ["infixr", string_of_int p])
    1.42 -  | string_of_mixfix (Binder (sy, p1, p2)) =
    1.43 -      parens (spaces ["binder", quote sy, brackets (string_of_int p1), string_of_int p2])
    1.44 -  | string_of_mixfix Structure = "(structure)";
    1.45 +fun pretty_mixfix NoSyn = Pretty.str ""
    1.46 +  | pretty_mixfix (Mixfix (s, ps, p)) =
    1.47 +      parens (Pretty.breaks [quoted s, brackets (Pretty.commas (map int ps)), int p])
    1.48 +  | pretty_mixfix (Delimfix s) = parens [quoted s]
    1.49 +  | pretty_mixfix (InfixName (s, p)) = parens (Pretty.breaks [keyword "infix", quoted s, int p])
    1.50 +  | pretty_mixfix (InfixlName (s, p)) = parens (Pretty.breaks [keyword "infixl", quoted s, int p])
    1.51 +  | pretty_mixfix (InfixrName (s, p)) = parens (Pretty.breaks [keyword "infixl", quoted s, int p])
    1.52 +  | pretty_mixfix (Infix p) = parens (Pretty.breaks [keyword "infix", int p])
    1.53 +  | pretty_mixfix (Infixl p) = parens (Pretty.breaks [keyword "infixl", int p])
    1.54 +  | pretty_mixfix (Infixr p) = parens (Pretty.breaks [keyword "infixr", int p])
    1.55 +  | pretty_mixfix (Binder (s, p1, p2)) =
    1.56 +      parens (Pretty.breaks [keyword "binder", quoted s, brackets [int p1], int p2])
    1.57 +  | pretty_mixfix Structure = parens [keyword "structure"];
    1.58 +
    1.59 +end;
    1.60  
    1.61  
    1.62  (* syntax specifications *)