src/Pure/Tools/build_log.scala
changeset 64079 ff26032b7f2a
parent 64063 2c5039363ea3
child 64080 2e5c0bd708af
     1.1 --- a/src/Pure/Tools/build_log.scala	Fri Oct 07 10:46:34 2016 +0200
     1.2 +++ b/src/Pure/Tools/build_log.scala	Fri Oct 07 11:10:17 2016 +0200
     1.3 @@ -134,8 +134,6 @@
     1.4      val afp_version = "afp_version"
     1.5    }
     1.6  
     1.7 -  val ml_settings = List("ML_PLATFORM", "ML_HOME", "ML_SYSTEM", "ML_OPTIONS")
     1.8 -
     1.9    object AFP
    1.10    {
    1.11      val Date_Format =
    1.12 @@ -147,7 +145,6 @@
    1.13      val Test_End = new Regex("""^End test on (.+), \w+, elapsed time:.*$""")
    1.14      val Isabelle_Version = new Regex("""^Isabelle version: .* -- hg id (\w+)$""")
    1.15      val AFP_Version = new Regex("""^AFP version: .* -- hg id (\w+)$""")
    1.16 -    val settings = "ISABELLE_BUILD_OPTIONS" :: ml_settings
    1.17    }
    1.18  
    1.19    private def parse_header(log_file: Log_File): Header =
    1.20 @@ -170,7 +167,7 @@
    1.21                  Field.build_end -> end_date.toString,
    1.22                  Field.isabelle_version -> isabelle_version,
    1.23                  Field.afp_version -> afp_version),
    1.24 -              log_file.get_settings(AFP.settings))
    1.25 +              log_file.get_settings(Build.all_settings))
    1.26  
    1.27            case _ => log_file.err("cannot detect start/end date in afp-test log")
    1.28          }
    1.29 @@ -216,7 +213,7 @@
    1.30          case i =>
    1.31            val a = s.substring(0, i)
    1.32            Library.try_unquote(s.substring(i + 1)) match {
    1.33 -            case Some(b) if Build.ml_options.contains(a) => Some((a, b))
    1.34 +            case Some(b) if Build.ml_settings.contains(a) => Some((a, b))
    1.35              case _ => None
    1.36            }
    1.37        }