explicit indication of consolidated nodes;
authorwenzelm
Mon Aug 14 11:30:07 2017 +0200 (2017-08-14)
changeset 6641072a7e29104f1
parent 66409 f749d39c016b
child 66411 72de7d59e2f7
explicit indication of consolidated nodes;
src/Pure/PIDE/protocol.scala
src/Tools/jEdit/src/theories_dockable.scala
     1.1 --- a/src/Pure/PIDE/protocol.scala	Sun Aug 13 23:45:45 2017 +0100
     1.2 +++ b/src/Pure/PIDE/protocol.scala	Mon Aug 14 11:30:07 2017 +0200
     1.3 @@ -126,13 +126,16 @@
     1.4    /* node status */
     1.5  
     1.6    sealed case class Node_Status(
     1.7 -    unprocessed: Int, running: Int, warned: Int, failed: Int, finished: Int)
     1.8 +    unprocessed: Int, running: Int, warned: Int, failed: Int, finished: Int, consolidated: Boolean)
     1.9    {
    1.10      def total: Int = unprocessed + running + warned + failed + finished
    1.11    }
    1.12  
    1.13    def node_status(
    1.14 -    state: Document.State, version: Document.Version, node: Document.Node): Node_Status =
    1.15 +    state: Document.State,
    1.16 +    version: Document.Version,
    1.17 +    name: Document.Node.Name,
    1.18 +    node: Document.Node): Node_Status =
    1.19    {
    1.20      var unprocessed = 0
    1.21      var running = 0
    1.22 @@ -149,7 +152,9 @@
    1.23        else if (status.is_finished) finished += 1
    1.24        else unprocessed += 1
    1.25      }
    1.26 -    Node_Status(unprocessed, running, warned, failed, finished)
    1.27 +    val consolidated = state.node_consolidated(version, name)
    1.28 +
    1.29 +    Node_Status(unprocessed, running, warned, failed, finished, consolidated)
    1.30    }
    1.31  
    1.32  
     2.1 --- a/src/Tools/jEdit/src/theories_dockable.scala	Sun Aug 13 23:45:45 2017 +0100
     2.2 +++ b/src/Tools/jEdit/src/theories_dockable.scala	Mon Aug 14 11:30:07 2017 +0200
     2.3 @@ -95,6 +95,12 @@
     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 +    nodes_status.get(name) match {
     2.9 +      case None => false
    2.10 +      case Some(st) => st.consolidated
    2.11 +    }
    2.12 +
    2.13    private def in(geometry: Option[(Point, Dimension)], loc0: Point, p: Point): Boolean =
    2.14      geometry match {
    2.15        case Some((loc, size)) =>
    2.16 @@ -132,10 +138,6 @@
    2.17      val label = new Label {
    2.18        background = view.getTextArea.getPainter.getBackground
    2.19        foreground = view.getTextArea.getPainter.getForeground
    2.20 -      border =
    2.21 -        BorderFactory.createCompoundBorder(
    2.22 -          BorderFactory.createLineBorder(foreground, 1),
    2.23 -          BorderFactory.createEmptyBorder(1, 1, 1, 1))
    2.24        opaque = false
    2.25        xAlignment = Alignment.Leading
    2.26  
    2.27 @@ -174,6 +176,15 @@
    2.28        }
    2.29      }
    2.30  
    2.31 +    def label_border(name: Document.Node.Name)
    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.createEmptyBorder(3, 3, 3, 3))
    2.38 +    }
    2.39 +
    2.40      layout(checkbox) = BorderPanel.Position.West
    2.41      layout(label) = BorderPanel.Position.Center
    2.42    }
    2.43 @@ -186,6 +197,7 @@
    2.44        val component = Node_Renderer_Component
    2.45        component.node_name = name
    2.46        component.checkbox.selected = nodes_required.contains(name)
    2.47 +      component.label_border(name)
    2.48        component.label.text = name.theory_base_name
    2.49        component
    2.50      }
    2.51 @@ -208,7 +220,11 @@
    2.52        (nodes_status /: iterator)({ case (status, (name, node)) =>
    2.53            if (!name.is_theory || PIDE.resources.session_base.loaded_theory(name) || node.is_empty)
    2.54              status
    2.55 -          else status + (name -> Protocol.node_status(snapshot.state, snapshot.version, node)) })
    2.56 +          else {
    2.57 +            val st = Protocol.node_status(snapshot.state, snapshot.version, name, node)
    2.58 +            status + (name -> st)
    2.59 +          }
    2.60 +      })
    2.61  
    2.62      val nodes_status2 =
    2.63        nodes_status1 -- nodes_status1.keysIterator.filter(nodes.is_hidden(_))