# HG changeset patch
# User wenzelm
# Date 1358366969 -3600
# Node ID 12de8ea66f54b707d46b0711f8e9d5cd1c63490b
# Parent  fe4714886d923bb283ad02df94626fa944dbd175
close tooltip after Active.action, to make it look more interactive (notably due to lack of dynamic update);

diff -r fe4714886d92 -r 12de8ea66f54 src/Tools/jEdit/src/document_view.scala
--- a/src/Tools/jEdit/src/document_view.scala	Wed Jan 16 20:41:29 2013 +0100
+++ b/src/Tools/jEdit/src/document_view.scala	Wed Jan 16 21:09:29 2013 +0100
@@ -70,7 +70,7 @@
   def get_rendering(): Rendering = Rendering(model.snapshot(), PIDE.options.value)
 
   val rich_text_area =
-    new Rich_Text_Area(text_area.getView, text_area, get_rendering _,
+    new Rich_Text_Area(text_area.getView, text_area, get_rendering _, () => (),
       caret_visible = true, hovering = false)
 
 
diff -r fe4714886d92 -r 12de8ea66f54 src/Tools/jEdit/src/pretty_text_area.scala
--- a/src/Tools/jEdit/src/pretty_text_area.scala	Wed Jan 16 20:41:29 2013 +0100
+++ b/src/Tools/jEdit/src/pretty_text_area.scala	Wed Jan 16 21:09:29 2013 +0100
@@ -55,6 +55,7 @@
 class Pretty_Text_Area(
   view: View,
   background: Option[Color] = None,
+  close_action: () => Unit = () => (),
   propagate_keys: Boolean = false) extends JEditEmbeddedTextArea
 {
   text_area =>
@@ -71,7 +72,7 @@
   private var future_rendering: Option[java.util.concurrent.Future[Unit]] = None
 
   private val rich_text_area =
-    new Rich_Text_Area(view, text_area, () => current_rendering,
+    new Rich_Text_Area(view, text_area, () => current_rendering, close_action,
       caret_visible = false, hovering = true)
 
   def refresh()
diff -r fe4714886d92 -r 12de8ea66f54 src/Tools/jEdit/src/pretty_tooltip.scala
--- a/src/Tools/jEdit/src/pretty_tooltip.scala	Wed Jan 16 20:41:29 2013 +0100
+++ b/src/Tools/jEdit/src/pretty_tooltip.scala	Wed Jan 16 21:09:29 2013 +0100
@@ -55,7 +55,8 @@
 
   /* pretty text area */
 
-  val pretty_text_area = new Pretty_Text_Area(view, Some(rendering.tooltip_color), true)
+  val pretty_text_area =
+    new Pretty_Text_Area(view, Some(rendering.tooltip_color), () => window.dispose(), true)
   pretty_text_area.resize(Rendering.font_family(),
     Rendering.font_size("jedit_tooltip_font_scale").round)
   pretty_text_area.update(rendering.snapshot, results, body)
diff -r fe4714886d92 -r 12de8ea66f54 src/Tools/jEdit/src/rich_text_area.scala
--- a/src/Tools/jEdit/src/rich_text_area.scala	Wed Jan 16 20:41:29 2013 +0100
+++ b/src/Tools/jEdit/src/rich_text_area.scala	Wed Jan 16 21:09:29 2013 +0100
@@ -27,6 +27,7 @@
   view: View,
   text_area: TextArea,
   get_rendering: () => Rendering,
+  close_action: () => Unit,
   caret_visible: Boolean,
   hovering: Boolean)
 {
@@ -158,7 +159,9 @@
           case None =>
         }
         active_area.text_info match {
-          case Some((text, Text.Info(_, markup))) => Active.action(view, text, markup)
+          case Some((text, Text.Info(_, markup))) =>
+            Active.action(view, text, markup)
+            close_action()
           case None =>
         }
       }