more robust Sendback handling: JVM/jEdit paranoia for case matching, treat Pretty body not just XML.Text, replace proper_range only (without trailing whitespace);

--- a/src/Pure/PIDE/protocol.scala	Wed Apr 18 18:31:48 2012 +0200
+++ b/src/Pure/PIDE/protocol.scala	Wed Apr 18 20:22:44 2012 +0200
@@ -154,6 +154,15 @@
       case _ => false
     }
 
+  object Sendback
+  {
+    def unapply(msg: Any): Option[XML.Body] =
+      msg match {
+        case XML.Elem(Markup(Isabelle_Markup.SENDBACK, _), body) => Some(body)
+        case _ => None
+      }
+  }
+
 
   /* reported positions */
 

--- a/src/Pure/PIDE/text.scala	Wed Apr 18 18:31:48 2012 +0200
+++ b/src/Pure/PIDE/text.scala	Wed Apr 18 20:22:44 2012 +0200
@@ -41,6 +41,8 @@
 
     override def toString = "[" + start.toString + ":" + stop.toString + "]"
 
+    def length: Int = stop - start
+
     def map(f: Offset => Offset): Range = Range(f(start), f(stop))
     def +(i: Offset): Range = map(_ + i)
     def -(i: Offset): Range = map(_ - i)

--- a/src/Tools/jEdit/src/output_dockable.scala	Wed Apr 18 18:31:48 2012 +0200
+++ b/src/Tools/jEdit/src/output_dockable.scala	Wed Apr 18 20:22:44 2012 +0200
@@ -28,22 +28,34 @@
   private val html_panel =
     new HTML_Panel(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()
-
+    override val handler: PartialFunction[HTML_Panel.Event, Unit] =
+    {
+      case HTML_Panel.Mouse_Click(elem, event)
+      if Protocol.Sendback.unapply(elem.getUserData(Markup.Data.name)).isDefined =>
+        val sendback = Protocol.Sendback.unapply(elem.getUserData(Markup.Data.name)).get
         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()
+            doc_view.robust_body() {
+              current_command match {
+                case Some(cmd) =>
+                  val model = doc_view.model
+                  val buffer = model.buffer
+                  val snapshot = model.snapshot()
+                  snapshot.node.command_start(cmd) match {
+                    case Some(start) if !snapshot.is_outdated =>
+                      val text = Pretty.string_of(sendback)
+                      buffer.beginCompoundEdit()
+                      buffer.remove(start, cmd.proper_range.length)
+                      buffer.insert(start, text)
+                      buffer.endCompoundEdit()
+                    case _ =>
+                  }
+                case None =>
+              }
+            }
           case None =>
         }
-    }       
+    }
   }
 
   set_content(html_panel)