# HG changeset patch
# User wenzelm
# Date 1468247808 -7200
# Node ID f6b5124b7023c39d282acbbc029e9c31d7fdaed5
# Parent  4c3fa4dba79f1bb91bcd2c80dde1f18692a3e591
clarified indentation;

diff -r 4c3fa4dba79f -r f6b5124b7023 src/Tools/jEdit/src/text_structure.scala
--- a/src/Tools/jEdit/src/text_structure.scala	Mon Jul 11 16:36:29 2016 +0200
+++ b/src/Tools/jEdit/src/text_structure.scala	Mon Jul 11 16:36:48 2016 +0200
@@ -109,7 +109,8 @@
             head_token(current_line) match {
               case None => indent_structure + indent_extra
               case Some(tok) =>
-                if (keywords.is_command(tok, Keyword.theory)) indent_begin
+                if (keywords.is_before_command(tok) ||
+                    keywords.is_command(tok, Keyword.theory)) indent_begin
                 else if (tok.is_command) indent_structure + indent_begin - indent_offset(tok)
                 else {
                   prev_command match {