--- 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),
--- 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
}
--- 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),
--- 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))),
--- 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" +
--- 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)