# HG changeset patch
# User wenzelm
# Date 1498227401 -7200
# Node ID 148d616260143ccc2ceccccd0244e0634d1a020f
# Parent  5f02bf37324f4db9b9387f4ee6062b401e05f9d0
indent = 0 for blank lines: produce less whitespace by default;

diff -r 5f02bf37324f -r 148d61626014 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))