src/Tools/Graphview/tree_panel.scala
author wenzelm
Mon Mar 12 11:17:59 2018 +0100 (19 months ago)
changeset 67835 c8e4ee2b5482
parent 66206 2d2082db735a
permissions -rw-r--r--
tuned imports;
wenzelm@59392
     1
/*  Title:      Tools/Graphview/tree_panel.scala
wenzelm@59392
     2
    Author:     Makarius
wenzelm@59392
     3
wenzelm@59392
     4
Tree view on graph nodes.
wenzelm@59392
     5
*/
wenzelm@59392
     6
wenzelm@59392
     7
package isabelle.graphview
wenzelm@59392
     8
wenzelm@59392
     9
wenzelm@59392
    10
import isabelle._
wenzelm@59392
    11
wenzelm@59396
    12
import java.awt.{Dimension, Rectangle}
wenzelm@59396
    13
import java.awt.event.{KeyEvent, KeyAdapter, MouseEvent, MouseAdapter}
wenzelm@59392
    14
import javax.swing.JTree
wenzelm@59396
    15
import javax.swing.tree.{DefaultMutableTreeNode, TreeSelectionModel, TreePath}
wenzelm@59396
    16
import javax.swing.event.{TreeSelectionEvent, TreeSelectionListener, DocumentListener, DocumentEvent}
wenzelm@59392
    17
wenzelm@59392
    18
import scala.util.matching.Regex
wenzelm@59396
    19
import scala.swing.{Component, ScrollPane, BorderPanel, Label, TextField, Button, CheckBox, Action}
wenzelm@59392
    20
wenzelm@59392
    21
wenzelm@59459
    22
