tuned;
authorwenzelm
Fri Oct 07 11:10:17 2016 +0200 (2016-10-07)
changeset 64079ff26032b7f2a
parent 64078 0b22328a353c
child 64080 2e5c0bd708af
tuned;
src/Pure/Tools/build.scala
src/Pure/Tools/build_log.scala
src/Pure/Tools/ci_profile.scala
     1.1 --- a/src/Pure/Tools/build.scala	Fri Oct 07 10:46:34 2016 +0200
     1.2 +++ b/src/Pure/Tools/build.scala	Fri Oct 07 11:10:17 2016 +0200
     1.3 @@ -686,16 +686,15 @@
     1.4  
     1.5    /* Isabelle tool wrapper */
     1.6  
     1.7 -  val ml_options = List("ML_PLATFORM", "ML_HOME", "ML_SYSTEM", "ML_OPTIONS")
     1.8 +  val build_settings = List("ISABELLE_BUILD_OPTIONS")
     1.9 +  val ml_settings = List("ML_PLATFORM", "ML_HOME", "ML_SYSTEM", "ML_OPTIONS")
    1.10 +  val all_settings = build_settings ::: ml_settings
    1.11  
    1.12    val isabelle_tool = Isabelle_Tool("build", "build and manage Isabelle sessions", args =>
    1.13    {
    1.14 +    def show(a: String): String = a + "=" + quote(Isabelle_System.getenv(a))
    1.15      def show_settings(): String =
    1.16 -      cat_lines(List(
    1.17 -        "ISABELLE_BUILD_OPTIONS=" +
    1.18 -          quote(Isabelle_System.getenv("ISABELLE_BUILD_OPTIONS")),
    1.19 -        "") :::
    1.20 -        ml_options.map(opt => opt + "=" + quote(Isabelle_System.getenv(opt))))
    1.21 +      cat_lines(build_settings.map(show(_)) ::: List("") ::: ml_settings.map(show(_)))
    1.22  
    1.23      val build_options = Word.explode(Isabelle_System.getenv("ISABELLE_BUILD_OPTIONS"))
    1.24  
     2.1 --- a/src/Pure/Tools/build_log.scala	Fri Oct 07 10:46:34 2016 +0200
     2.2 +++ b/src/Pure/Tools/build_log.scala	Fri Oct 07 11:10:17 2016 +0200
     2.3 @@ -134,8 +134,6 @@
     2.4      val afp_version = "afp_version"
     2.5    }
     2.6  
     2.7 -  val ml_settings = List("ML_PLATFORM", "ML_HOME", "ML_SYSTEM", "ML_OPTIONS")
     2.8 -
     2.9    object AFP
    2.10    {
    2.11      val Date_Format =
    2.12 @@ -147,7 +145,6 @@
    2.13      val Test_End = new Regex("""^End test on (.+), \w+, elapsed time:.*$""")
    2.14      val Isabelle_Version = new Regex("""^Isabelle version: .* -- hg id (\w+)$""")
    2.15      val AFP_Version = new Regex("""^AFP version: .* -- hg id (\w+)$""")
    2.16 -    val settings = "ISABELLE_BUILD_OPTIONS" :: ml_settings
    2.17    }
    2.18  
    2.19    private def parse_header(log_file: Log_File): Header =
    2.20 @@ -170,7 +167,7 @@
    2.21                  Field.build_end -> end_date.toString,
    2.22                  Field.isabelle_version -> isabelle_version,
    2.23                  Field.afp_version -> afp_version),
    2.24 -              log_file.get_settings(AFP.settings))
    2.25 +              log_file.get_settings(Build.all_settings))
    2.26  
    2.27            case _ => log_file.err("cannot detect start/end date in afp-test log")
    2.28          }
    2.29 @@ -216,7 +213,7 @@
    2.30          case i =>
    2.31            val a = s.substring(0, i)
    2.32            Library.try_unquote(s.substring(i + 1)) match {
    2.33 -            case Some(b) if Build.ml_options.contains(a) => Some((a, b))
    2.34 +            case Some(b) if Build.ml_settings.contains(a) => Some((a, b))
    2.35              case _ => None
    2.36            }
    2.37        }
     3.1 --- a/src/Pure/Tools/ci_profile.scala	Fri Oct 07 10:46:34 2016 +0200
     3.2 +++ b/src/Pure/Tools/ci_profile.scala	Fri Oct 07 11:10:17 2016 +0200
     3.3 @@ -86,7 +86,7 @@
     3.4    override final def apply(args: List[String]): Unit =
     3.5    {
     3.6      print_section("CONFIGURATION")
     3.7 -    Build.ml_options.foreach(opt => println(opt + "=" + quote(Isabelle_System.getenv(opt))))
     3.8 +    Build.ml_settings.foreach(a => println(a + "=" + quote(Isabelle_System.getenv(a))))
     3.9      val props = load_properties()
    3.10      System.getProperties().putAll(props)
    3.11