# HG changeset patch
# User wenzelm
# Date 1468223110 -7200
# Node ID 8002eec44fbb811fb9a785e11453dbcc4f58cf8c
# Parent  9c5fcd355a2d49b250f9adf9c7241c3211798d7d
tuned;

diff -r 9c5fcd355a2d -r 8002eec44fbb 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
                   }
             }