# HG changeset patch
# User wenzelm
# Date 1498220476 -7200
# Node ID 8903653fc22e0b80a96f864d2f31d9b9d607ac87
# Parent  6c71a3af85a3875c8c642a1f3f2b3aa9a72cac3d
avoid trailing spaces;

diff -r 6c71a3af85a3 -r 8903653fc22e src/Tools/jEdit/src/isabelle.scala
--- a/src/Tools/jEdit/src/isabelle.scala	Fri Jun 23 11:55:33 2017 +0200
+++ b/src/Tools/jEdit/src/isabelle.scala	Fri Jun 23 14:21:16 2017 +0200
@@ -263,8 +263,8 @@
             val caret = text_area.getCaretPosition
             val (toks1, toks2) = Text_Structure.split_line_content(buffer, keywords, line, caret)
 
-            if (toks1.nonEmpty && keywords.is_indent_command(toks1.head))
-              buffer.indentLine(line, true)
+            if (toks1.isEmpty) buffer.removeTrailingWhiteSpace(Array(line))
+            else if (keywords.is_indent_command(toks1.head)) buffer.indentLine(line, true)
 
             if (toks2.isEmpty || keywords.is_indent_command(toks2.head))
               JEdit_Lib.buffer_edit(buffer) {