1.1 --- a/src/Pure/PIDE/protocol.scala	Wed Apr 18 18:31:48 2012 +0200
     1.2 +++ b/src/Pure/PIDE/protocol.scala	Wed Apr 18 20:22:44 2012 +0200
     1.3 @@ -154,6 +154,15 @@
     1.4        case _ => false
     1.5      }
     1.6  
     1.7 +  object Sendback
     1.8 +  {
     1.9 +    def unapply(msg: Any): Option[XML.Body] =
    1.10 +      msg match {
    1.11 +        case XML.Elem(Markup(Isabelle_Markup.SENDBACK, _), body) => Some(body)
    1.12 +        case _ => None
    1.13 +      }
    1.14 +  }
    1.15 +
    1.16  
    1.17    /* reported positions */
    1.18  

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

     3.1 --- a/src/Tools/jEdit/src/output_dockable.scala	Wed Apr 18 18:31:48 2012 +0200
     3.2 +++ b/src/Tools/jEdit/src/output_dockable.scala	Wed Apr 18 20:22:44 2012 +0200
     3.3 @@ -28,22 +28,34 @@
     3.4    private val html_panel =
     3.5      new HTML_Panel(Isabelle.font_family(), scala.math.round(Isabelle.font_size()))
     3.6    {
     3.7 -    override val handler: PartialFunction[HTML_Panel.Event, Unit] = {
     3.8 -      case HTML_Panel.Mouse_Click(elem, event) if elem.getClassName() == "sendback" =>
     3.9 -        val text = elem.getFirstChild().getNodeValue()
    3.10 -
    3.11 +    override val handler: PartialFunction[HTML_Panel.Event, Unit] =
    3.12 +    {
    3.13 +      case HTML_Panel.Mouse_Click(elem, event)
    3.14 +      if Protocol.Sendback.unapply(elem.getUserData(Markup.Data.name)).isDefined =>
    3.15 +        val sendback = Protocol.Sendback.unapply(elem.getUserData(Markup.Data.name)).get
    3.16          Document_View(view.getTextArea) match {
    3.17            case Some(doc_view) =>
    3.18 -            val cmd = current_command.get
    3.19 -            val start_ofs = doc_view.model.snapshot().node.command_start(cmd).get
    3.20 -            val buffer = view.getBuffer
    3.21 -            buffer.beginCompoundEdit()
    3.22 -            buffer.remove(start_ofs, cmd.length)
    3.23 -            buffer.insert(start_ofs, text)
    3.24 -            buffer.endCompoundEdit()
    3.25 +            doc_view.robust_body() {
    3.26 +              current_command match {
    3.27 +                case Some(cmd) =>
    3.28 +                  val model = doc_view.model
    3.29 +                  val buffer = model.buffer
    3.30 +                  val snapshot = model.snapshot()
    3.31 +                  snapshot.node.command_start(cmd) match {
    3.32 +                    case Some(start) if !snapshot.is_outdated =>
    3.33 +                      val text = Pretty.string_of(sendback)
    3.34 +                      buffer.beginCompoundEdit()
    3.35 +                      buffer.remove(start, cmd.proper_range.length)
    3.36 +                      buffer.insert(start, text)
    3.37 +                      buffer.endCompoundEdit()
    3.38 +                    case _ =>
    3.39 +                  }
    3.40 +                case None =>
    3.41 +              }
    3.42 +            }
    3.43            case None =>
    3.44          }
    3.45 -    }       
    3.46 +    }
    3.47    }
    3.48  
    3.49    set_content(html_panel)