# HG changeset patch
# User wenzelm
# Date 1475833530 -7200
# Node ID 38bb09ed965b6ce70443d6419c0569c7c9feb321
# Parent  2e5c0bd708af8f980afcd90e079c55940d8b724e
more uniform treatment of settings;

diff -r 2e5c0bd708af -r 38bb09ed965b src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Fri Oct 07 11:24:58 2016 +0200
+++ b/src/Pure/Tools/build.scala	Fri Oct 07 11:45:30 2016 +0200
@@ -730,7 +730,7 @@
 
   Build and manage Isabelle sessions, depending on implicit settings:
 
-""" + Library.prefix_lines("  ", Build_Log.Setting.show_all()),
+""" + Library.prefix_lines("  ", Build_Log.Settings.show()),
       "D:" -> (arg => select_dirs = select_dirs ::: List(Path.explode(arg))),
       "R" -> (_ => requirements = true),
       "X:" -> (arg => exclude_session_groups = exclude_session_groups ::: List(arg)),
@@ -757,7 +757,7 @@
         Library.trim_line(
           Isabelle_System.bash(
             """echo "Started at $(date) ($ML_IDENTIFIER on $(hostname))" """).out) + "\n")
-      progress.echo(Build_Log.Setting.show_all() + "\n")
+      progress.echo(Build_Log.Settings.show() + "\n")
     }
 
     val start_time = Time.now()
diff -r 2e5c0bd708af -r 38bb09ed965b src/Pure/Tools/build_log.scala
--- a/src/Pure/Tools/build_log.scala	Fri Oct 07 11:24:58 2016 +0200
+++ b/src/Pure/Tools/build_log.scala	Fri Oct 07 11:45:30 2016 +0200
@@ -16,19 +16,34 @@
 
 object Build_Log
 {
-  /** build settings **/
+  /** 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 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
+
+    type Entry = (String, String)
+    type T = List[Entry]
 
-  object Setting
-  {
-    def apply(a: String, b: String): String = a + "=" + quote(b)
-    def getenv(a: String): String = apply(a, Isabelle_System.getenv(a))
+    object Entry
+    {
+      def unapply(s: String): Option[Entry] =
+        s.indexOf('=') match {
+          case -1 => None
+          case i =>
+            val a = s.substring(0, i)
+            val b = Library.perhaps_unquote(s.substring(i + 1))
+            Some((a, b))
+        }
+      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(_)))
+    def show(): String =
+      cat_lines(
+        build_settings.map(Entry.getenv(_)) ::: List("") ::: ml_settings.map(Entry.getenv(_)))
   }
 
 
@@ -67,11 +82,11 @@
 
     /* settings */
 
-    def get_setting(setting: String): String =
-      lines.find(_.startsWith(setting + "=")) getOrElse err("missing " + setting)
+    def get_setting(a: String): Settings.Entry =
+      Settings.Entry.unapply(
+        lines.find(_.startsWith(a + "=")) getOrElse err("missing " + a)).get
 
-    def get_settings(settings: List[String]): List[String] =
-      settings.map(get_setting(_))
+    def get_settings(as: List[String]): Settings.T = as.map(get_setting(_))
 
 
     /* properties (YXML) */
@@ -139,7 +154,8 @@
     val JENKINS = Value("jenkins")
   }
 
-  sealed case class Header(kind: Header_Kind.Value, props: Properties.T, settings: List[String])
+  sealed case class Header(
+    kind: Header_Kind.Value, props: Properties.T, settings: List[(String, String)])
 
   object Field
   {
@@ -183,7 +199,7 @@
                 Field.build_end -> end_date.toString,
                 Field.isabelle_version -> isabelle_version,
                 Field.afp_version -> afp_version),
-              log_file.get_settings(all_settings))
+              log_file.get_settings(Settings.all_settings))
 
           case _ => log_file.err("cannot detect start/end date in afp-test log")
         }
@@ -203,7 +219,7 @@
   /* main log: produced by isatest, afp-test, jenkins etc. */
 
   sealed case class Info(
-    ml_options: List[(String, String)],
+    settings: List[(String, String)],
     finished: Map[String, Timing],
     timing: Map[String, Timing],
     threads: Map[String, Int])
@@ -221,23 +237,9 @@
   private val Session_Timing =
     new Regex("""^Timing (\S+) \((\d) threads, (\d+\.\d+)s elapsed time, (\d+\.\d+)s cpu time, (\d+\.\d+)s GC time.*$""")
 
-  private object ML_Option
-  {
-    def unapply(s: String): Option[(String, String)] =
-      s.indexOf('=') match {
-        case -1 => None
-        case i =>
-          val a = s.substring(0, i)
-          Library.try_unquote(s.substring(i + 1)) match {
-            case Some(b) if ml_settings.contains(a) => Some((a, b))
-            case _ => None
-          }
-      }
-  }
-
   private def parse_info(log_file: Log_File): Info =
   {
-    val ml_options = new mutable.ListBuffer[(String, String)]
+    val settings = new mutable.ListBuffer[(String, String)]
     var finished = Map.empty[String, Timing]
     var timing = Map.empty[String, Timing]
     var threads = Map.empty[String, Int]
@@ -261,11 +263,12 @@
           val gc = Time.seconds(g)
           timing += (name -> Timing(elapsed, cpu, gc))
           threads += (name -> t)
-        case ML_Option(a, b) => ml_options += (a -> b)
+        case Settings.Entry(a, b) if Settings.all_settings.contains(a) =>
+          settings += (a -> b)
         case _ =>
       }
     }
 
-    Info(ml_options.toList, finished, timing, threads)
+    Info(settings.toList, finished, timing, threads)
   }
 }
diff -r 2e5c0bd708af -r 38bb09ed965b src/Pure/Tools/ci_profile.scala
--- a/src/Pure/Tools/ci_profile.scala	Fri Oct 07 11:24:58 2016 +0200
+++ b/src/Pure/Tools/ci_profile.scala	Fri Oct 07 11:45:30 2016 +0200
@@ -86,7 +86,7 @@
   override final def apply(args: List[String]): Unit =
   {
     print_section("CONFIGURATION")
-    println(Build_Log.Setting.show_all())
+    println(Build_Log.Settings.show())
     val props = load_properties()
     System.getProperties().putAll(props)