equal
deleted
inserted
replaced
125 (*strings*) |
125 (*strings*) |
126 val nth_elem_string: int * string -> string |
126 val nth_elem_string: int * string -> string |
127 val foldl_string: ('a * string -> 'a) -> 'a * string -> 'a |
127 val foldl_string: ('a * string -> 'a) -> 'a * string -> 'a |
128 val exists_string: (string -> bool) -> string -> bool |
128 val exists_string: (string -> bool) -> string -> bool |
129 val enclose: string -> string -> string -> string |
129 val enclose: string -> string -> string -> string |
|
130 val unenclose: string -> string |
130 val quote: string -> string |
131 val quote: string -> string |
131 val space_implode: string -> string list -> string |
132 val space_implode: string -> string list -> string |
132 val commas: string list -> string |
133 val commas: string list -> string |
133 val commas_quote: string list -> string |
134 val commas_quote: string list -> string |
134 val cat_lines: string list -> string |
135 val cat_lines: string list -> string |
671 |
672 |
672 fun exists_string pred str = foldl_string (fn (b, s) => b orelse pred s) (false, str); |
673 fun exists_string pred str = foldl_string (fn (b, s) => b orelse pred s) (false, str); |
673 |
674 |
674 (*enclose in brackets*) |
675 (*enclose in brackets*) |
675 fun enclose lpar rpar str = lpar ^ str ^ rpar; |
676 fun enclose lpar rpar str = lpar ^ str ^ rpar; |
|
677 fun unenclose str = String.substring (str, 1, size str - 2); |
676 |
678 |
677 (*simple quoting (does not escape special chars)*) |
679 (*simple quoting (does not escape special chars)*) |
678 val quote = enclose "\"" "\""; |
680 val quote = enclose "\"" "\""; |
679 |
681 |
680 (*space_implode "..." (explode "hello") = "h...e...l...l...o"*) |
682 (*space_implode "..." (explode "hello") = "h...e...l...l...o"*) |