src/Tools/jEdit/src/sendback.scala
changeset 50215 97959912840a
parent 50195 863b1dfc396c
child 50341 0c65a7cfc0f3
     1.1 --- a/src/Tools/jEdit/src/sendback.scala	Mon Nov 26 14:43:28 2012 +0100
     1.2 +++ b/src/Tools/jEdit/src/sendback.scala	Mon Nov 26 16:16:47 2012 +0100
     1.3 @@ -14,22 +14,21 @@
     1.4  
     1.5  object Sendback
     1.6  {
     1.7 -  def activate(view: View, text: String, id: Option[Document.Exec_ID])
     1.8 +  def activate(view: View, text: String, props: Properties.T)
     1.9    {
    1.10      Swing_Thread.require()
    1.11  
    1.12      Document_View(view.getTextArea) match {
    1.13        case Some(doc_view) =>
    1.14          doc_view.rich_text_area.robust_body() {
    1.15 +          val text_area = doc_view.text_area
    1.16            val model = doc_view.model
    1.17            val buffer = model.buffer
    1.18            val snapshot = model.snapshot()
    1.19  
    1.20            if (!snapshot.is_outdated) {
    1.21 -            id match {
    1.22 -              case None =>
    1.23 -                doc_view.text_area.setSelectedText(text)
    1.24 -              case Some(exec_id) =>
    1.25 +            props match {
    1.26 +              case Position.Id(exec_id) =>
    1.27                  snapshot.state.execs.get(exec_id).map(_.command) match {
    1.28                    case Some(command) =>
    1.29                      snapshot.node.command_start(command) match {
    1.30 @@ -42,6 +41,22 @@
    1.31                      }
    1.32                    case None =>
    1.33                  }
    1.34 +              case _ =>
    1.35 +                JEdit_Lib.buffer_edit(buffer) {
    1.36 +                  val text1 =
    1.37 +                    if (props.exists(_ == Markup.PADDING_LINE) &&
    1.38 +                        text_area.getSelectionCount == 0)
    1.39 +                    {
    1.40 +                      def pad(range: Text.Range): String =
    1.41 +                        if (JEdit_Lib.try_get_text(buffer, range) == Some("\n")) "" else "\n"
    1.42 +
    1.43 +                      val caret = JEdit_Lib.point_range(buffer, text_area.getCaretPosition)
    1.44 +                      val before_caret = JEdit_Lib.point_range(buffer, caret.start - 1)
    1.45 +                      pad(before_caret) + text + pad(caret)
    1.46 +                    }
    1.47 +                    else text
    1.48 +                  text_area.setSelectedText(text1)
    1.49 +                }
    1.50              }
    1.51            }
    1.52          }