make buttons closer to original mouse position;
authorwenzelm
Sun, 07 Oct 2012 16:15:31 +0200
changeset 49727 2fe56b600698
parent 49726 2074197dc274
child 49728 74f36dab2b62
make buttons closer to original mouse position;
src/Tools/jEdit/src/isabelle_rendering.scala
src/Tools/jEdit/src/pretty_tooltip.scala
--- 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)