# HG changeset patch
# User wenzelm
# Date 1421681464 -3600
# Node ID 283aa6225d987a2b285b34cd1ec6957cf1d13e6b
# Parent 4a0b34ef05630b7db250cfc16ac4cab57cc252e5
proper tooltips -- override action toolTip which is empty here;
diff -r 4a0b34ef0563 -r 283aa6225d98 src/Tools/Graphview/main_panel.scala
--- a/src/Tools/Graphview/main_panel.scala Mon Jan 19 11:37:53 2015 +0100
+++ b/src/Tools/Graphview/main_panel.scala Mon Jan 19 16:31:04 2015 +0100
@@ -49,41 +49,47 @@
val controls =
new Wrap_Panel(Wrap_Panel.Alignment.Right)(
new CheckBox() {
- tooltip = "Show full node content"
selected = visualizer.show_content
action = Action("Show content") {
visualizer.show_content = selected
update_layout()
}
+ tooltip = "Show full node content within graph layout"
},
new CheckBox() {
- tooltip = "Draw edges with explicit arrow heads"
selected = visualizer.show_arrow_heads
action = Action("Show arrow heads") {
visualizer.show_arrow_heads = selected
graph_panel.repaint()
}
+ tooltip = "Draw edges with explicit arrow heads"
},
new CheckBox() {
- tooltip = "Show dummy nodes -- easier mouse dragging"
selected = visualizer.show_dummies
action = Action("Show dummies") {
visualizer.show_dummies = selected
graph_panel.repaint()
}
+ tooltip = "Draw dummy nodes within graph layout, for easier mouse dragging"
},
new Button {
action = Action("Save image") {
- tooltip = "Save current image as PNG or PDF"
chooser.showSaveDialog(this) match {
case FileChooser.Result.Approve => export(chooser.selectedFile)
case _ =>
}
}
+ tooltip = "Save current graph layout as PNG or PDF"
},
graph_panel.zoom,
- new Button { action = Action("Fit to window") { graph_panel.fit_to_window() } },
- new Button { action = Action("Update layout") { update_layout() } })
+ new Button {
+ action = Action("Fit to window") { graph_panel.fit_to_window() }
+ tooltip = "Zoom to fit window width and height"
+ },
+ new Button {
+ action = Action("Update layout") { update_layout() }
+ tooltip = "Regenerate graph layout according to built-in algorithm"
+ })
/* FIXME
new Button { action = Action("Colorations") { color_dialog.open } },
new Button { action = Action("Filters") { mutator_dialog.open } }
diff -r 4a0b34ef0563 -r 283aa6225d98 src/Tools/Graphview/tree_panel.scala
--- a/src/Tools/Graphview/tree_panel.scala Mon Jan 19 11:37:53 2015 +0100
+++ b/src/Tools/Graphview/tree_panel.scala Mon Jan 19 16:31:04 2015 +0100
@@ -137,8 +137,8 @@
})
private val selection_apply = new Button {
+ action = Action("Apply") { selection_action () }
tooltip = "Apply tree selection to graph"
- action = Action("Apply") { selection_action () }
}
private val controls = new Wrap_Panel(Wrap_Panel.Alignment.Right)(