src/Tools/jEdit/src/sendback.scala
author wenzelm
Fri, 21 Sep 2012 15:39:51 +0200
changeset 49492 2e3e7ea5ce8e
child 49493 db58490a68ac
permissions -rw-r--r--
some support for hovering and sendback area;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
49492
2e3e7ea5ce8e some support for hovering and sendback area;
wenzelm
parents:
diff changeset
     1
/*  Title:      Tools/jEdit/src/sendback.scala
2e3e7ea5ce8e some support for hovering and sendback area;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
2e3e7ea5ce8e some support for hovering and sendback area;
wenzelm
parents:
diff changeset
     3
2e3e7ea5ce8e some support for hovering and sendback area;
wenzelm
parents:
diff changeset
     4
Clickable "sendback" areas within the source text.
2e3e7ea5ce8e some support for hovering and sendback area;
wenzelm
parents:
diff changeset
     5
*/
2e3e7ea5ce8e some support for hovering and sendback area;
wenzelm
parents:
diff changeset
     6
2e3e7ea5ce8e some support for hovering and sendback area;
wenzelm
parents:
diff changeset
     7
package isabelle.jedit
2e3e7ea5ce8e some support for hovering and sendback area;
wenzelm
parents:
diff changeset
     8
2e3e7ea5ce8e some support for hovering and sendback area;
wenzelm
parents:
diff changeset
     9
2e3e7ea5ce8e some support for hovering and sendback area;
wenzelm
parents:
diff changeset
    10
import isabelle._
2e3e7ea5ce8e some support for hovering and sendback area;
wenzelm
parents:
diff changeset
    11
2e3e7ea5ce8e some support for hovering and sendback area;
wenzelm
parents:
diff changeset
    12
import org.gjt.sp.jedit.{View, jEdit}
2e3e7ea5ce8e some support for hovering and sendback area;
wenzelm
parents:
diff changeset
    13
import org.gjt.sp.jedit.textarea.JEditTextArea
2e3e7ea5ce8e some support for hovering and sendback area;
wenzelm
parents:
diff changeset
    14
2e3e7ea5ce8e some support for hovering and sendback area;
wenzelm
parents:
diff changeset
    15
2e3e7ea5ce8e some support for hovering and sendback area;
wenzelm
parents:
diff changeset
    16
object Sendback
2e3e7ea5ce8e some support for hovering and sendback area;
wenzelm
parents:
diff changeset
    17
{
2e3e7ea5ce8e some support for hovering and sendback area;
wenzelm
parents:
diff changeset
    18
  def apply(command: Command, body: XML.Body): Sendback = new Sendback(command, body)
2e3e7ea5ce8e some support for hovering and sendback area;
wenzelm
parents:
diff changeset
    19
}
2e3e7ea5ce8e some support for hovering and sendback area;
wenzelm
parents:
diff changeset
    20
2e3e7ea5ce8e some support for hovering and sendback area;
wenzelm
parents:
diff changeset
    21
class Sendback private(command: Command, body: XML.Body)
2e3e7ea5ce8e some support for hovering and sendback area;
wenzelm
parents:
diff changeset
    22
{
2e3e7ea5ce8e some support for hovering and sendback area;
wenzelm
parents:
diff changeset
    23
  def activate(view: View)
2e3e7ea5ce8e some support for hovering and sendback area;
wenzelm
parents:
diff changeset
    24
  {
2e3e7ea5ce8e some support for hovering and sendback area;
wenzelm
parents:
diff changeset
    25
    Swing_Thread.require()
2e3e7ea5ce8e some support for hovering and sendback area;
wenzelm
parents:
diff changeset
    26
2e3e7ea5ce8e some support for hovering and sendback area;
wenzelm
parents:
diff changeset
    27
    Document_View(view.getTextArea) match {
2e3e7ea5ce8e some support for hovering and sendback area;
wenzelm
parents:
diff changeset
    28
      case Some(doc_view) =>
2e3e7ea5ce8e some support for hovering and sendback area;
wenzelm
parents:
diff changeset
    29
        doc_view.rich_text_area.robust_body() {
2e3e7ea5ce8e some support for hovering and sendback area;
wenzelm
parents:
diff changeset
    30
          val model = doc_view.model
2e3e7ea5ce8e some support for hovering and sendback area;
wenzelm
parents:
diff changeset
    31
          val buffer = model.buffer
2e3e7ea5ce8e some support for hovering and sendback area;
wenzelm
parents:
diff changeset
    32
          val snapshot = model.snapshot()
2e3e7ea5ce8e some support for hovering and sendback area;
wenzelm
parents:
diff changeset
    33
          snapshot.node.command_start(command) match {
2e3e7ea5ce8e some support for hovering and sendback area;
wenzelm
parents:
diff changeset
    34
            case Some(start) if !snapshot.is_outdated =>
2e3e7ea5ce8e some support for hovering and sendback area;
wenzelm
parents:
diff changeset
    35
              val text = Pretty.string_of(body)
2e3e7ea5ce8e some support for hovering and sendback area;
wenzelm
parents:
diff changeset
    36
              try {
2e3e7ea5ce8e some support for hovering and sendback area;
wenzelm
parents:
diff changeset
    37
                buffer.beginCompoundEdit()
2e3e7ea5ce8e some support for hovering and sendback area;
wenzelm
parents:
diff changeset
    38
                buffer.remove(start, command.proper_range.length)
2e3e7ea5ce8e some support for hovering and sendback area;
wenzelm
parents:
diff changeset
    39
                buffer.insert(start, text)
2e3e7ea5ce8e some support for hovering and sendback area;
wenzelm
parents:
diff changeset
    40
              }
2e3e7ea5ce8e some support for hovering and sendback area;
wenzelm
parents:
diff changeset
    41
              finally { buffer.endCompoundEdit() }
2e3e7ea5ce8e some support for hovering and sendback area;
wenzelm
parents:
diff changeset
    42
            case _ =>
2e3e7ea5ce8e some support for hovering and sendback area;
wenzelm
parents:
diff changeset
    43
          }
2e3e7ea5ce8e some support for hovering and sendback area;
wenzelm
parents:
diff changeset
    44
        }
2e3e7ea5ce8e some support for hovering and sendback area;
wenzelm
parents:
diff changeset
    45
      case None =>
2e3e7ea5ce8e some support for hovering and sendback area;
wenzelm
parents:
diff changeset
    46
    }
2e3e7ea5ce8e some support for hovering and sendback area;
wenzelm
parents:
diff changeset
    47
  }
2e3e7ea5ce8e some support for hovering and sendback area;
wenzelm
parents:
diff changeset
    48
}
2e3e7ea5ce8e some support for hovering and sendback area;
wenzelm
parents:
diff changeset
    49