--- 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 =>
}
}