# HG changeset patch
# User wenzelm
# Date 1597314579 -7200
# Node ID 262d3c11a24da61a766a9dfc7868e7e3cb0baff2
# Parent  ae6544cf1c8c24395dbd75d0be8057bb6ef9b91b
clarified GUI;

diff -r ae6544cf1c8c -r 262d3c11a24d src/Tools/jEdit/src/ml_status.scala
--- a/src/Tools/jEdit/src/ml_status.scala	Wed Aug 12 20:09:37 2020 +0200
+++ b/src/Tools/jEdit/src/ml_status.scala	Thu Aug 13 12:29:39 2020 +0200
@@ -11,6 +11,7 @@
 
 import java.awt.{Color, Dimension, Graphics, Graphics2D, Insets, RenderingHints}
 import java.awt.font.FontRenderContext
+import java.awt.event.{MouseAdapter, MouseEvent}
 import javax.swing.{JComponent, JLabel}
 
 import org.gjt.sp.jedit.{View, jEdit}
@@ -21,7 +22,7 @@
 {
   private val template = "99999/99999MB"
 
-  private class GUI extends JComponent
+  private class GUI(view: View) extends JComponent
   {
     /* component state -- owned by GUI thread */
 
@@ -122,11 +123,23 @@
       super.removeNotify()
       PIDE.session.runtime_statistics -= main
     }
+
+
+    /* mouse listener */
+
+    addMouseListener(new MouseAdapter {
+      override def mouseClicked(evt: MouseEvent)
+      {
+        if (evt.getClickCount == 2) {
+          view.getInputHandler.invokeAction("isabelle-monitor-float")
+        }
+      }
+    })
   }
 
   class Widget_Factory extends StatusWidgetFactory
   {
     override def getWidget(view: View): Widget =
-      new Widget { override def getComponent: JComponent = new GUI }
+      new Widget { override def getComponent: JComponent = new GUI(view) }
   }
 }