# HG changeset patch
# User wenzelm
# Date 1478081200 -3600
# Node ID f630e9385d7e03b6021616f2b00a82bd8c1b0489
# Parent  2cb3e2c2ce8b2f95efdc0d393c378bfa038b0c23
more accurate start_line: avoid changing the original command (e.g. 'try', 'sledgehammer');

diff -r 2cb3e2c2ce8b -r f630e9385d7e 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 {