src/Pure/Admin/build_status.scala
changeset 65940 9c7241798c3b
parent 65939 9fb044904a4d
child 65941 316c30b60ebc
     1.1 --- a/src/Pure/Admin/build_status.scala	Fri May 26 23:21:50 2017 +0200
     1.2 +++ b/src/Pure/Admin/build_status.scala	Fri May 26 23:33:42 2017 +0200
     1.3 @@ -100,10 +100,21 @@
     1.4      maximum_heap: Long,
     1.5      average_heap: Long,
     1.6      stored_heap: Long,
     1.7 -    status: Build_Log.Session_Status.Value)
     1.8 +    status: Build_Log.Session_Status.Value,
     1.9 +    errors: List[String])
    1.10    {
    1.11      def finished: Boolean = status == Build_Log.Session_Status.finished
    1.12      def failed: Boolean = status == Build_Log.Session_Status.failed
    1.13 +
    1.14 +    def present_errors(name: String): XML.Body =
    1.15 +      if (errors.isEmpty) HTML.text(name + " (" + isabelle_version + ")")
    1.16 +      else {
    1.17 +        val tooltip_errors =
    1.18 +          errors.map(msg => HTML.pre(HTML.text(Symbol.decode(msg))) + HTML.error_message_class)
    1.19 +        val tooltip = List(HTML.div(tooltip_errors) + HTML.tooltip_class)
    1.20 +        HTML.span(HTML.text(name) ::: tooltip) + HTML.error_class ::
    1.21 +        HTML.text(" (" + isabelle_version + ")")
    1.22 +      }
    1.23    }
    1.24  
    1.25    sealed case class Image(name: String, width: Int, height: Int)
    1.26 @@ -149,7 +160,8 @@
    1.27              Build_Log.Data.ml_timing_cpu,
    1.28              Build_Log.Data.ml_timing_gc,
    1.29              Build_Log.Data.heap_size,
    1.30 -            Build_Log.Data.status) :::
    1.31 +            Build_Log.Data.status,
    1.32 +            Build_Log.Data.errors) :::
    1.33            (if (ml_statistics) List(Build_Log.Data.ml_statistics) else Nil)
    1.34  
    1.35          val Threads_Option = """threads\s*=\s*(\d+)""".r
    1.36 @@ -209,7 +221,8 @@
    1.37                  maximum_heap = ml_stats.maximum_heap_size,
    1.38                  average_heap = ml_stats.average_heap_size,
    1.39                  stored_heap = ML_Statistics.heap_scale(res.long(Build_Log.Data.heap_size)),
    1.40 -                status = Build_Log.Session_Status.withName(res.string(Build_Log.Data.status)))
    1.41 +                status = Build_Log.Session_Status.withName(res.string(Build_Log.Data.status)),
    1.42 +                errors = Build_Log.uncompress_errors(res.bytes(Build_Log.Data.errors)))
    1.43  
    1.44              val sessions = data_entries.getOrElse(data_name, Map.empty)
    1.45              val entries = sessions.get(session_name).map(_.entries) getOrElse Nil
    1.46 @@ -262,9 +275,9 @@
    1.47              (data_entry.failed_sessions match {
    1.48                case Nil => Nil
    1.49                case sessions =>
    1.50 -                HTML.break ::: List(HTML.span(HTML.text("Failed:")) + HTML.error_message_class) :::
    1.51 -                HTML.text(" " +
    1.52 -                  commas(sessions.map(s => s.name + " (" + s.head.isabelle_version + ")")))
    1.53 +                HTML.break :::
    1.54 +                List(HTML.span(HTML.text("Failed sessions:")) + HTML.error_message_class) :::
    1.55 +                List(HTML.itemize(sessions.map(s => s.head.present_errors(s.name))))
    1.56              })
    1.57            }))))))
    1.58