clarified focus after dismiss;

--- a/src/Tools/jEdit/src/pretty_tooltip.scala	Mon Jul 01 15:05:18 2013 +0200
+++ b/src/Tools/jEdit/src/pretty_tooltip.scala	Mon Jul 01 15:08:29 2013 +0200
@@ -109,6 +109,10 @@
         old.foreach(_.hide_popup)
         tip.hide_popup
         stack = rest
+        rest match {
+          case top :: _ => top.request_focus
+          case Nil =>
+        }
       case _ =>
     }
   }
@@ -273,5 +277,7 @@
   }
 
   private def hide_popup: Unit = popup.hide
+
+  private def request_focus: Unit = pretty_text_area.requestFocus
 }