# HG changeset patch
# User wenzelm
# Date 1349619331 -7200
# Node ID 2fe56b60069842f1c06c715ae71718e11f673edd
# Parent  2074197dc274710792e731aebbfedd07df54f00b
make buttons closer to original mouse position;

diff -r 2074197dc274 -r 2fe56b600698 src/Tools/jEdit/src/isabelle_rendering.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 */
diff -r 2074197dc274 -r 2fe56b600698 src/Tools/jEdit/src/pretty_tooltip.scala
--- 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)