--- a/src/Tools/jEdit/src/isabelle_rendering.scala Sun Oct 07 16:05:31 2012 +0200
+++ b/src/Tools/jEdit/src/isabelle_rendering.scala Sun Oct 07 16:15:31 2012 +0200
@@ -56,8 +56,8 @@
legacy_pri -> load_icon("16x16/status/dialog-warning.png"),
error_pri -> load_icon("16x16/status/dialog-error.png"))
+ val tooltip_close_icon = load_icon("16x16/actions/document-close.png")
val tooltip_detach_icon = load_icon("16x16/actions/window-new.png")
- val tooltip_close_icon = load_icon("16x16/actions/document-close.png")
/* token markup -- text styles */
--- a/src/Tools/jEdit/src/pretty_tooltip.scala Sun Oct 07 16:05:31 2012 +0200
+++ b/src/Tools/jEdit/src/pretty_tooltip.scala Sun Oct 07 16:15:31 2012 +0200
@@ -76,6 +76,13 @@
/* controls */
+ private val close = new Label {
+ icon = Isabelle_Rendering.tooltip_close_icon
+ tooltip = "Close tooltip window"
+ listenTo(mouse.clicks)
+ reactions += { case _: MouseClicked => window.dispose() }
+ }
+
private val detach = new Label {
icon = Isabelle_Rendering.tooltip_detach_icon
tooltip = "Detach tooltip window"
@@ -85,14 +92,7 @@
}
}
- private val close = new Label {
- icon = Isabelle_Rendering.tooltip_close_icon
- tooltip = "Close tooltip window"
- listenTo(mouse.clicks)
- reactions += { case _: MouseClicked => window.dispose() }
- }
-
- private val controls = new FlowPanel(FlowPanel.Alignment.Right)(detach, close)
+ private val controls = new FlowPanel(FlowPanel.Alignment.Left)(close, detach)
window.add(controls.peer, BorderLayout.NORTH)