# HG changeset patch
# User wenzelm
# Date 1468432244 -7200
# Node ID 05908c773ca707720fd29234831af93d8b968c63
# Parent  464ef556bd218d69819c7f210226e31b077ffcdc
tuned;

diff -r 464ef556bd21 -r 05908c773ca7 src/Tools/jEdit/src/text_structure.scala
--- a/src/Tools/jEdit/src/text_structure.scala	Wed Jul 13 19:36:47 2016 +0200
+++ b/src/Tools/jEdit/src/text_structure.scala	Wed Jul 13 19:50:44 2016 +0200
@@ -26,13 +26,13 @@
     def iterator(line: Int, lim: Int = limit): Iterator[Text.Info[Token]] =
     {
       val it = Token_Markup.line_token_iterator(syntax, buffer, line, line + lim)
-      if (comments) it.filterNot(_.info.is_space) else it.filter(_.info.is_proper)
+      if (comments) it.filterNot(_.info.is_space) else it.filterNot(_.info.is_improper)
     }
 
     def reverse_iterator(line: Int, lim: Int = limit): Iterator[Text.Info[Token]] =
     {
       val it = Token_Markup.line_token_reverse_iterator(syntax, buffer, line, line - lim)
-      if (comments) it.filterNot(_.info.is_space) else it.filter(_.info.is_proper)
+      if (comments) it.filterNot(_.info.is_space) else it.filterNot(_.info.is_improper)
     }
   }
 
@@ -107,17 +107,6 @@
             if (keywords.is_command(tok, Keyword.proof_enclose)) indent_size
             else 0
 
-          def indent_brackets: Int =
-            (0 /: prev_line_span)(
-              { case (i, tok) =>
-                  if (tok.is_open_bracket) i + indent_size
-                  else if (tok.is_close_bracket) i - indent_size
-                  else i })
-
-          def indent_extra: Int =
-            if (prev_span.exists(keywords.is_quasi_command(_))) indent_size
-            else 0
-
           def indent_structure: Int =
             nav.reverse_iterator(current_line - 1).scanLeft((0, false))(
               { case ((ind, _), Text.Info(range, tok)) =>
@@ -133,6 +122,17 @@
                   else (ind1, false)
               }).collectFirst({ case (i, true) => i }).getOrElse(0)
 
+          def indent_brackets: Int =
+            (0 /: prev_line_span)(
+              { case (i, tok) =>
+                  if (tok.is_open_bracket) i + indent_size
+                  else if (tok.is_close_bracket) i - indent_size
+                  else i })
+
+          def indent_extra: Int =
+            if (prev_span.exists(keywords.is_quasi_command(_))) indent_size
+            else 0
+
           val indent =
             line_head(current_line) match {
               case None => indent_structure + indent_brackets + indent_extra