changeset 73736 | a8ff6e4ee661 |
parent 73573 | a30a60aef59f |
child 73963 | 59b6f0462086 |
--- a/src/Pure/library.scala Tue May 18 22:02:21 2021 +0200 +++ b/src/Pure/library.scala Wed May 19 10:41:28 2021 +0200 @@ -107,6 +107,9 @@ def prefix_lines(prfx: String, str: String): String = if (str == "") str else cat_lines(split_lines(str).map(prfx + _)) + def indent_lines(n: Int, str: String): String = + prefix_lines(Symbol.spaces(n), str) + def first_line(source: CharSequence): String = { val lines = separated_chunks(_ == '\n', source)