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';
     1 /*  Title:      Tools/jEdit/src/sendback.scala
     2     Author:     Makarius
     3 
     4 Clickable "sendback" areas within the source text.
     5 */
     6 
     7 package isabelle.jedit
     8 
     9 
    10 import isabelle._
    11 
    12 import org.gjt.sp.jedit.View
    13 
    14 
    15 object Sendback
    16 {
    17   def activate(view: View, text: String, props: Properties.T)
    18   {
    19     Swing_Thread.require()
    20 
    21     Document_View(view.getTextArea) match {
    22       case Some(doc_view) =>
    23         doc_view.rich_text_area.robust_body() {
    24           val text_area = doc_view.text_area
    25           val model = doc_view.model
    26           val buffer = model.buffer
    27           val snapshot = model.snapshot()
    28 
    29           if (!snapshot.is_outdated) {
    30             props match {
    31               case Position.Id(exec_id) =>
    32                 snapshot.state.execs.get(exec_id).map(_.command) match {
    33                   case Some(command) =>
    34                     snapshot.node.command_start(command) match {
    35                       case Some(start) =>
    36                         JEdit_Lib.buffer_edit(buffer) {
    37                           buffer.remove(start, command.proper_range.length)
    38                           buffer.insert(start, text)
    39                         }
    40                       case None =>
    41                     }
    42                   case None =>
    43                 }
    44               case _ =>
    45                 JEdit_Lib.buffer_edit(buffer) {
    46                   val text1 =
    47                     if (props.exists(_ == Markup.PADDING_LINE) &&
    48                         text_area.getSelectionCount == 0)
    49                     {
    50                       def pad(range: Text.Range): String =
    51                         if (JEdit_Lib.try_get_text(buffer, range) == Some("\n")) "" else "\n"
    52 
    53                       val caret = JEdit_Lib.point_range(buffer, text_area.getCaretPosition)
    54                       val before_caret = JEdit_Lib.point_range(buffer, caret.start - 1)
    55                       pad(before_caret) + text + pad(caret)
    56                     }
    57                     else text
    58                   text_area.setSelectedText(text1)
    59                 }
    60             }
    61           }
    62         }
    63       case None =>
    64     }
    65   }
    66 }
    67