more explicit failure;
authorwenzelm
Mon Aug 14 13:53:49 2017 +0200 (2017-08-14)
changeset 6641172de7d59e2f7
parent 66410 72a7e29104f1
child 66412 a8556be5be0b
more explicit failure;
src/Pure/PIDE/protocol.scala
src/Tools/jEdit/src/theories_dockable.scala
     1.1 --- a/src/Pure/PIDE/protocol.scala	Mon Aug 14 11:30:07 2017 +0200
     1.2 +++ b/src/Pure/PIDE/protocol.scala	Mon Aug 14 13:53:49 2017 +0200
     1.3 @@ -129,6 +129,7 @@
     1.4      unprocessed: Int, running: Int, warned: Int, failed: Int, finished: Int, consolidated: Boolean)
     1.5    {
     1.6      def total: Int = unprocessed + running + warned + failed + finished
     1.7 +    def ok: Boolean = failed == 0
     1.8    }
     1.9  
    1.10    def node_status(
     2.1 --- a/src/Tools/jEdit/src/theories_dockable.scala	Mon Aug 14 11:30:07 2017 +0200
     2.2 +++ b/src/Tools/jEdit/src/theories_dockable.scala	Mon Aug 14 13:53:49 2017 +0200
     2.3 @@ -95,10 +95,16 @@
     2.4    private var nodes_status: Map[Document.Node.Name, Protocol.Node_Status] = Map.empty
     2.5    private var nodes_required: Set[Document.Node.Name] = Document_Model.required_nodes()
     2.6  
     2.7 -  private def nodes_status_consolidated(name: Document.Node.Name): Boolean =
     2.8 +  private object Overall_Node_Status extends Enumeration
     2.9 +  {
    2.10 +    val ok, failed, pending = Value
    2.11 +  }
    2.12 +
    2.13 +  private def overall_node_status(name: Document.Node.Name): Overall_Node_Status.Value =
    2.14      nodes_status.get(name) match {
    2.15 -      case None => false
    2.16 -      case Some(st) => st.consolidated
    2.17 +      case Some(st) if st.consolidated =>
    2.18 +        if (st.ok) Overall_Node_Status.ok else Overall_Node_Status.failed
    2.19 +      case _ => Overall_Node_Status.pending
    2.20      }
    2.21  
    2.22    private def in(geometry: Option[(Point, Dimension)], loc0: Point, p: Point): Boolean =
    2.23 @@ -178,10 +184,15 @@
    2.24  
    2.25      def label_border(name: Document.Node.Name)
    2.26      {
    2.27 +      val status = overall_node_status(name)
    2.28 +      val color =
    2.29 +        if (status == Overall_Node_Status.failed) PIDE.options.color_value("error_color")
    2.30 +        else label.foreground
    2.31 +      val thickness = if (status == Overall_Node_Status.pending) 1 else 3
    2.32 +
    2.33        label.border =
    2.34          BorderFactory.createCompoundBorder(
    2.35 -          BorderFactory.createLineBorder(
    2.36 -            label.foreground, if (nodes_status_consolidated(name)) 3 else 1),
    2.37 +          BorderFactory.createLineBorder(color, thickness),
    2.38            BorderFactory.createEmptyBorder(3, 3, 3, 3))
    2.39      }
    2.40