class Tree_Panel(val graphview: Graphview, graph_panel: Graph_Panel) extends BorderPanel
wenzelm@59392
    23
{
wenzelm@59396
    24
  /* main actions */
wenzelm@59396
    25
wenzelm@59396
    26
  private def selection_action()
wenzelm@59396
    27
  {
wenzelm@59396
    28
    if (tree != null) {
wenzelm@59459
    29
      graphview.current_node = None
wenzelm@59459
    30
      graphview.Selection.clear()
wenzelm@59396
    31
      val paths = tree.getSelectionPaths
wenzelm@59396
    32
      if (paths != null) {
wenzelm@59396
    33
        for (path <- paths if path != null) {
wenzelm@59396
    34
          path.getLastPathComponent match {
wenzelm@59396
    35
            case tree_node: DefaultMutableTreeNode =>
wenzelm@59396
    36
              tree_node.getUserObject match {
wenzelm@59459
    37
                case node: Graph_Display.Node => graphview.Selection.add(node)
wenzelm@59396
    38
                case _ =>
wenzelm@59396
    39
              }
wenzelm@59396
    40
            case _ =>
wenzelm@59396
    41
          }
wenzelm@59396
    42
        }
wenzelm@59396
    43
      }
wenzelm@59397
    44
      graph_panel.repaint()
wenzelm@59396
    45
    }
wenzelm@59396
    46
  }
wenzelm@59396
    47
wenzelm@59396
    48
  private def point_action(path: TreePath)
wenzelm@59396
    49
  {
wenzelm@59396
    50
    if (tree_pane != null && path != null) {
wenzelm@59396
    51
      val action_node =
wenzelm@59396
    52
        path.getLastPathComponent match {
wenzelm@59396
    53
          case tree_node: DefaultMutableTreeNode =>
wenzelm@59396
    54
            tree_node.getUserObject match {
wenzelm@59396
    55
              case node: Graph_Display.Node => Some(node)
wenzelm@59396
    56
              case _ => None
wenzelm@59396
    57
            }
wenzelm@59396
    58
          case _ => None
wenzelm@59396
    59
        }
wenzelm@59397
    60
      action_node.foreach(graph_panel.scroll_to_node(_))
wenzelm@59459
    61
      graphview.current_node = action_node
wenzelm@59397
    62
      graph_panel.repaint()
wenzelm@59396
    63
    }
wenzelm@59396
    64
  }
wenzelm@59396
    65
wenzelm@59396
    66
wenzelm@59392
    67
  /* tree */
wenzelm@59392
    68
wenzelm@59392
    69
  private var nodes = List.empty[Graph_Display.Node]
wenzelm@59392
    70
  private val root = new DefaultMutableTreeNode("Nodes")
wenzelm@59392
    71
wenzelm@59396
    72
  val tree = new JTree(root)
wenzelm@60292
    73
  tree.setRowHeight(0)
wenzelm@59396
    74
wenzelm@59396
    75
  tree.addKeyListener(new KeyAdapter {
wenzelm@59396
    76
    override def keyPressed(e: KeyEvent): Unit =
wenzelm@59396
    77
      if (e.getKeyCode == KeyEvent.VK_ENTER) {
wenzelm@59396
    78
        e.consume
wenzelm@59396
    79
        selection_action()
wenzelm@59396
    80
      }
wenzelm@59396
    81
  })
wenzelm@59392
    82
  tree.addMouseListener(new MouseAdapter {
wenzelm@59396
    83
    override def mousePressed(e: MouseEvent): Unit =
wenzelm@59396
    84
      if (e.getClickCount == 2)
wenzelm@59396
    85
        point_action(tree.getPathForLocation(e.getX, e.getY))
wenzelm@59392
    86
  })
wenzelm@59392
    87
wenzelm@59392
    88
  private val tree_pane = new ScrollPane(Component.wrap(tree))
wenzelm@59392
    89
  tree_pane.horizontalScrollBarPolicy = ScrollPane.BarPolicy.Always
wenzelm@59392
    90
  tree_pane.verticalScrollBarPolicy = ScrollPane.BarPolicy.Always
wenzelm@60849
    91
  tree_pane.minimumSize = new Dimension(200, 100)
wenzelm@59392
    92
  tree_pane.peer.getVerticalScrollBar.setUnitIncrement(10)
wenzelm@59392
    93
wenzelm@59392
    94
wenzelm@59392
    95
  /* controls */
wenzelm@59392
    96
wenzelm@59392
    97
  private var selection_pattern: Option[Regex] = None
wenzelm@59392
    98
wenzelm@59392
    99
  private def selection_filter(node: Graph_Display.Node): Boolean =
wenzelm@59392
   100
    selection_pattern match {
wenzelm@59402
   101
      case None => false
wenzelm@59392
   102
      case Some(re) => re.pattern.matcher(node.toString).find
wenzelm@59392
   103
    }
wenzelm@59392
   104
wenzelm@59392
   105
  private val selection_label = new Label("Selection:") {
wenzelm@59392
   106
    tooltip = "Selection of nodes via regular expression"
wenzelm@59392
   107
  }
wenzelm@59392
   108
wenzelm@59392
   109
  private val selection_field = new TextField(10) {
wenzelm@59392
   110
    tooltip = selection_label.tooltip
wenzelm@59392
   111
  }
wenzelm@59392
   112
  private val selection_field_foreground = selection_field.foreground
wenzelm@59392
   113
wenzelm@59392
   114
  private val selection_delay =
wenzelm@59459
   115
    GUI_Thread.delay_last(graphview.options.seconds("editor_input_delay")) {
wenzelm@59392
   116
      val (pattern, ok) =
wenzelm@59392
   117
        selection_field.text match {
wenzelm@59392
   118
          case null | "" => (None, true)
wenzelm@59392
   119
          case s =>
wenzelm@59392
   120
            val pattern = Library.make_regex(s)
wenzelm@59392
   121
            (pattern, pattern.isDefined)
wenzelm@59392
   122
        }
wenzelm@59392
   123
      if (selection_pattern != pattern) {
wenzelm@59392
   124
        selection_pattern = pattern
wenzelm@59402
   125
        tree.setSelectionRows(
wenzelm@59402
   126
          (for { (node, i) <- nodes.iterator.zipWithIndex if selection_filter(node) }
wenzelm@59402
   127
            yield i + 1).toArray)
wenzelm@59402
   128
        tree.repaint()
wenzelm@59392
   129
      }
wenzelm@59392
   130
      selection_field.foreground =
wenzelm@59459
   131
        if (ok) selection_field_foreground else graphview.error_color
wenzelm@59392
   132
    }
wenzelm@59392
   133
wenzelm@59392
   134
  selection_field.peer.getDocument.addDocumentListener(new DocumentListener {
wenzelm@59392
   135
    def changedUpdate(e: DocumentEvent) { selection_delay.invoke() }
wenzelm@59392
   136
    def insertUpdate(e: DocumentEvent) { selection_delay.invoke() }
wenzelm@59392
   137
    def removeUpdate(e: DocumentEvent) { selection_delay.invoke() }
wenzelm@59392
   138
  })
wenzelm@59392
   139
wenzelm@59392
   140
  private val selection_apply = new Button {
wenzelm@59406
   141
    action = Action("<html><b>Apply</b></html>") { selection_action () }
wenzelm@59392
   142
    tooltip = "Apply tree selection to graph"
wenzelm@59392
   143
  }
wenzelm@59392
   144
wenzelm@59409
   145
  private val controls =
wenzelm@66206
   146
    Wrap_Panel(List(selection_label, selection_field, selection_apply))
wenzelm@59392
   147
wenzelm@59392
   148
wenzelm@59392
   149
  /* main layout */
wenzelm@59392
   150
wenzelm@59392
   151
  def refresh()
wenzelm@59392
   152
  {
wenzelm@59459
   153
    val new_nodes = graphview.visible_graph.topological_order
wenzelm@59392
   154
    if (new_nodes != nodes) {
wenzelm@60846
   155
      tree.clearSelection
wenzelm@60846
   156
wenzelm@59392
   157
      nodes = new_nodes
wenzelm@59392
   158
wenzelm@59392
   159
      root.removeAllChildren
wenzelm@59392
   160
      for (node <- nodes) root.add(new DefaultMutableTreeNode(node))
wenzelm@59392
   161
wenzelm@60905
   162
      tree.expandRow(0)
wenzelm@59392
   163
      tree.revalidate()
wenzelm@59392
   164
    }
wenzelm@59392
   165
    revalidate()
wenzelm@59392
   166
    repaint()
wenzelm@59392
   167
  }
wenzelm@59392
   168
wenzelm@59392
   169
  layout(tree_pane) = BorderPanel.Position.Center
wenzelm@59392
   170
  layout(controls) = BorderPanel.Position.North
wenzelm@59392
   171
  refresh()
wenzelm@59392
   172
}