# HG changeset patch
# User wenzelm
# Date 1621413688 -7200
# Node ID a8ff6e4ee6613c9eb7e514d2bde8f3896fb9ef11
# Parent  26cd26aaf108bf514fed3a44213ad75539376be9
tuned signature;

diff -r 26cd26aaf108 -r a8ff6e4ee661 src/Pure/Admin/components.scala
--- a/src/Pure/Admin/components.scala	Tue May 18 22:02:21 2021 +0200
+++ b/src/Pure/Admin/components.scala	Wed May 19 10:41:28 2021 +0200
@@ -339,7 +339,7 @@
   Build and publish Isabelle components as .tar.gz archives on SSH server,
   depending on system options:
 
-""" + Library.prefix_lines("  ", show_options) + "\n",
+""" + Library.indent_lines(2, show_options) + "\n",
         "P" -> (_ => publish = true),
         "f" -> (_ => force = true),
         "o:" -> (arg => options = options + arg),
diff -r 26cd26aaf108 -r a8ff6e4ee661 src/Pure/Thy/latex.scala
--- a/src/Pure/Thy/latex.scala	Tue May 18 22:02:21 2021 +0200
+++ b/src/Pure/Thy/latex.scala	Wed May 19 10:41:28 2021 +0200
@@ -22,7 +22,7 @@
     val root_log_path = dir + Path.explode(root_name).ext("log")
     if (root_log_path.is_file) {
       for { (msg, pos) <- filter_errors(dir, File.read(root_log_path)) }
-      yield "Latex error" + Position.here(pos) + ":\n" + Library.prefix_lines("  ", msg)
+      yield "Latex error" + Position.here(pos) + ":\n" + Library.indent_lines(2, msg)
     }
     else Nil
   }
diff -r 26cd26aaf108 -r a8ff6e4ee661 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Tue May 18 22:02:21 2021 +0200
+++ b/src/Pure/Tools/build.scala	Wed May 19 10:41:28 2021 +0200
@@ -576,7 +576,7 @@
 
   Build and manage Isabelle sessions, depending on implicit settings:
 
-""" + Library.prefix_lines("  ",  Build_Log.Settings.show()) + "\n",
+""" + Library.indent_lines(2,  Build_Log.Settings.show()) + "\n",
       "B:" -> (arg => base_sessions = base_sessions ::: List(arg)),
       "D:" -> (arg => select_dirs = select_dirs ::: List(Path.explode(arg))),
       "N" -> (_ => numa_shuffling = true),
diff -r 26cd26aaf108 -r a8ff6e4ee661 src/Pure/Tools/dump.scala
--- a/src/Pure/Tools/dump.scala	Tue May 18 22:02:21 2021 +0200
+++ b/src/Pure/Tools/dump.scala	Wed May 19 10:41:28 2021 +0200
@@ -456,7 +456,7 @@
 
   Dump cumulative PIDE session database, with the following aspects:
 
-""" + Library.prefix_lines("    ", show_aspects) + "\n",
+""" + Library.indent_lines(4, show_aspects) + "\n",
       "A:" -> (arg => aspects = Library.distinct(space_explode(',', arg)).map(the_aspect)),
       "B:" -> (arg => base_sessions = base_sessions ::: List(arg)),
       "D:" -> (arg => select_dirs = select_dirs ::: List(Path.explode(arg))),
diff -r 26cd26aaf108 -r a8ff6e4ee661 src/Pure/Tools/phabricator.scala
--- a/src/Pure/Tools/phabricator.scala	Tue May 18 22:02:21 2021 +0200
+++ b/src/Pure/Tools/phabricator.scala	Wed May 19 10:41:28 2021 +0200
@@ -91,7 +91,7 @@
     NAME="$(echo "$REPLY" | cut -d: -f1)"
     ROOT="$(echo "$REPLY" | cut -d: -f2)"
     {
-""" + Library.prefix_lines("      ", body) + """
+""" + Library.indent_lines(6, body) + """
     } < /dev/null
   done
 } < """ + File.bash_path(global_config) + "\n" +
diff -r 26cd26aaf108 -r a8ff6e4ee661 src/Pure/library.scala
--- 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)