more realistic sendback: pick exec_id from message position and text from buffer;

--- a/src/Pure/PIDE/command.scala	Fri Sep 21 15:39:51 2012 +0200
+++ b/src/Pure/PIDE/command.scala	Fri Sep 21 16:50:44 2012 +0200
@@ -60,16 +60,15 @@
         case XML.Elem(Markup(name, atts), body) =>
           atts match {
             case Isabelle_Markup.Serial(i) =>
-              val props = Position.purge(atts)
-              val result = XML.Elem(Markup(name, props), body)
-              val result_message = XML.Elem(Markup(Isabelle_Markup.message(name), props), body)
+              val message1 = XML.Elem(Markup(Isabelle_Markup.message(name), atts), body)
+              val message2 = XML.Elem(Markup(name, Position.purge(atts)), body)
 
-              val st0 = copy(results = results + (i -> result_message))
+              val st0 = copy(results = results + (i -> message1))
               val st1 =
-                if (Protocol.is_tracing(result)) st0
+                if (Protocol.is_tracing(message)) st0
                 else
                   (st0 /: Protocol.message_positions(command, message))(
-                    (st, range) => st.add_markup(Text.Info(range, result)))
+                    (st, range) => st.add_markup(Text.Info(range, message2)))
 
               st1
             case _ => System.err.println("Ignored message without serial number: " + message); this

--- a/src/Tools/jEdit/src/isabelle_rendering.scala	Fri Sep 21 15:39:51 2012 +0200
+++ b/src/Tools/jEdit/src/isabelle_rendering.scala	Fri Sep 21 16:50:44 2012 +0200
@@ -239,17 +239,21 @@
   }
 
 
-  def sendback(range: Text.Range): Option[Text.Info[Sendback]] =
+  def sendback(range: Text.Range): Option[Text.Info[Document.Exec_ID]] =
   {
-    snapshot.select_markup(range, Some(Set(Isabelle_Markup.SENDBACK)),
-        {
-          case Text.Info(info_range, Protocol.Sendback(body)) =>
-            Text.Info(snapshot.convert(info_range), body)
-        }) match
-    {
-      case Text.Info(_, Text.Info(range, body)) #:: _ =>
-        snapshot.node.command_at(range.start)
-          .map(command_range => Text.Info(range, Sendback(command_range._1, body)))
+    val results =
+      snapshot.cumulate_markup[(Option[Document.Exec_ID], Option[Text.Range])](range,
+        (None, None), Some(messages_include + Isabelle_Markup.SENDBACK),
+          {
+            case ((_, info), Text.Info(_, XML.Elem(Markup(name, Position.Id(id)), _)))
+            if messages_include(name) => (Some(id), info)
+
+            case ((id, _), Text.Info(info_range, XML.Elem(Markup(Isabelle_Markup.SENDBACK, _), _))) =>
+              (id, Some(snapshot.convert(info_range)))
+          })
+
+    (for (Text.Info(_, (Some(id), Some(r))) <- results) yield Text.Info(r, id)) match {
+      case res #:: _ => Some(res)
       case _ => None
     }
   }
@@ -375,6 +379,10 @@
   }
 
 
