| changeset 67435 | f83c1842a559 |
| parent 67389 | 7e21d19e7ad7 |
| child 67438 | fdb7b995974d |
--- a/src/Pure/General/symbol.scala Sun Jan 14 20:39:27 2018 +0100 +++ b/src/Pure/General/symbol.scala Sun Jan 14 20:58:41 2018 +0100 @@ -132,6 +132,9 @@ def length(text: CharSequence): Int = iterator(text).length + def trim_blanks(text: CharSequence): String = + Library.trim(is_blank(_), explode(text)).mkString + /* decoding offsets */