src/Pure/library.scala
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)