adhoc event handler to insert 'sendback' text into the buffer, replacing the original command

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