1.1 --- a/src/Tools/jEdit/src/document_view.scala	Wed Jan 16 20:41:29 2013 +0100
     1.2 +++ b/src/Tools/jEdit/src/document_view.scala	Wed Jan 16 21:09:29 2013 +0100
     1.3 @@ -70,7 +70,7 @@
     1.4    def get_rendering(): Rendering = Rendering(model.snapshot(), PIDE.options.value)
     1.5  
     1.6    val rich_text_area =
     1.7 -    new Rich_Text_Area(text_area.getView, text_area, get_rendering _,
     1.8 +    new Rich_Text_Area(text_area.getView, text_area, get_rendering _, () => (),
     1.9        caret_visible = true, hovering = false)
    1.10  
    1.11  

     2.1 --- a/src/Tools/jEdit/src/pretty_text_area.scala	Wed Jan 16 20:41:29 2013 +0100
     2.2 +++ b/src/Tools/jEdit/src/pretty_text_area.scala	Wed Jan 16 21:09:29 2013 +0100
     2.3 @@ -55,6 +55,7 @@
     2.4  class Pretty_Text_Area(
     2.5    view: View,
     2.6    background: Option[Color] = None,
     2.7 +  close_action: () => Unit = () => (),
     2.8    propagate_keys: Boolean = false) extends JEditEmbeddedTextArea
     2.9  {
    2.10    text_area =>
    2.11 @@ -71,7 +72,7 @@
    2.12    private var future_rendering: Option[java.util.concurrent.Future[Unit]] = None
    2.13  
    2.14    private val rich_text_area =
    2.15 -    new Rich_Text_Area(view, text_area, () => current_rendering,
    2.16 +    new Rich_Text_Area(view, text_area, () => current_rendering, close_action,
    2.17        caret_visible = false, hovering = true)
    2.18  
    2.19    def refresh()

     3.1 --- a/src/Tools/jEdit/src/pretty_tooltip.scala	Wed Jan 16 20:41:29 2013 +0100
     3.2 +++ b/src/Tools/jEdit/src/pretty_tooltip.scala	Wed Jan 16 21:09:29 2013 +0100
     3.3 @@ -55,7 +55,8 @@
     3.4  
     3.5    /* pretty text area */
     3.6  
     3.7 -  val pretty_text_area = new Pretty_Text_Area(view, Some(rendering.tooltip_color), true)
     3.8 +  val pretty_text_area =
     3.9 +    new Pretty_Text_Area(view, Some(rendering.tooltip_color), () => window.dispose(), true)
    3.10    pretty_text_area.resize(Rendering.font_family(),
    3.11      Rendering.font_size("jedit_tooltip_font_scale").round)
    3.12    pretty_text_area.update(rendering.snapshot, results, body)

     4.1 --- a/src/Tools/jEdit/src/rich_text_area.scala	Wed Jan 16 20:41:29 2013 +0100
     4.2 +++ b/src/Tools/jEdit/src/rich_text_area.scala	Wed Jan 16 21:09:29 2013 +0100
     4.3 @@ -27,6 +27,7 @@
     4.4    view: View,
     4.5    text_area: TextArea,
     4.6    get_rendering: () => Rendering,
     4.7 +  close_action: () => Unit,
     4.8    caret_visible: Boolean,
     4.9    hovering: Boolean)
    4.10  {
    4.11 @@ -158,7 +159,9 @@
    4.12            case None =>
    4.13          }
    4.14          active_area.text_info match {
    4.15 -          case Some((text, Text.Info(_, markup))) => Active.action(view, text, markup)
    4.16 +          case Some((text, Text.Info(_, markup))) =>
    4.17 +            Active.action(view, text, markup)
    4.18 +            close_action()
    4.19            case None =>
    4.20          }
    4.21        }