tuned;
authorwenzelm
Tue May 09 20:02:31 2017 +0200 (2017-05-09)
changeset 65791cf48ef4f4e63
parent 65790 91940684a267
child 65792 c58752102b34
tuned;
src/Pure/Admin/build_status.scala
     1.1 --- a/src/Pure/Admin/build_status.scala	Tue May 09 19:57:04 2017 +0200
     1.2 +++ b/src/Pure/Admin/build_status.scala	Tue May 09 20:02:31 2017 +0200
     1.3 @@ -9,6 +9,28 @@
     1.4  
     1.5  object Build_Status
     1.6  {
     1.7 +  /* data profiles */
     1.8 +
     1.9 +  sealed case class Profile(description: String, sql: String)
    1.10 +  {
    1.11 +    def select(columns: List[SQL.Column], days: Int, only_sessions: Set[String]): SQL.Source =
    1.12 +    {
    1.13 +      val sql_sessions =
    1.14 +        if (only_sessions.isEmpty) ""
    1.15 +        else
    1.16 +          only_sessions.iterator.map(a => Build_Log.Data.session_name + " = " + SQL.string(a))
    1.17 +            .mkString("(", " OR ", ") AND ")
    1.18 +
    1.19 +      Build_Log.Data.universal_table.select(columns, distinct = true,
    1.20 +        sql = "WHERE " +
    1.21 +          Build_Log.Data.pull_date + " > " + Build_Log.Data.recent_time(days) + " AND " +
    1.22 +          Build_Log.Data.status + " = " + SQL.string(Build_Log.Session_Status.finished.toString) +
    1.23 +          " AND " + sql_sessions + SQL.enclose(sql) +
    1.24 +          " ORDER BY " + Build_Log.Data.pull_date + " DESC")
    1.25 +    }
    1.26 +  }
    1.27 +
    1.28 +
    1.29    /* build status */
    1.30  
    1.31    val default_target_dir = Path.explode("build_status")
    1.32 @@ -33,30 +55,7 @@
    1.33    }
    1.34  
    1.35  
    1.36 -  /* data profiles */
    1.37 -
    1.38 -  def clean_name(name: String): String =
    1.39 -    name.flatMap(c => if (c == ' ' || c == '/') "_" else if (c == ',') "" else c.toString)
    1.40 -
    1.41 -  sealed case class Profile(description: String, sql: String)
    1.42 -  {
    1.43 -    def select(columns: List[SQL.Column], days: Int, only_sessions: Set[String]): SQL.Source =
    1.44 -    {
    1.45 -      val sql_sessions =
    1.46 -        if (only_sessions.isEmpty) ""
    1.47 -        else
    1.48 -          only_sessions.iterator.map(a => Build_Log.Data.session_name + " = " + SQL.string(a))
    1.49 -            .mkString("(", " OR ", ") AND ")
    1.50 -
    1.51 -      Build_Log.Data.universal_table.select(columns, distinct = true,
    1.52 -        sql = "WHERE " +
    1.53 -          Build_Log.Data.pull_date + " > " + Build_Log.Data.recent_time(days) + " AND " +
    1.54 -          Build_Log.Data.status + " = " + SQL.string(Build_Log.Session_Status.finished.toString) +
    1.55 -          " AND " + sql_sessions + SQL.enclose(sql) +
    1.56 -          " ORDER BY " + Build_Log.Data.pull_date + " DESC")
    1.57 -    }
    1.58 -  }
    1.59 -
    1.60 +  /* read data */
    1.61  
    1.62    sealed case class Data(date: Date, entries: List[(String, List[Session])])
    1.63    sealed case class Session(name: String, threads: Int, entries: List[Entry])
    1.64 @@ -70,9 +69,6 @@
    1.65    }
    1.66    sealed case class Entry(date: Date, timing: Timing, ml_timing: Timing, heap_size: Long)
    1.67  
    1.68 -
    1.69 -  /* read data */
    1.70 -
    1.71    def read_data(options: Options,
    1.72      progress: Progress = No_Progress,
    1.73      profiles: List[Profile] = default_profiles,
    1.74 @@ -165,6 +161,9 @@
    1.75      target_dir: Path = default_target_dir,
    1.76      image_size: (Int, Int) = default_image_size)
    1.77    {
    1.78 +    def clean_name(name: String): String =
    1.79 +      name.flatMap(c => if (c == ' ' || c == '/') "_" else if (c == ',') "" else c.toString)
    1.80 +
    1.81      Isabelle_System.mkdirs(target_dir)
    1.82      File.write(target_dir + Path.basic("index.html"),
    1.83        HTML.output_document(