src/Tools/jEdit/src/sendback.scala
author wenzelm
Mon Nov 26 16:16:47 2012 +0100 (2012-11-26 ago)
changeset 50215 97959912840a
parent 50195 863b1dfc396c
child 50341 0c65a7cfc0f3
permissions -rw-r--r--
more general sendback properties;
support for padding of line boundary, e.g. for ad-hoc insertion of commands via 'help';
wenzelm@49492
     1
/*  Title:      Tools/jEdit/src/sendback.scala
wenzelm@49492
     2
    Author:     Makarius
wenzelm@49492
     3
wenzelm@49492
     4
Clickable "sendback" areas within the source text.
wenzelm@49492
     5
*/
wenzelm@49492
     6
wenzelm@49492
     7
package isabelle.jedit
wenzelm@49492
     8
wenzelm@49492
     9
wenzelm@49492
    10
import isabelle._
wenzelm@49492
    11
wenzelm@49493
    12
import org.gjt.sp.jedit.View
wenzelm@49492
    13
wenzelm@49492
    14
wenzelm@49492
    15
object Sendback
wenzelm@49492
    16
{
wenzelm@50215
    17
  def activate(view: View, text: String, props: Properties.T)
wenzelm@49492
    18
  {
wenzelm@49492
    19
    Swing_Thread.require()
wenzelm@49492
    20
wenzelm@49492
    21
    Document_View(view.getTextArea) match {
wenzelm@49492
    22
      case Some(doc_view) =>
wenzelm@49492
    23
        doc_view.rich_text_area.robust_body() {
wenzelm@50215
    24
          val text_area = doc_view.text_area
wenzelm@49492
    25
          val model = doc_view.model
wenzelm@49492
    26
          val buffer = model.buffer
wenzelm@49492
    27
          val snapshot = model.snapshot()
wenzelm@49493
    28
wenzelm@50164
    29
          if (!snapshot.is_outdated) {
wenzelm@50215
    30
            props match {
wenzelm@50215
    31
              case Position.Id(exec_id) =>
wenzelm@50164
    32
                snapshot.state.execs.get(exec_id).map(_.command) match {
wenzelm@50164
    33
                  case Some(command) =>
wenzelm@50164
    34
                    snapshot.node.command_start(command) match {
wenzelm@50164
    35
                      case Some(start) =>
wenzelm@50195
    36
                        JEdit_Lib.buffer_edit(buffer) {
wenzelm@50164
    37
                          buffer.remove(start, command.proper_range.length)
wenzelm@50164
    38
                          buffer.insert(start, text)
wenzelm@50164
    39
                        }
wenzelm@50164
    40
                      case None =>
wenzelm@50164
    41
                    }
wenzelm@50164
    42
                  case None =>
wenzelm@50164
    43
                }
wenzelm@50215
    44
              case _ =>
wenzelm@50215
    45
                JEdit_Lib.buffer_edit(buffer) {
wenzelm@50215
    46
                  val text1 =
wenzelm@50215
    47
                    if (props.exists(_ == Markup.PADDING_LINE) &&
wenzelm@50215
    48
                        text_area.getSelectionCount == 0)
wenzelm@50215
    49
                    {
wenzelm@50215
    50
                      def pad(range: Text.Range): String =
wenzelm@50215
    51
                        if (JEdit_Lib.try_get_text(buffer, range) == Some("\n")) "" else "\n"
wenzelm@50215
    52
wenzelm@50215
    53
                      val caret = JEdit_Lib.point_range(buffer, text_area.getCaretPosition)
wenzelm@50215
    54
                      val before_caret = JEdit_Lib.point_range(buffer, caret.start - 1)
wenzelm@50215
    55
                      pad(before_caret) + text + pad(caret)
wenzelm@50215
    56
                    }
wenzelm@50215
    57
                    else text
wenzelm@50215
    58
                  text_area.setSelectedText(text1)
wenzelm@50215
    59
                }
wenzelm@50164
    60
            }
wenzelm@49492
    61
          }
wenzelm@49492
    62
        }
wenzelm@49492
    63
      case None =>
wenzelm@49492
    64
    }
wenzelm@49492
    65
  }
wenzelm@49492
    66
}
wenzelm@49492
    67