more accurate start_line: avoid changing the original command (e.g. 'try', 'sledgehammer');
--- 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 {