provide general insert_line_padding as convenience operation, e.g. for BeanShell macros;
authorwenzelm
Tue Dec 04 11:06:51 2012 +0100 (2012-12-04)
changeset 503410c65a7cfc0f3
parent 50340 72519bf5f135
child 50344 608265769ce0
provide general insert_line_padding as convenience operation, e.g. for BeanShell macros;
src/Tools/jEdit/src/isabelle.scala
src/Tools/jEdit/src/sendback.scala
     1.1 --- a/src/Tools/jEdit/src/isabelle.scala	Tue Dec 04 10:02:51 2012 +0100
     1.2 +++ b/src/Tools/jEdit/src/isabelle.scala	Tue Dec 04 11:06:51 2012 +0100
     1.3 @@ -60,6 +60,27 @@
     1.4    def decrease_font_size(view: View): Unit = change_font_size(view, i => i - ((i / 10) max 1))
     1.5  
     1.6  
     1.7 +  /* structured insert */
     1.8 +
     1.9 +  def insert_line_padding(text_area: JEditTextArea, text: String)
    1.10 +  {
    1.11 +    val buffer = text_area.getBuffer
    1.12 +    JEdit_Lib.buffer_edit(buffer) {
    1.13 +      val text1 =
    1.14 +        if (text_area.getSelectionCount == 0) {
    1.15 +          def pad(range: Text.Range): String =
    1.16 +            if (JEdit_Lib.try_get_text(buffer, range) == Some("\n")) "" else "\n"
    1.17 +
    1.18 +          val caret = JEdit_Lib.point_range(buffer, text_area.getCaretPosition)
    1.19 +          val before_caret = JEdit_Lib.point_range(buffer, caret.start - 1)
    1.20 +          pad(before_caret) + text + pad(caret)
    1.21 +        }
    1.22 +        else text
    1.23 +      text_area.setSelectedText(text1)
    1.24 +    }
    1.25 +  }
    1.26 +
    1.27 +
    1.28    /* control styles */
    1.29  
    1.30    def control_sub(text_area: JEditTextArea)
     2.1 --- a/src/Tools/jEdit/src/sendback.scala	Tue Dec 04 10:02:51 2012 +0100
     2.2 +++ b/src/Tools/jEdit/src/sendback.scala	Tue Dec 04 11:06:51 2012 +0100
     2.3 @@ -42,21 +42,9 @@
     2.4                    case None =>
     2.5                  }
     2.6                case _ =>
     2.7 -                JEdit_Lib.buffer_edit(buffer) {
     2.8 -                  val text1 =
     2.9 -                    if (props.exists(_ == Markup.PADDING_LINE) &&
    2.10 -                        text_area.getSelectionCount == 0)
    2.11 -                    {
    2.12 -                      def pad(range: Text.Range): String =
    2.13 -                        if (JEdit_Lib.try_get_text(buffer, range) == Some("\n")) "" else "\n"
    2.14 -
    2.15 -                      val caret = JEdit_Lib.point_range(buffer, text_area.getCaretPosition)
    2.16 -                      val before_caret = JEdit_Lib.point_range(buffer, caret.start - 1)
    2.17 -                      pad(before_caret) + text + pad(caret)
    2.18 -                    }
    2.19 -                    else text
    2.20 -                  text_area.setSelectedText(text1)
    2.21 -                }
    2.22 +                if (props.exists(_ == Markup.PADDING_LINE))
    2.23 +                  Isabelle.insert_line_padding(text_area, text)
    2.24 +                else text_area.setSelectedText(text)
    2.25              }
    2.26            }
    2.27          }