dismiss popups more uniformly;

--- a/src/Tools/jEdit/src/completion_popup.scala	Wed Aug 28 09:12:50 2013 +0200
+++ b/src/Tools/jEdit/src/completion_popup.scala	Wed Aug 28 09:36:05 2013 +0200
@@ -28,16 +28,28 @@
   { override def toString: String = description }
 
 
-  /* register single instance within root */
+  /* single instance within root */
+
+  def dismissed_view(view: View): Boolean = dismissed(view.getRootPane)
+
+  private def dismissed(root: JComponent): Boolean =
+  {
+    Swing_Thread.require()
+
+    root.getClientProperty(Completion_Popup) match {
+      case old_completion: Completion_Popup =>
+        old_completion.hide_popup
+        true
+      case _ =>
+        false
+    }
+  }
 
   private def register(root: JComponent, completion: Completion_Popup)
   {
     Swing_Thread.require()
 
-    root.getClientProperty(Completion_Popup) match {
-      case old_completion: Completion_Popup => old_completion.hide_popup
-      case _ =>
-    }
+    dismissed(root)
     root.putClientProperty(Completion_Popup, completion)
   }
 
@@ -69,13 +81,13 @@
     {
       Swing_Thread.require()
 
+      dismissed(text_area)
+
       val view = text_area.getView
       val root = view.getRootPane
       val buffer = text_area.getBuffer
       val painter = text_area.getPainter
 
-      register(root, null)
-
       if (buffer.isEditable && !evt.isConsumed) {
         get_syntax match {
           case Some(syntax) =>

--- a/src/Tools/jEdit/src/document_view.scala	Wed Aug 28 09:12:50 2013 +0200
+++ b/src/Tools/jEdit/src/document_view.scala	Wed Aug 28 09:36:05 2013 +0200
@@ -154,7 +154,7 @@
       key_typed = Completion_Popup.Text_Area.input(text_area, PIDE.get_recent_syntax, _),
       key_pressed = (evt: KeyEvent) =>
         {
-          if (evt.getKeyCode == KeyEvent.VK_ESCAPE && Pretty_Tooltip.dismissed_all())
+          if (evt.getKeyCode == KeyEvent.VK_ESCAPE && PIDE.dismissed_popups(text_area.getView))
             evt.consume
         }
     )

--- a/src/Tools/jEdit/src/plugin.scala	Wed Aug 28 09:12:50 2013 +0200
+++ b/src/Tools/jEdit/src/plugin.scala	Wed Aug 28 09:36:05 2013 +0200
@@ -53,6 +53,16 @@
   lazy val editor = new JEdit_Editor
 
 
+  /* popups */
+
+  def dismissed_popups(view: View): Boolean =
+  {
+    val b1 = Completion_Popup.dismissed_view(view)
+    val b2 = Pretty_Tooltip.dismissed_all()
+    b1 || b2
+  }
+
+
   /* document model and view */
 
   def document_model(buffer: Buffer): Option[Document_Model] = Document_Model(buffer)
@@ -265,7 +275,7 @@
                 PIDE.init_view(buffer, text_area)
             }
             else {
-              Pretty_Tooltip.dismissed_all()
+              PIDE.dismissed_popups(text_area.getView)
               PIDE.exit_view(buffer, text_area)
             }
           }

--- a/src/Tools/jEdit/src/pretty_text_area.scala	Wed Aug 28 09:12:50 2013 +0200
+++ b/src/Tools/jEdit/src/pretty_text_area.scala	Wed Aug 28 09:36:05 2013 +0200
@@ -177,7 +177,7 @@
             evt.consume
 
           case KeyEvent.VK_ESCAPE =>
-            if (Pretty_Tooltip.dismissed_all()) evt.consume
+            if (PIDE.dismissed_popups(view)) evt.consume
 
           case _ =>
         }