src/Pure/Tools/build_log.scala
changeset 64081 38bb09ed965b
parent 64080 2e5c0bd708af
child 64082 d57c7295f601
     1.1 --- a/src/Pure/Tools/build_log.scala	Fri Oct 07 11:24:58 2016 +0200
     1.2 +++ b/src/Pure/Tools/build_log.scala	Fri Oct 07 11:45:30 2016 +0200
     1.3 @@ -16,19 +16,34 @@
     1.4  
     1.5  object Build_Log
     1.6  {
     1.7 -  /** build settings **/
     1.8 +  /** settings **/
     1.9  
    1.10 -  val build_settings = List("ISABELLE_BUILD_OPTIONS")
    1.11 -  val ml_settings = List("ML_PLATFORM", "ML_HOME", "ML_SYSTEM", "ML_OPTIONS")
    1.12 -  val all_settings = build_settings ::: ml_settings
    1.13 +  object Settings
    1.14 +  {
    1.15 +    val build_settings = List("ISABELLE_BUILD_OPTIONS")
    1.16 +    val ml_settings = List("ML_PLATFORM", "ML_HOME", "ML_SYSTEM", "ML_OPTIONS")
    1.17 +    val all_settings = build_settings ::: ml_settings
    1.18 +
    1.19 +    type Entry = (String, String)
    1.20 +    type T = List[Entry]
    1.21  
    1.22 -  object Setting
    1.23 -  {
    1.24 -    def apply(a: String, b: String): String = a + "=" + quote(b)
    1.25 -    def getenv(a: String): String = apply(a, Isabelle_System.getenv(a))
    1.26 +    object Entry
    1.27 +    {
    1.28 +      def unapply(s: String): Option[Entry] =
    1.29 +        s.indexOf('=') match {
    1.30 +          case -1 => None
    1.31 +          case i =>
    1.32 +            val a = s.substring(0, i)
    1.33 +            val b = Library.perhaps_unquote(s.substring(i + 1))
    1.34 +            Some((a, b))
    1.35 +        }
    1.36 +      def apply(a: String, b: String): String = a + "=" + quote(b)
    1.37 +      def getenv(a: String): String = apply(a, Isabelle_System.getenv(a))
    1.38 +    }
    1.39  
    1.40 -    def show_all(): String =
    1.41 -      cat_lines(build_settings.map(getenv(_)) ::: List("") ::: ml_settings.map(getenv(_)))
    1.42 +    def show(): String =
    1.43 +      cat_lines(
    1.44 +        build_settings.map(Entry.getenv(_)) ::: List("") ::: ml_settings.map(Entry.getenv(_)))
    1.45    }
    1.46  
    1.47  
    1.48 @@ -67,11 +82,11 @@
    1.49  
    1.50      /* settings */
    1.51  
    1.52 -    def get_setting(setting: String): String =
    1.53 -      lines.find(_.startsWith(setting + "=")) getOrElse err("missing " + setting)
    1.54 +    def get_setting(a: String): Settings.Entry =
    1.55 +      Settings.Entry.unapply(
    1.56 +        lines.find(_.startsWith(a + "=")) getOrElse err("missing " + a)).get
    1.57  
    1.58 -    def get_settings(settings: List[String]): List[String] =
    1.59 -      settings.map(get_setting(_))
    1.60 +    def get_settings(as: List[String]): Settings.T = as.map(get_setting(_))
    1.61  
    1.62  
    1.63      /* properties (YXML) */
    1.64 @@ -139,7 +154,8 @@
    1.65      val JENKINS = Value("jenkins")
    1.66    }
    1.67  
    1.68 -  sealed case class Header(kind: Header_Kind.Value, props: Properties.T, settings: List[String])
    1.69 +  sealed case class Header(
    1.70 +    kind: Header_Kind.Value, props: Properties.T, settings: List[(String, String)])
    1.71  
    1.72    object Field
    1.73    {
    1.74 @@ -183,7 +199,7 @@
    1.75                  Field.build_end -> end_date.toString,
    1.76                  Field.isabelle_version -> isabelle_version,
    1.77                  Field.afp_version -> afp_version),
    1.78 -              log_file.get_settings(all_settings))
    1.79 +              log_file.get_settings(Settings.all_settings))
    1.80  
    1.81            case _ => log_file.err("cannot detect start/end date in afp-test log")
    1.82          }
    1.83 @@ -203,7 +219,7 @@
    1.84    /* main log: produced by isatest, afp-test, jenkins etc. */
    1.85  
    1.86    sealed case class Info(
    1.87 -    ml_options: List[(String, String)],
    1.88 +    settings: List[(String, String)],
    1.89      finished: Map[String, Timing],
    1.90      timing: Map[String, Timing],
    1.91      threads: Map[String, Int])
    1.92 @@ -221,23 +237,9 @@
    1.93    private val Session_Timing =
    1.94      new Regex("""^Timing (\S+) \((\d) threads, (\d+\.\d+)s elapsed time, (\d+\.\d+)s cpu time, (\d+\.\d+)s GC time.*$""")
    1.95  
    1.96 -  private object ML_Option
    1.97 -  {
    1.98 -    def unapply(s: String): Option[(String, String)] =
    1.99 -      s.indexOf('=') match {
   1.100 -        case -1 => None
   1.101 -        case i =>
   1.102 -          val a = s.substring(0, i)
   1.103 -          Library.try_unquote(s.substring(i + 1)) match {
   1.104 -            case Some(b) if ml_settings.contains(a) => Some((a, b))
   1.105 -            case _ => None
   1.106 -          }
   1.107 -      }
   1.108 -  }
   1.109 -
   1.110    private def parse_info(log_file: Log_File): Info =
   1.111    {
   1.112 -    val ml_options = new mutable.ListBuffer[(String, String)]
   1.113 +    val settings = new mutable.ListBuffer[(String, String)]
   1.114      var finished = Map.empty[String, Timing]
   1.115      var timing = Map.empty[String, Timing]
   1.116      var threads = Map.empty[String, Int]
   1.117 @@ -261,11 +263,12 @@
   1.118            val gc = Time.seconds(g)
   1.119            timing += (name -> Timing(elapsed, cpu, gc))
   1.120            threads += (name -> t)
   1.121 -        case ML_Option(a, b) => ml_options += (a -> b)
   1.122 +        case Settings.Entry(a, b) if Settings.all_settings.contains(a) =>
   1.123 +          settings += (a -> b)
   1.124          case _ =>
   1.125        }
   1.126      }
   1.127  
   1.128 -    Info(ml_options.toList, finished, timing, threads)
   1.129 +    Info(settings.toList, finished, timing, threads)
   1.130    }
   1.131  }