equal
deleted
inserted
replaced
143 val cartouche: string -> string |
143 val cartouche: string -> string |
144 val space_implode: string -> string list -> string |
144 val space_implode: string -> string list -> string |
145 val commas: string list -> string |
145 val commas: string list -> string |
146 val commas_quote: string list -> string |
146 val commas_quote: string list -> string |
147 val cat_lines: string list -> string |
147 val cat_lines: string list -> string |
148 val terminate_lines: string list -> string |
|
149 val space_explode: string -> string -> string list |
148 val space_explode: string -> string -> string list |
150 val split_lines: string -> string list |
149 val split_lines: string -> string list |
151 val plain_words: string -> string |
150 val plain_words: string -> string |
152 val prefix_lines: string -> string -> string |
151 val prefix_lines: string -> string -> string |
153 val prefix: string -> string -> string |
152 val prefix: string -> string -> string |
747 val commas = space_implode ", "; |
746 val commas = space_implode ", "; |
748 val commas_quote = commas o map quote; |
747 val commas_quote = commas o map quote; |
749 |
748 |
750 val cat_lines = space_implode "\n"; |
749 val cat_lines = space_implode "\n"; |
751 |
750 |
752 fun terminate_lines lines = cat_lines lines ^ "\n"; |
|
753 |
|
754 (*space_explode "." "h.e..l.lo" = ["h", "e", "", "l", "lo"]*) |
751 (*space_explode "." "h.e..l.lo" = ["h", "e", "", "l", "lo"]*) |
755 fun space_explode _ "" = [] |
752 fun space_explode _ "" = [] |
756 | space_explode sep s = String.fields (fn c => str c = sep) s; |
753 | space_explode sep s = String.fields (fn c => str c = sep) s; |
757 |
754 |
758 val split_lines = space_explode "\n"; |
755 val split_lines = space_explode "\n"; |