tuned signature;
authorwenzelm
Sat Oct 08 15:39:42 2016 +0200 (2016-10-08)
changeset 64105d93bd6d253c6
parent 64104 b70fa05d6746
child 64106 b7ff61d50b19
tuned signature;
src/Pure/Tools/build_log.scala
     1.1 --- a/src/Pure/Tools/build_log.scala	Sat Oct 08 14:55:34 2016 +0200
     1.2 +++ b/src/Pure/Tools/build_log.scala	Sat Oct 08 15:39:42 2016 +0200
     1.3 @@ -192,6 +192,10 @@
     1.4  
     1.5      /* parse various formats */
     1.6  
     1.7 +    def parse_meta_info(): Meta_Info = Build_Log.parse_meta_info(log_file)
     1.8 +
     1.9 +    def parse_build_info(): Build_Info = Build_Log.parse_build_info(log_file)
    1.10 +
    1.11      def parse_session_info(
    1.12          default_name: String = "",
    1.13          command_timings: Boolean = false,
    1.14 @@ -199,15 +203,11 @@
    1.15          task_statistics: Boolean = false): Session_Info =
    1.16        Build_Log.parse_session_info(
    1.17          log_file, default_name, command_timings, ml_statistics, task_statistics)
    1.18 -
    1.19 -    def parse_header(): Header = Build_Log.parse_header(log_file)
    1.20 -
    1.21 -    def parse_build_info(): Build_Info = Build_Log.parse_build_info(log_file)
    1.22    }
    1.23  
    1.24  
    1.25  
    1.26 -  /** meta data **/
    1.27 +  /** meta info **/
    1.28  
    1.29    object Field
    1.30    {
    1.31 @@ -226,12 +226,13 @@
    1.32      val JENKINS = Value("jenkins")
    1.33    }
    1.34  
    1.35 -  object Header
    1.36 +  object Meta_Info
    1.37    {
    1.38 -    val empty: Header = Header(Kind.EMPTY, Nil, Nil)
    1.39 +    val empty: Meta_Info = Meta_Info(Kind.EMPTY, Nil, Nil)
    1.40    }
    1.41  
    1.42 -  sealed case class Header(kind: Kind.Value, props: Properties.T, settings: List[(String, String)])
    1.43 +  sealed case class Meta_Info(
    1.44 +    kind: Kind.Value, props: Properties.T, settings: List[(String, String)])
    1.45    {
    1.46      def is_empty: Boolean = props.isEmpty && settings.isEmpty
    1.47    }
    1.48 @@ -254,10 +255,10 @@
    1.49      val Bad_Init = new Regex("""^cp:.*: Disc quota exceeded$""")
    1.50    }
    1.51  
    1.52 -  private def parse_header(log_file: Log_File): Header =
    1.53 +  private def parse_meta_info(log_file: Log_File): Meta_Info =
    1.54    {
    1.55      def parse(kind: Kind.Value, start: Date, hostname: String,
    1.56 -      Test_End: Regex, Isabelle_Version: Regex, AFP_Version: Regex): Header =
    1.57 +      Test_End: Regex, Isabelle_Version: Regex, AFP_Version: Regex): Meta_Info =
    1.58      {
    1.59        val start_date = Field.build_start -> start.toString
    1.60        val end_date =
    1.61 @@ -275,7 +276,7 @@
    1.62        val afp_version =
    1.63          log_file.find_match(AFP_Version).map(Field.afp_version -> _)
    1.64  
    1.65 -      Header(kind,
    1.66 +      Meta_Info(kind,
    1.67          start_date :: end_date ::: build_host :::
    1.68            isabelle_version.toList ::: afp_version.toList,
    1.69          log_file.get_settings(Settings.all_settings))
    1.70 @@ -294,10 +295,10 @@
    1.71          parse(Kind.AFP_TEST, start, "",
    1.72            AFP.Test_End, AFP.Isabelle_Version, AFP.AFP_Version)
    1.73  
    1.74 -      case line :: _ if line.startsWith("\0") => Header.empty
    1.75 -      case List(Isatest.Test_End(_)) => Header.empty
    1.76 -      case _ :: AFP.Bad_Init() :: _ => Header.empty
    1.77 -      case Nil => Header.empty
    1.78 +      case line :: _ if line.startsWith("\0") => Meta_Info.empty
    1.79 +      case List(Isatest.Test_End(_)) => Meta_Info.empty
    1.80 +      case _ :: AFP.Bad_Init() :: _ => Meta_Info.empty
    1.81 +      case Nil => Meta_Info.empty
    1.82  
    1.83        case _ => log_file.err("cannot detect log header format")
    1.84      }