more accurate start_line: avoid changing the original command (e.g. 'try', 'sledgehammer');
authorwenzelm
Wed, 02 Nov 2016 11:06:40 +0100
changeset 64456 f630e9385d7e
parent 64455 2cb3e2c2ce8b
child 64457 f7aa4d0f7d02
more accurate start_line: avoid changing the original command (e.g. 'try', 'sledgehammer');
src/Tools/jEdit/src/isabelle.scala
--- a/src/Tools/jEdit/src/isabelle.scala	Tue Nov 01 21:07:13 2016 +0100
+++ b/src/Tools/jEdit/src/isabelle.scala	Wed Nov 02 11:06:40 2016 +0100
@@ -338,9 +338,9 @@
                 JEdit_Lib.buffer_edit(buffer) {
                   if (padding) {
                     text_area.moveCaretPosition(start + range.length)
+                    val start_line = text_area.getCaretLine + 1
                     text_area.setSelectedText("\n" + text)
                     val end_line = text_area.getCaretLine
-                    val start_line = end_line - split_lines(text).length
                     buffer.indentLines(start_line, end_line)
                   }
                   else {