--- 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()