indent = 0 for blank lines: produce less whitespace by default;
authorwenzelm
Fri, 23 Jun 2017 16:16:41 +0200
changeset 66179 148d61626014
parent 66178 5f02bf37324f
child 66180 201d42f67bba
indent = 0 for blank lines: produce less whitespace by default;
src/Tools/jEdit/src/text_structure.scala
--- a/src/Tools/jEdit/src/text_structure.scala	Fri Jun 23 15:46:25 2017 +0200
+++ b/src/Tools/jEdit/src/text_structure.scala	Fri Jun 23 16:16:41 2017 +0200
@@ -141,8 +141,10 @@
             else 0
 
           val indent =
-            if (Token_Markup.Line_Context.before(buffer, current_line).get_context == Scan.Finished)
-            {
+            if (Token_Markup.Line_Context.before(buffer, current_line).get_context != Scan.Finished)
+              line_indent(current_line)
+            else if (Token_Markup.Line_Context.after(buffer, current_line).structure.blank) 0
+            else {
               line_head(current_line) match {
                 case Some(info @ Text.Info(range, tok)) =>
                   if (tok.is_begin ||
@@ -179,7 +181,6 @@
                   }
               }
             }
-            else line_indent(current_line)
 
           actions.clear()
           actions.add(new IndentAction.AlignOffset(indent max 0))