# HG changeset patch
# User wenzelm
# Date 1377610551 -7200
# Node ID 6ce8328d79123e6cc24c2bfa18aa91342bfa79f0
# Parent  f6c6688961db2960ba06c640103334ef78da55ed
explicit "hidden" operation with focus management;
explicit popup_font;
just one option jedit_popup_font_scale for tooltip and completion;

diff -r f6c6688961db -r 6ce8328d7912 src/Tools/jEdit/etc/options
--- a/src/Tools/jEdit/etc/options	Tue Aug 27 14:56:11 2013 +0200
+++ b/src/Tools/jEdit/etc/options	Tue Aug 27 15:35:51 2013 +0200
@@ -9,12 +9,12 @@
 public option jedit_font_scale : real = 1.0
   -- "scale factor of add-on panels wrt. main text area"
 
+public option jedit_popup_font_scale : real = 0.85
+  -- "scale factor of popups wrt. main text area"
+
 public option jedit_tooltip_delay : real = 0.75
   -- "open/close delay for document tooltips"
 
-public option jedit_tooltip_font_scale : real = 0.85
-  -- "scale factor of tooltips wrt. main text area"
-
 public option jedit_tooltip_margin : int = 60
   -- "margin for tooltip pretty-printing"
 
diff -r f6c6688961db -r 6ce8328d7912 src/Tools/jEdit/src/completion_popup.scala
--- a/src/Tools/jEdit/src/completion_popup.scala	Tue Aug 27 14:56:11 2013 +0200
+++ b/src/Tools/jEdit/src/completion_popup.scala	Tue Aug 27 15:35:51 2013 +0200
@@ -9,7 +9,7 @@
 
 import isabelle._
 
-import java.awt.{Point, BorderLayout, Dimension}
+import java.awt.{Font, Point, BorderLayout, Dimension}
 import java.awt.event.{KeyEvent, MouseEvent, MouseAdapter, FocusAdapter, FocusEvent}
 import javax.swing.{JPanel, JComponent, PopupFactory, SwingUtilities}
 
@@ -27,16 +27,19 @@
 
   def apply(
     opt_view: Option[View],
-    parent: JComponent,
+    root: JComponent,
+    popup_font: Font,
     screen_point: Point,
     items: List[Item],
-    complete: Item => Unit): Completion_Popup =
+    complete: Item => Unit,
+    hidden: () => Unit): Completion_Popup =
   {
     Swing_Thread.require()
 
     require(!items.isEmpty)
 
-    val completion = new Completion_Popup(opt_view, parent, screen_point, items, complete)
+    val completion =
+      new Completion_Popup(opt_view, root, popup_font, screen_point, items, complete, hidden)
     completion.show_popup()
     completion
   }
@@ -47,20 +50,30 @@
 
     val buffer = text_area.getBuffer
     if (buffer.isEditable) {
+      val view = text_area.getView
       val painter = text_area.getPainter
       val caret = text_area.getCaretPosition
 
       // FIXME
       def complete(item: Item) { }
+
+      def hidden() { text_area.requestFocus }
+
+      // FIXME
       val token_length = 0
       val items: List[Item] = Nil
 
+      val popup_font =
+        painter.getFont.deriveFont(
+          (painter.getFont.getSize2D * PIDE.options.real("jedit_popup_font_scale")).toFloat
+            max 10.0f)
+
       if (!items.isEmpty) {
         val location = text_area.offsetToXY(caret - token_length)
         if (location != null) {
           location.y = location.y + painter.getFontMetrics.getHeight
           SwingUtilities.convertPointToScreen(location, painter)
-          apply(Some(text_area.getView), painter, location, items, complete _)
+          apply(Some(view), view.getRootPane, popup_font, location, items, complete _, hidden _)
         }
       }
     }
@@ -70,10 +83,12 @@
 
 class Completion_Popup private(
   opt_view: Option[View],
-  parent: JComponent,
+  root: JComponent,
+  popup_font: Font,
   screen_point: Point,
   items: List[Completion_Popup.Item],
-  complete: Completion_Popup.Item => Unit) extends JPanel(new BorderLayout)
+  complete: Completion_Popup.Item => Unit,
+  hidden: () => Unit) extends JPanel(new BorderLayout)
 {
   completion =>
 
@@ -84,7 +99,7 @@
 
   private val list_view = new ListView(items)
   {
-    font = parent.getFont
+    font = popup_font
   }
   list_view.selection.intervalMode = ListView.IntervalMode.Single
   list_view.peer.setFocusTraversalKeysEnabled(false)
@@ -198,7 +213,7 @@
 
     val x = screen_point.x min (screen_bounds.x + screen_bounds.width - w)
     val y = screen_point.y min (screen_bounds.y + screen_bounds.height - h)
-    PopupFactory.getSharedInstance.getPopup(parent, completion, x, y)
+    PopupFactory.getSharedInstance.getPopup(root, completion, x, y)
   }
 
   def show_popup()
@@ -211,18 +226,12 @@
   def hide_popup()
   {
     opt_view match {
-      case Some(view) =>
-        if (view.getKeyEventInterceptor == key_listener)
-          view.setKeyEventInterceptor(null)
-        popup.hide
-        view.getTextArea match {
-          case null =>
-          case text_area => text_area.requestFocus
-        }
-      case None =>
-        popup.hide
-        parent.requestFocus
+      case Some(view) if (view.getKeyEventInterceptor == key_listener) =>
+        view.setKeyEventInterceptor(null)
+      case _ =>
     }
+    popup.hide
+    hidden()
   }
 }
 
diff -r f6c6688961db -r 6ce8328d7912 src/Tools/jEdit/src/pretty_tooltip.scala
--- a/src/Tools/jEdit/src/pretty_tooltip.scala	Tue Aug 27 14:56:11 2013 +0200
+++ b/src/Tools/jEdit/src/pretty_tooltip.scala	Tue Aug 27 15:35:51 2013 +0200
@@ -195,7 +195,7 @@
   })
 
   pretty_text_area.resize(Rendering.font_family(),
-    Rendering.font_size("jedit_tooltip_font_scale").round)
+    Rendering.font_size("jedit_popup_font_scale").round)
 
 
   /* main content */