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