--- a/src/Pure/Tools/build.scala Fri Oct 07 11:10:17 2016 +0200
+++ b/src/Pure/Tools/build.scala Fri Oct 07 11:24:58 2016 +0200
@@ -686,16 +686,8 @@
/* Isabelle tool wrapper */
- val build_settings = List("ISABELLE_BUILD_OPTIONS")
- val ml_settings = List("ML_PLATFORM", "ML_HOME", "ML_SYSTEM", "ML_OPTIONS")
- val all_settings = build_settings ::: ml_settings
-
val isabelle_tool = Isabelle_Tool("build", "build and manage Isabelle sessions", args =>
{
- def show(a: String): String = a + "=" + quote(Isabelle_System.getenv(a))
- def show_settings(): String =
- cat_lines(build_settings.map(show(_)) ::: List("") ::: ml_settings.map(show(_)))
-
val build_options = Word.explode(Isabelle_System.getenv("ISABELLE_BUILD_OPTIONS"))
var select_dirs: List[Path] = Nil
@@ -738,7 +730,7 @@
Build and manage Isabelle sessions, depending on implicit settings:
-""" + Library.prefix_lines(" ", show_settings()),
+""" + Library.prefix_lines(" ", Build_Log.Setting.show_all()),
"D:" -> (arg => select_dirs = select_dirs ::: List(Path.explode(arg))),
"R" -> (_ => requirements = true),
"X:" -> (arg => exclude_session_groups = exclude_session_groups ::: List(arg)),
@@ -765,7 +757,7 @@
Library.trim_line(
Isabelle_System.bash(
"""echo "Started at $(date) ($ML_IDENTIFIER on $(hostname))" """).out) + "\n")
- progress.echo(show_settings() + "\n")
+ progress.echo(Build_Log.Setting.show_all() + "\n")
}
val start_time = Time.now()
--- a/src/Pure/Tools/build_log.scala Fri Oct 07 11:10:17 2016 +0200
+++ b/src/Pure/Tools/build_log.scala Fri Oct 07 11:24:58 2016 +0200
@@ -16,6 +16,22 @@
object Build_Log
{
+ /** build settings **/
+
+ val build_settings = List("ISABELLE_BUILD_OPTIONS")
+ val ml_settings = List("ML_PLATFORM", "ML_HOME", "ML_SYSTEM", "ML_OPTIONS")
+ val all_settings = build_settings ::: ml_settings
+
+ object Setting
+ {
+ def apply(a: String, b: String): String = a + "=" + quote(b)
+ def getenv(a: String): String = apply(a, Isabelle_System.getenv(a))
+
+ def show_all(): String =
+ cat_lines(build_settings.map(getenv(_)) ::: List("") ::: ml_settings.map(getenv(_)))
+ }
+
+
/** log file **/
object Log_File
@@ -167,7 +183,7 @@
Field.build_end -> end_date.toString,
Field.isabelle_version -> isabelle_version,
Field.afp_version -> afp_version),
- log_file.get_settings(Build.all_settings))
+ log_file.get_settings(all_settings))
case _ => log_file.err("cannot detect start/end date in afp-test log")
}
@@ -213,7 +229,7 @@
case i =>
val a = s.substring(0, i)
Library.try_unquote(s.substring(i + 1)) match {
- case Some(b) if Build.ml_settings.contains(a) => Some((a, b))
+ case Some(b) if ml_settings.contains(a) => Some((a, b))
case _ => None
}
}
--- a/src/Pure/Tools/ci_profile.scala Fri Oct 07 11:10:17 2016 +0200
+++ b/src/Pure/Tools/ci_profile.scala Fri Oct 07 11:24:58 2016 +0200
@@ -86,7 +86,7 @@
override final def apply(args: List[String]): Unit =
{
print_section("CONFIGURATION")
- Build.ml_settings.foreach(a => println(a + "=" + quote(Isabelle_System.getenv(a))))
+ println(Build_Log.Setting.show_all())
val props = load_properties()
System.getProperties().putAll(props)