# HG changeset patch
# User wenzelm
# Date 1377763319 -7200
# Node ID 0dfd78ff76961c9f27898e45f26972af0ebd949d
# Parent  0460d6962cedf3720072feb9e41003091681572a
more abstract Completion_Popup.Text_Area;
more uniform font size;

diff -r 0460d6962ced -r 0dfd78ff7696 src/Tools/jEdit/src/completion_popup.scala
--- a/src/Tools/jEdit/src/completion_popup.scala	Thu Aug 29 09:16:03 2013 +0200
+++ b/src/Tools/jEdit/src/completion_popup.scala	Thu Aug 29 10:01:59 2013 +0200
@@ -28,35 +28,33 @@
   { override def toString: String = description }
 
 
-  /* maintain single instance */
-
-  def dismissed(layered: JLayeredPane): Boolean =
-  {
-    Swing_Thread.require()
-
-    layered.getClientProperty(Completion_Popup) match {
-      case old_completion: Completion_Popup =>
-        old_completion.hide_popup()
-        true
-      case _ =>
-        false
-    }
-  }
-
-  private def register(layered: JLayeredPane, completion: Completion_Popup)
-  {
-    Swing_Thread.require()
-
-    dismissed(layered)
-    layered.putClientProperty(Completion_Popup, completion)
-  }
-
-
-  /* jEdit text area operations */
+  /* setup for jEdit text area */
 
   object Text_Area
   {
-    private def insert(text_area: JEditTextArea, item: Item)
+    def apply(text_area: JEditTextArea, get_syntax: => Option[Outer_Syntax]): Text_Area =
+      new Text_Area(text_area, get_syntax)
+  }
+
+  class Text_Area private(text_area: JEditTextArea, get_syntax: => Option[Outer_Syntax])
+  {
+    private var completion_popup: Option[Completion_Popup] = None
+
+    def dismissed(): Boolean =
+    {
+      Swing_Thread.require()
+
+      completion_popup match {
+        case Some(completion) =>
+          completion.hide_popup()
+          completion_popup = None
+          true
+        case None =>
+          false
+      }
+    }
+
+    private def insert(item: Item)
     {
       Swing_Thread.require()
 
@@ -75,7 +73,7 @@
       }
     }
 
