src/Pure/Admin/build_status.scala
changeset 65754 05c6a29c9132
parent 65752 ed7b5cd3a7f2
child 65755 21b4bfa6d204
     1.1 --- a/src/Pure/Admin/build_status.scala	Sun May 07 16:04:19 2017 +0200
     1.2 +++ b/src/Pure/Admin/build_status.scala	Sun May 07 16:14:49 2017 +0200
     1.3 @@ -44,7 +44,12 @@
     1.4        !timing.is_zero && timing.elapsed >= elapsed_threshold
     1.5    }
     1.6  
     1.7 -  type Data = Map[String, Map[String, List[Entry]]]
     1.8 +  sealed case class Data(date: Date, entries: Map[String, Map[String, List[Entry]]])
     1.9 +  {
    1.10 +    def sorted_entries: List[(String, List[(String, List[Entry])])] =
    1.11 +      entries.toList.sortBy(_._1).map({ case (name, session_entries) =>
    1.12 +        (name, session_entries.toList.sortBy(_._2.head.timing.elapsed.ms).reverse) })
    1.13 +  }
    1.14  
    1.15  
    1.16    /* read data */
    1.17 @@ -57,7 +62,8 @@
    1.18      elapsed_threshold: Time = Time.zero,
    1.19      verbose: Boolean = false): Data =
    1.20    {
    1.21 -    var data: Data = Map.empty
    1.22 +    val date = Date.now()
    1.23 +    var data_entries = Map.empty[String, Map[String, List[Entry]]]
    1.24  
    1.25      val store = Build_Log.store(options)
    1.26      using(store.open_database())(db =>
    1.27 @@ -113,51 +119,43 @@
    1.28                    Build_Log.Data.ml_timing_cpu,
    1.29                    Build_Log.Data.ml_timing_gc))
    1.30  
    1.31 -            val session_entries = data.getOrElse(name, Map.empty)
    1.32 +            val session_entries = data_entries.getOrElse(name, Map.empty)
    1.33              val entries = session_entries.getOrElse(session, Nil)
    1.34 -            data += (name -> (session_entries + (session -> (entry :: entries))))
    1.35 +            data_entries += (name -> (session_entries + (session -> (entry :: entries))))
    1.36            }
    1.37          })
    1.38        }
    1.39      })
    1.40  
    1.41 -    for {
    1.42 -      (name, session_entries) <- data
    1.43 -      session_entries1 <-
    1.44 -        {
    1.45 -          val session_entries1 =
    1.46 -            for {
    1.47 -              (session, entries) <- session_entries
    1.48 -              if entries.filter(_.check(elapsed_threshold)).length >= 3
    1.49 -            } yield (session, entries)
    1.50 -          if (session_entries1.isEmpty) None
    1.51 -          else Some(session_entries1)
    1.52 -        }
    1.53 -    } yield (name, session_entries1)
    1.54 +    Data(date,
    1.55 +      for {
    1.56 +        (name, session_entries) <- data_entries
    1.57 +        session_entries1 <-
    1.58 +          {
    1.59 +            val session_entries1 =
    1.60 +              for {
    1.61 +                (session, entries) <- session_entries
    1.62 +                if entries.filter(_.check(elapsed_threshold)).length >= 3
    1.63 +              } yield (session, entries)
    1.64 +            if (session_entries1.isEmpty) None
    1.65 +            else Some(session_entries1)
    1.66 +          }
    1.67 +      } yield (name, session_entries1))
    1.68    }
    1.69  
    1.70  
    1.71    /* present data */
    1.72  
    1.73 -  private val html_header = """<!DOCTYPE HTML PUBLIC "-//IETF//DTD HTML//EN">
    1.74 -<html>
    1.75 -<head><title>Build status</title></head>
    1.76 -<body>
    1.77 -"""
    1.78 -  private val html_footer = """
    1.79 -</body>
    1.80 -</html>
    1.81 -"""
    1.82 -
    1.83    def present_data(data: Data,
    1.84      progress: Progress = No_Progress,
    1.85      target_dir: Path = default_target_dir,
    1.86      image_size: (Int, Int) = default_image_size,
    1.87      ml_timing: Option[Boolean] = None)
    1.88    {
    1.89 -    val data_entries = data.toList.sortBy(_._1)
    1.90 -    for ((name, session_entries) <- data_entries) {
    1.91 -      val dir = target_dir + Path.explode(name)
    1.92 +    val data_entries = data.sorted_entries
    1.93 +
    1.94 +    for ((data_name, session_entries) <- data_entries) {
    1.95 +      val dir = target_dir + Path.explode(data_name)
    1.96        progress.echo("output " + dir)
    1.97        Isabelle_System.mkdirs(dir)
    1.98  
    1.99 @@ -209,26 +207,37 @@
   1.100              val result =
   1.101                Isabelle_System.bash("\"$ISABELLE_GNUPLOT\" " + File.bash_path(gnuplot_file))
   1.102              if (result.rc != 0)
   1.103 -              result.error("Gnuplot failed for " + name + "/" + session).check
   1.104 +              result.error("Gnuplot failed for " + data_name + "/" + session).check
   1.105            }
   1.106          }
   1.107        }
   1.108  
   1.109 +      val sessions = session_entries.toList.sortBy(_._2.head.timing.elapsed.ms).reverse
   1.110 +      val heading = "Build status for " + data_name + " (" + data.date + ")"
   1.111 +
   1.112        File.write(dir + Path.basic("index.html"),
   1.113 -        html_header + "\n<h1>" + HTML.output(name) + "</h1>\n" +
   1.114 -        cat_lines(
   1.115 -          session_entries.toList.map(_._1).sorted.map(session =>
   1.116 -            """<br/><img src=""" + quote(HTML.output(session + ".png")) + """><br/>""")) +
   1.117 -        "\n" + html_footer)
   1.118 +        HTML.output_document(
   1.119 +          List(HTML.title(heading)),
   1.120 +          HTML.chapter(heading) ::
   1.121 +          HTML.itemize(
   1.122 +            sessions.map({ case (name, entries) =>
   1.123 +              HTML.link("#session_" + name, HTML.text(name)) ::
   1.124 +              HTML.text(" (" + entries.head.timing.message_resources + ")") })) ::
   1.125 +          sessions.flatMap({ case (name, entries) =>
   1.126 +            List(
   1.127 +              HTML.section(name + " (" + entries.head.timing.message_resources + ")") +
   1.128 +                HTML.id("session_" + name),
   1.129 +              HTML.par(List(HTML.image(name + ".png")))) })))
   1.130      }
   1.131  
   1.132 +    val heading = "Build status (" + data.date + ")"
   1.133 +
   1.134      File.write(target_dir + Path.basic("index.html"),
   1.135 -      html_header + "\n<ul>\n" +
   1.136 -      cat_lines(
   1.137 -        data_entries.map(_._1).map(name =>
   1.138 -          """<li> <a href=""" + quote(HTML.output(name + "/index.html")) + """>""" +
   1.139 -            HTML.output(name) + """</a> </li>""")) +
   1.140 -      "\n</ul>\n" + html_footer)
   1.141 +      HTML.output_document(
   1.142 +        List(HTML.title(heading)),
   1.143 +        List(HTML.chapter(heading),
   1.144 +          HTML.itemize(data_entries.map({ case (name, _) =>
   1.145 +            List(HTML.link(name + "/index.html", HTML.text(name))) })))))
   1.146    }
   1.147  
   1.148