# HG changeset patch
# User wenzelm
# Date 1354615611 -3600
# Node ID 0c65a7cfc0f3c815c92ed98e13c4982b7c3b8c35
# Parent  72519bf5f1352455cc664c43c9adeed42233df72
provide general insert_line_padding as convenience operation, e.g. for BeanShell macros;

diff -r 72519bf5f135 -r 0c65a7cfc0f3 src/Tools/jEdit/src/isabelle.scala
--- a/src/Tools/jEdit/src/isabelle.scala	Tue Dec 04 10:02:51 2012 +0100
+++ b/src/Tools/jEdit/src/isabelle.scala	Tue Dec 04 11:06:51 2012 +0100
@@ -60,6 +60,27 @@
   def decrease_font_size(view: View): Unit = change_font_size(view, i => i - ((i / 10) max 1))
 
 
+  /* structured insert */
+
+  def insert_line_padding(text_area: JEditTextArea, text: String)
+  {
+    val buffer = text_area.getBuffer
+    JEdit_Lib.buffer_edit(buffer) {
+      val text1 =
+        if (text_area.getSelectionCount == 0) {
+          def pad(range: Text.Range): String =
+            if (JEdit_Lib.try_get_text(buffer, range) == Some("\n")) "" else "\n"
+
+          val caret = JEdit_Lib.point_range(buffer, text_area.getCaretPosition)
+          val before_caret = JEdit_Lib.point_range(buffer, caret.start - 1)
+          pad(before_caret) + text + pad(caret)
+        }
+        else text
+      text_area.setSelectedText(text1)
+    }
+  }
+
+
   /* control styles */
 
   def control_sub(text_area: JEditTextArea)
diff -r 72519bf5f135 -r 0c65a7cfc0f3 src/Tools/jEdit/src/sendback.scala
--- a/src/Tools/jEdit/src/sendback.scala	Tue Dec 04 10:02:51 2012 +0100
+++ b/src/Tools/jEdit/src/sendback.scala	Tue Dec 04 11:06:51 2012 +0100
@@ -42,21 +42,9 @@
                   case None =>
                 }
               case _ =>
-                JEdit_Lib.buffer_edit(buffer) {
-                  val text1 =
-                    if (props.exists(_ == Markup.PADDING_LINE) &&
-                        text_area.getSelectionCount == 0)
-                    {
-                      def pad(range: Text.Range): String =
-                        if (JEdit_Lib.try_get_text(buffer, range) == Some("\n")) "" else "\n"
-
-                      val caret = JEdit_Lib.point_range(buffer, text_area.getCaretPosition)
-                      val before_caret = JEdit_Lib.point_range(buffer, caret.start - 1)
-                      pad(before_caret) + text + pad(caret)
-                    }
-                    else text
-                  text_area.setSelectedText(text1)
-                }
+                if (props.exists(_ == Markup.PADDING_LINE))
+                  Isabelle.insert_line_padding(text_area, text)
+                else text_area.setSelectedText(text)
             }
           }
         }