# HG changeset patch # User wenzelm # Date 1291393767 -3600 # Node ID 10aeae27c7a603ba8519d1f8aaf95946c8ce3c17 # Parent f48c5b951042430bca283b7cfde2c357d7b03930 removed confusing comments (cf. 500171e7aa59); diff -r f48c5b951042 -r 10aeae27c7a6 src/Pure/library.ML --- a/src/Pure/library.ML Fri Dec 03 17:18:41 2010 +0100 +++ b/src/Pure/library.ML Fri Dec 03 17:29:27 2010 +0100 @@ -727,13 +727,11 @@ (*simple quoting (does not escape special chars)*) val quote = enclose "\"" "\""; -(*space_implode "..." (Symbol.explode "hello") = "h...e...l...l...o"*) fun space_implode a bs = implode (separate a bs); val commas = space_implode ", "; val commas_quote = commas o map quote; -(*concatenate messages, one per line, into a string*) val cat_lines = space_implode "\n"; (*space_explode "." "h.e..l.lo" = ["h", "e", "", "l", "lo"]*)