tuned;
authorwenzelm
Mon, 11 Jul 2016 09:45:10 +0200
changeset 63431 8002eec44fbb
parent 63430 9c5fcd355a2d
child 63432 ba7901e94e7b
tuned;
src/Tools/jEdit/src/text_structure.scala
--- a/src/Tools/jEdit/src/text_structure.scala	Sun Jul 10 11:48:30 2016 +0200
+++ b/src/Tools/jEdit/src/text_structure.scala	Mon Jul 11 09:45:10 2016 +0200
@@ -85,16 +85,16 @@
 
           val indent =
             head_token(current_line) match {
-              case Some(tok) if tok.is_command =>
+              case None => indent_structure
+              case Some(tok) =>
                 if (keywords.is_command(tok, Keyword.theory)) 0
-                else indent_structure - indent_offset(tok)
-              case _ =>
-                if (nav.iterator(current_line, 1).isEmpty) indent_structure
+                else if (tok.is_command) indent_structure - indent_offset(tok)
                 else
                   prev_command match {
-                    case Some(tok) =>
-                      indent_structure - indent_offset(tok) - indent_indent(tok) + indent_size
                     case None => line_indent(prev_line)
+                    case Some(prev_tok) =>
+                      indent_structure - indent_offset(prev_tok) -
+                      indent_indent(prev_tok) + indent_size
                   }
             }