# HG changeset patch
# User wenzelm
# Date 1468433097 -7200
# Node ID 2c9444125485bae292fb3beacf839fe0828f4a1a
# Parent  cf2d332acb7c6c28fe636d175f37505de6a465de
tuned;

diff -r cf2d332acb7c -r 2c9444125485 src/Tools/jEdit/src/text_structure.scala
--- a/src/Tools/jEdit/src/text_structure.scala	Wed Jul 13 20:00:56 2016 +0200
+++ b/src/Tools/jEdit/src/text_structure.scala	Wed Jul 13 20:04:57 2016 +0200
@@ -155,10 +155,10 @@
                           case (true, false) => - indent_extra
                           case (false, true) => indent_extra
                         }
-                      line_indent(prev_line) - indent_offset(tok) + indent_brackets + extra
+                      line_indent(prev_line) + indent_brackets + extra - indent_offset(tok)
                     case Some(prev_tok) =>
-                      indent_structure - indent_offset(tok) - indent_offset(prev_tok) +
-                      indent_brackets - indent_indent(prev_tok) + indent_size
+                      indent_structure + indent_brackets + indent_size - indent_offset(tok) -
+                      indent_offset(prev_tok) - indent_indent(prev_tok)
                   }
                }
             }