-    def input(text_area: JEditTextArea, get_syntax: => Option[Outer_Syntax], evt: KeyEvent)
+    def input(evt: KeyEvent)
     {
       Swing_Thread.require()
 
@@ -85,7 +83,7 @@
       val painter = text_area.getPainter
 
       if (buffer.isEditable && !evt.isConsumed) {
-        dismissed(layered)
+        dismissed()
 
         get_syntax match {
           case Some(syntax) =>
@@ -109,10 +107,7 @@
             }
             result match {
               case Some((original, items)) =>
-                val popup_font =
-                  painter.getFont.deriveFont(
-                    (painter.getFont.getSize2D * PIDE.options.real("jedit_popup_font_scale")).toFloat
-                      max 10.0f)
+                val font = painter.getFont.deriveFont(Rendering.font_size("jedit_popup_font_scale"))
 
                 val loc1 = text_area.offsetToXY(caret - original.length)
                 if (loc1 != null) {
@@ -120,15 +115,15 @@
                     SwingUtilities.convertPoint(painter,
                       loc1.x, loc1.y + painter.getFontMetrics.getHeight, layered)
                   val completion =
-                    new Completion_Popup(layered, loc2, popup_font, items) {
-                      override def complete(item: Item) { insert(text_area, item) }
+                    new Completion_Popup(layered, loc2, font, items) {
+                      override def complete(item: Item) { insert(item) }
                       override def propagate(e: KeyEvent) {
                         JEdit_Lib.propagate_key(view, e)
-                        input(text_area, get_syntax, e)
+                        input(e)
                       }
                       override def refocus() { text_area.requestFocus }
                     }
-                  register(layered, completion)
+                  completion_popup = Some(completion)
                   completion.show_popup()
                 }
               case None =>
@@ -144,7 +139,7 @@
 class Completion_Popup private(
   layered: JLayeredPane,
   location: Point,
-  popup_font: Font,
+  font: Font,
   items: List[Completion_Popup.Item]) extends JPanel(new BorderLayout)
 {
   completion =>
@@ -163,9 +158,7 @@
   /* list view */
 
   private val list_view = new ListView(items)
-  {
-    font = popup_font
-  }
+  list_view.font = font
   list_view.selection.intervalMode = ListView.IntervalMode.Single
   list_view.peer.setFocusTraversalKeysEnabled(false)
   list_view.peer.setVisibleRowCount(items.length min 8)
diff -r 0460d6962ced -r 0dfd78ff7696 src/Tools/jEdit/src/document_view.scala
--- a/src/Tools/jEdit/src/document_view.scala	Thu Aug 29 09:16:03 2013 +0200
+++ b/src/Tools/jEdit/src/document_view.scala	Thu Aug 29 10:01:59 2013 +0200
@@ -149,6 +149,11 @@
 
   /* key listener */
 
+  private val completion_popup =
+    Completion_Popup.Text_Area(text_area, PIDE.get_recent_syntax)
+
+  def dismissed_popups(): Boolean = completion_popup.dismissed()
+
   private val key_listener =
     JEdit_Lib.key_listener(
       key_pressed = (evt: KeyEvent) =>
@@ -156,7 +161,7 @@
           if (evt.getKeyCode == KeyEvent.VK_ESCAPE && PIDE.dismissed_popups(text_area.getView))
             evt.consume
         },
-      key_typed = Completion_Popup.Text_Area.input(text_area, PIDE.get_recent_syntax, _)
+      key_typed = completion_popup.input _
     )
 
 
diff -r 0460d6962ced -r 0dfd78ff7696 src/Tools/jEdit/src/isabelle.scala
--- a/src/Tools/jEdit/src/isabelle.scala	Thu Aug 29 09:16:03 2013 +0200
+++ b/src/Tools/jEdit/src/isabelle.scala	Thu Aug 29 10:01:59 2013 +0200
@@ -98,19 +98,14 @@
 
   /* font size */
 
-  def change_font_size(view: View, change: Int => Int)
-  {
-    val size = change(jEdit.getIntegerProperty("view.fontsize", 16)) max 5 min 250
-    jEdit.setIntegerProperty("view.fontsize", size)
-    jEdit.propertiesChanged()
-    jEdit.saveSettings()
-    view.getStatus.setMessageAndClear("Text font size: " + size)
-  }
+  def reset_font_size(view: View): Unit =
+    Rendering.font_size_change(view, _ => PIDE.options.int("jedit_reset_font_size"))
 
-  def reset_font_size(view: View): Unit =
-    change_font_size(view, _ => PIDE.options.int("jedit_reset_font_size"))
-  def increase_font_size(view: View): Unit = change_font_size(view, i => i + ((i / 10) max 1))
-  def decrease_font_size(view: View): Unit = change_font_size(view, i => i - ((i / 10) max 1))
+  def increase_font_size(view: View): Unit =
+    Rendering.font_size_change(view, i => i + ((i / 10) max 1))
+
+  def decrease_font_size(view: View): Unit =
+    Rendering.font_size_change(view, i => i - ((i / 10) max 1))
 
 
   /* structured insert */
diff -r 0460d6962ced -r 0dfd78ff7696 src/Tools/jEdit/src/plugin.scala
--- a/src/Tools/jEdit/src/plugin.scala	Thu Aug 29 09:16:03 2013 +0200
+++ b/src/Tools/jEdit/src/plugin.scala	Thu Aug 29 10:01:59 2013 +0200
@@ -57,9 +57,16 @@
 
   def dismissed_popups(view: View): Boolean =
   {
-    val b1 = Completion_Popup.dismissed(view.getLayeredPane)
-    val b2 = Pretty_Tooltip.dismissed_all()
-    b1 || b2
+    var dismissed = false
+
+    for {
+      text_area <- JEdit_Lib.jedit_text_areas(view)
+      doc_view <- document_view(text_area)
+    } { if (doc_view.dismissed_popups()) dismissed = true }
+
+    if (Pretty_Tooltip.dismissed_all()) dismissed = true
+
+    dismissed
   }
 
 
diff -r 0460d6962ced -r 0dfd78ff7696 src/Tools/jEdit/src/rendering.scala
--- a/src/Tools/jEdit/src/rendering.scala	Thu Aug 29 09:16:03 2013 +0200
+++ b/src/Tools/jEdit/src/rendering.scala	Thu Aug 29 10:01:59 2013 +0200
@@ -14,7 +14,7 @@
 import javax.swing.Icon
 
 import org.gjt.sp.jedit.syntax.{Token => JEditToken}
-import org.gjt.sp.jedit.jEdit
+import org.gjt.sp.jedit.{jEdit, View}
 
 import scala.collection.immutable.SortedMap
 
@@ -45,8 +45,21 @@
 
   def font_family(): String = jEdit.getProperty("view.font")
 
+  private def view_font_size(): Int = jEdit.getIntegerProperty("view.fontsize", 16)
+  private val font_size0 = 5
+  private val font_size1 = 250
+
   def font_size(scale: String): Float =
-    (jEdit.getIntegerProperty("view.fontsize", 16) * PIDE.options.real(scale)).toFloat
+    (view_font_size() * PIDE.options.real(scale)).toFloat max font_size0 min font_size1
+
+  def font_size_change(view: View, change: Int => Int)
+  {
+    val size = change(view_font_size()) max font_size0 min font_size1
+    jEdit.setIntegerProperty("view.fontsize", size)
+    jEdit.propertiesChanged()
+    jEdit.saveSettings()
+    view.getStatus.setMessageAndClear("Text font size: " + size)
+  }
 
 
   /* popup window bounds */