src/Tools/jEdit/src/isabelle.scala
changeset 50341 0c65a7cfc0f3
parent 50299 f70b3712040f
child 50433 9131dadb2bf7
     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)