+  private val messages_include =
+    Set(Isabelle_Markup.WRITELN_MESSAGE, Isabelle_Markup.TRACING_MESSAGE,
+      Isabelle_Markup.WARNING_MESSAGE, Isabelle_Markup.ERROR_MESSAGE)
+
   private val message_colors = Map(
     Isabelle_Rendering.writeln_pri -> writeln_message_color,
     Isabelle_Rendering.tracing_pri -> tracing_message_color,
@@ -383,11 +391,8 @@
 
   def line_background(range: Text.Range): Option[(Color, Boolean)] =
   {
-    val messages =
-      Set(Isabelle_Markup.WRITELN_MESSAGE, Isabelle_Markup.TRACING_MESSAGE,
-        Isabelle_Markup.WARNING_MESSAGE, Isabelle_Markup.ERROR_MESSAGE)
     val results =
-      snapshot.cumulate_markup[Int](range, 0, Some(messages),
+      snapshot.cumulate_markup[Int](range, 0, Some(messages_include),
         {
           case (pri, Text.Info(_, XML.Elem(Markup(name, _), _)))
           if name == Isabelle_Markup.WRITELN_MESSAGE ||

--- a/src/Tools/jEdit/src/rich_text_area.scala	Fri Sep 21 15:39:51 2012 +0200
+++ b/src/Tools/jEdit/src/rich_text_area.scala	Fri Sep 21 16:50:44 2012 +0200
@@ -101,17 +101,25 @@
   private class Active_Area[A](
     rendering: Isabelle_Rendering => Text.Range => Option[Text.Info[A]])
   {
-    private var the_info: Option[Text.Info[A]] = None
+    private var the_text_info: Option[(String, Text.Info[A])] = None
 
-    def info: Option[Text.Info[A]] = the_info
+    def text_info: Option[(String, Text.Info[A])] = the_text_info
+    def info: Option[Text.Info[A]] = the_text_info.map(_._2)
 
     def update(new_info: Option[Text.Info[A]])
     {
-      val old_info = the_info
-      if (new_info != old_info) {
-        for { opt <- List(old_info, new_info); Text.Info(range, _) <- opt }
-          JEdit_Lib.invalidate_range(text_area, range)
-        the_info = new_info
+      val old_text_info = the_text_info
+      val new_text_info =
+        new_info.map(info => (text_area.getText(info.range.start, info.range.length), info))
+
+      if (new_text_info != old_text_info) {
+        for {
+          r0 <- JEdit_Lib.visible_range(text_area)
+          opt <- List(old_text_info, new_text_info)
+          (_, Text.Info(r1, _)) <- opt
+          r2 <- r1.try_restrict(r0)  // FIXME more precise?!
+        } JEdit_Lib.invalidate_range(text_area, r2)
+        the_text_info = new_text_info
       }
     }
 
@@ -127,7 +135,8 @@
 
   private val highlight_area = new Active_Area[Color]((r: Isabelle_Rendering) => r.highlight _)
   private val hyperlink_area = new Active_Area[Hyperlink]((r: Isabelle_Rendering) => r.hyperlink _)
-  private val sendback_area = new Active_Area[Sendback]((r: Isabelle_Rendering) => r.sendback _)
+  private val sendback_area =
+    new Active_Area[Document.Exec_ID]((r: Isabelle_Rendering) => r.sendback _)
 
   private val active_areas =
     List((highlight_area, true), (hyperlink_area, true), (sendback_area, false))
@@ -149,8 +158,8 @@
           case Some(Text.Info(_, link)) => link.follow(view)
           case None =>
         }
-        sendback_area.info match {
-          case Some(Text.Info(_, sendback)) => sendback.activate(view)
+        sendback_area.text_info match {
+          case Some((text, Text.Info(_, id))) => Sendback.activate(view, text, id)
           case None =>
         }
       }

--- a/src/Tools/jEdit/src/sendback.scala	Fri Sep 21 15:39:51 2012 +0200
+++ b/src/Tools/jEdit/src/sendback.scala	Fri Sep 21 16:50:44 2012 +0200
@@ -9,18 +9,12 @@
 
 import isabelle._
 
-import org.gjt.sp.jedit.{View, jEdit}
-import org.gjt.sp.jedit.textarea.JEditTextArea
+import org.gjt.sp.jedit.View
 
 
 object Sendback
 {
-  def apply(command: Command, body: XML.Body): Sendback = new Sendback(command, body)
-}
-
-class Sendback private(command: Command, body: XML.Body)
-{
-  def activate(view: View)
+  def activate(view: View, text: String, exec_id: Document.Exec_ID)
   {
     Swing_Thread.require()
 
@@ -30,15 +24,19 @@
           val model = doc_view.model
           val buffer = model.buffer
           val snapshot = model.snapshot()
-          snapshot.node.command_start(command) match {
-            case Some(start) if !snapshot.is_outdated =>
-              val text = Pretty.string_of(body)
-              try {
-                buffer.beginCompoundEdit()
-                buffer.remove(start, command.proper_range.length)
-                buffer.insert(start, text)
+
+          snapshot.state.execs.get(exec_id).map(_.command) match {
+            case Some(command) if !snapshot.is_outdated =>
+              snapshot.node.command_start(command) match {
+                case Some(start) =>
+                  try {
+                    buffer.beginCompoundEdit()
+                    buffer.remove(start, command.proper_range.length)
+                    buffer.insert(start, text)
+                  }
+                  finally { buffer.endCompoundEdit() }
+                case None =>
               }
-              finally { buffer.endCompoundEdit() }
             case _ =>
           }
         }