--- a/src/Pure/Tools/build.scala Fri Oct 07 10:46:34 2016 +0200
+++ b/src/Pure/Tools/build.scala Fri Oct 07 11:10:17 2016 +0200
@@ -686,16 +686,15 @@
/* Isabelle tool wrapper */
- val ml_options = List("ML_PLATFORM", "ML_HOME", "ML_SYSTEM", "ML_OPTIONS")
+ 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(List(
- "ISABELLE_BUILD_OPTIONS=" +
- quote(Isabelle_System.getenv("ISABELLE_BUILD_OPTIONS")),
- "") :::
- ml_options.map(opt => opt + "=" + quote(Isabelle_System.getenv(opt))))
+ cat_lines(build_settings.map(show(_)) ::: List("") ::: ml_settings.map(show(_)))
val build_options = Word.explode(Isabelle_System.getenv("ISABELLE_BUILD_OPTIONS"))
--- a/src/Pure/Tools/build_log.scala Fri Oct 07 10:46:34 2016 +0200
+++ b/src/Pure/Tools/build_log.scala Fri Oct 07 11:10:17 2016 +0200
@@ -134,8 +134,6 @@
val afp_version = "afp_version"
}
- val ml_settings = List("ML_PLATFORM", "ML_HOME", "ML_SYSTEM", "ML_OPTIONS")
-
object AFP
{
val Date_Format =
@@ -147,7 +145,6 @@
val Test_End = new Regex("""^End test on (.+), \w+, elapsed time:.*$""")
val Isabelle_Version = new Regex("""^Isabelle version: .* -- hg id (\w+)$""")
val AFP_Version = new Regex("""^AFP version: .* -- hg id (\w+)$""")
- val settings = "ISABELLE_BUILD_OPTIONS" :: ml_settings
}
private def parse_header(log_file: Log_File): Header =
@@ -170,7 +167,7 @@
Field.build_end -> end_date.toString,
Field.isabelle_version -> isabelle_version,
Field.afp_version -> afp_version),
- log_file.get_settings(AFP.settings))
+ log_file.get_settings(Build.all_settings))
case _ => log_file.err("cannot detect start/end date in afp-test log")
}
@@ -216,7 +213,7 @@
case i =>
val a = s.substring(0, i)
Library.try_unquote(s.substring(i + 1)) match {
- case Some(b) if Build.ml_options.contains(a) => Some((a, b))
+ case Some(b) if Build.ml_settings.contains(a) => Some((a, b))
case _ => None
}
}
--- a/src/Pure/Tools/ci_profile.scala Fri Oct 07 10:46:34 2016 +0200
+++ b/src/Pure/Tools/ci_profile.scala Fri Oct 07 11:10:17 2016 +0200
@@ -86,7 +86,7 @@
override final def apply(args: List[String]): Unit =
{
print_section("CONFIGURATION")
- Build.ml_options.foreach(opt => println(opt + "=" + quote(Isabelle_System.getenv(opt))))
+ Build.ml_settings.foreach(a => println(a + "=" + quote(Isabelle_System.getenv(a))))
val props = load_properties()
System.getProperties().putAll(props)