clarified modules;
authorwenzelm
Fri, 07 Oct 2016 11:24:58 +0200
changeset 64080 2e5c0bd708af
parent 64079 ff26032b7f2a
child 64081 38bb09ed965b
clarified modules; CI_Profile: show all settings;
src/Pure/Tools/build.scala
src/Pure/Tools/build_log.scala
src/Pure/Tools/ci_profile.scala
--- 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)