# HG changeset patch
# User wenzelm
# Date 1475831417 -7200
# Node ID ff26032b7f2abee5f9f83d50532272199e5649dc
# Parent  0b22328a353cdd5c5a7104d125d31a8675ddeecb
tuned;

diff -r 0b22328a353c -r ff26032b7f2a src/Pure/Tools/build.scala
--- 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"))
 
diff -r 0b22328a353c -r ff26032b7f2a src/Pure/Tools/build_log.scala
--- 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
           }
       }
diff -r 0b22328a353c -r ff26032b7f2a src/Pure/Tools/ci_profile.scala
--- 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)