# HG changeset patch
# User krauss
# Date 1306362028 -7200
# Node ID 6b41a075251f252907547adef060e2fc4347bc53
# Parent  a59db667752178c40f708a304f04f831a638217b
adhoc event handler to insert 'sendback' text into the buffer, replacing the original command

diff -r a59db6677521 -r 6b41a075251f src/Tools/jEdit/src/jedit/output_dockable.scala
--- a/src/Tools/jEdit/src/jedit/output_dockable.scala	Thu May 26 00:12:30 2011 +0200
+++ b/src/Tools/jEdit/src/jedit/output_dockable.scala	Thu May 26 00:20:28 2011 +0200
@@ -26,6 +26,25 @@
 
   private val html_panel =
     new HTML_Panel(Isabelle.system, Isabelle.font_family(), scala.math.round(Isabelle.font_size()))
+  {
+    override val handler: PartialFunction[HTML_Panel.Event, Unit] = {
+      case HTML_Panel.Mouse_Click(elem, event) if elem.getClassName() == "sendback" =>
+        val text = elem.getFirstChild().getNodeValue()
+
+        Document_View(view.getTextArea) match {
+          case Some(doc_view) =>
+            val cmd = current_command.get
+            val start_ofs = doc_view.model.snapshot().node.command_start(cmd).get
+            val buffer = view.getBuffer
+            buffer.beginCompoundEdit()
+            buffer.remove(start_ofs, cmd.length)
+            buffer.insert(start_ofs, text)
+            buffer.endCompoundEdit()
+          case None =>
+        }
+    }       
+  }
+
   set_content(html_panel)