more uniform output;

--- a/src/Pure/Tools/build.scala	Sat Aug 13 07:58:14 2016 +0200
+++ b/src/Pure/Tools/build.scala	Sat Aug 13 12:05:53 2016 +0200
@@ -728,17 +728,16 @@
 
   /* Isabelle tool wrapper */
 
+  val ml_options = List("ML_PLATFORM", "ML_HOME", "ML_SYSTEM", "ML_OPTIONS")
+
   val isabelle_tool = Isabelle_Tool("build", "build and manage Isabelle sessions", args =>
   {
     def show_settings(): String =
       cat_lines(List(
         "ISABELLE_BUILD_OPTIONS=" +
           quote(Isabelle_System.getenv("ISABELLE_BUILD_OPTIONS")),
-        "",
-        "ML_PLATFORM=" + quote(Isabelle_System.getenv("ML_PLATFORM")),
-        "ML_HOME=" + quote(Isabelle_System.getenv("ML_HOME")),
-        "ML_SYSTEM=" + quote(Isabelle_System.getenv("ML_SYSTEM")),
-        "ML_OPTIONS=" + quote(Isabelle_System.getenv("ML_OPTIONS"))))
+        "") :::
+        ml_options.map(opt => opt + "=" + quote(Isabelle_System.getenv(opt))))
 
     val build_options = Word.explode(Isabelle_System.getenv("ISABELLE_BUILD_OPTIONS"))
 

--- a/src/Pure/Tools/ci_profile.scala	Sat Aug 13 07:58:14 2016 +0200
+++ b/src/Pure/Tools/ci_profile.scala	Sat Aug 13 12:05:53 2016 +0200
@@ -14,13 +14,6 @@
 
 abstract class CI_Profile extends Isabelle_Tool.Body
 {
-
-  private def print_variable(name: String): Unit =
-  {
-    val value = Isabelle_System.getenv_strict(name)
-    println(name + "=" + Outer_Syntax.quote_string(value))
-  }
-
   private def build(options: Options): (Build.Results, Time) =
   {
     val progress = new Console_Progress(true)
@@ -82,7 +75,7 @@
   override final def apply(args: List[String]): Unit =
   {
     print_section("CONFIGURATION")
-    List("ML_PLATFORM", "ML_HOME", "ML_SYSTEM", "ML_OPTIONS").foreach(print_variable)
+    Build.ml_options.foreach(opt => println(opt + "=" + quote(Isabelle_System.getenv(opt))))
     val props = load_properties()
     System.getProperties().putAll(props)
 
@@ -143,5 +136,4 @@
   def post_hook(results: Build.Results): Unit
 
   def select_sessions(tree: Sessions.Tree): (List[String], Sessions.Tree)
-
 }