added string_of_mixfix;
authorwenzelm
Wed Oct 24 17:31:58 2001 +0200 (2001-10-24)
changeset 119206833cadb4062
parent 11919 68b2578d4592
child 11921 2a0e9622dc51
added string_of_mixfix;
src/Pure/Syntax/mixfix.ML
     1.1 --- a/src/Pure/Syntax/mixfix.ML	Wed Oct 24 17:31:20 2001 +0200
     1.2 +++ b/src/Pure/Syntax/mixfix.ML	Wed Oct 24 17:31:58 2001 +0200
     1.3 @@ -24,6 +24,7 @@
     1.4  sig
     1.5    include MIXFIX0
     1.6    val no_syn: 'a * 'b -> 'a * 'b * mixfix
     1.7 +  val string_of_mixfix: mixfix -> string
     1.8    val type_name: string -> mixfix -> string
     1.9    val const_name: string -> mixfix -> string
    1.10    val fix_mixfix: string -> mixfix -> mixfix
    1.11 @@ -67,6 +68,24 @@
    1.12  fun no_syn (x, y) = (x, y, NoSyn);
    1.13  
    1.14  
    1.15 +(* string_of_mixfix *)
    1.16 +
    1.17 +val parens = enclose "(" ")";
    1.18 +val brackets = enclose "[" "]";
    1.19 +val spaces = space_implode " ";
    1.20 +
    1.21 +fun string_of_mixfix NoSyn = ""
    1.22 +  | string_of_mixfix (Mixfix (sy, ps, p)) =
    1.23 +      parens (spaces [quote sy, brackets (commas (map string_of_int ps)), string_of_int p])
    1.24 +  | string_of_mixfix (Delimfix sy) = parens (quote sy)
    1.25 +  | string_of_mixfix (InfixName (sy, p)) = parens (spaces ["infix", quote sy, string_of_int p])
    1.26 +  | string_of_mixfix (InfixlName (sy, p)) = parens (spaces ["infixl", quote sy, string_of_int p])
    1.27 +  | string_of_mixfix (InfixrName (sy, p)) = parens (spaces ["infixl", quote sy, string_of_int p])
    1.28 +  | string_of_mixfix (Infix p) = parens (spaces ["infix", string_of_int p])
    1.29 +  | string_of_mixfix (Infixl p) = parens (spaces ["infixl", string_of_int p])
    1.30 +  | string_of_mixfix (Infixr p) = parens (spaces ["infixr", string_of_int p]);
    1.31 +
    1.32 +
    1.33  (* type / const names *)
    1.34  
    1.35  fun strip ("'" :: c :: cs) = c :: strip cs