--- a/src/Doc/System/Sessions.thy Sat Jun 27 11:25:30 2020 +0200
+++ b/src/Doc/System/Sessions.thy Wed Jul 01 21:14:04 2020 +0200
@@ -319,6 +319,7 @@
Build and manage Isabelle sessions, depending on implicit settings:
+ ISABELLE_TOOL_JAVA_OPTIONS="..."
ISABELLE_BUILD_OPTIONS="..."
ML_PLATFORM="..."
--- a/src/Pure/Admin/build_log.scala Sat Jun 27 11:25:30 2020 +0200
+++ b/src/Pure/Admin/build_log.scala Wed Jul 01 21:14:04 2020 +0200
@@ -71,8 +71,9 @@
def getenv(a: String): String = apply(a, Isabelle_System.getenv(a))
}
- def show(): String =
+ def show(verbose: Boolean = false): String =
cat_lines(
+ (if (verbose) List(Entry.getenv("ISABELLE_TOOL_JAVA_OPTIONS")) else Nil) :::
List(Entry.getenv(ISABELLE_BUILD_OPTIONS.name), "") :::
ml_settings.map(c => Entry.getenv(c.name)))
}
--- a/src/Pure/Tools/build.scala Sat Jun 27 11:25:30 2020 +0200
+++ b/src/Pure/Tools/build.scala Wed Jul 01 21:14:04 2020 +0200
@@ -847,7 +847,7 @@
Build and manage Isabelle sessions, depending on implicit settings:
-""" + Library.prefix_lines(" ", Build_Log.Settings.show()) + "\n",
+""" + Library.prefix_lines(" ", Build_Log.Settings.show(verbose = true)) + "\n",
"B:" -> (arg => base_sessions = base_sessions ::: List(arg)),
"D:" -> (arg => select_dirs = select_dirs ::: List(Path.explode(arg))),
"N" -> (_ => numa_shuffling = true),