# HG changeset patch
# User wenzelm
# Date 1468239906 -7200
# Node ID 2ce032a41a3abcd318b498273bf24eedab93c89e
# Parent  5ad98525e918f3e485132b8a58d3dee45b0aeedb
clarified indentation involving 'begin';

diff -r 5ad98525e918 -r 2ce032a41a3a src/Tools/jEdit/src/text_structure.scala
--- a/src/Tools/jEdit/src/text_structure.scala	Mon Jul 11 13:56:30 2016 +0200
+++ b/src/Tools/jEdit/src/text_structure.scala	Mon Jul 11 14:25:06 2016 +0200
@@ -78,6 +78,7 @@
 
           def indent_offset(tok: Token): Int =
             if (keywords.is_command(tok, Keyword.proof_enclose)) indent_size
+            else if (tok.is_begin) indent_size
             else 0
 
           def indent_extra: Int =
@@ -97,12 +98,19 @@
                   else (ind1, false)
               }).collectFirst({ case (i, true) => i }).getOrElse(0)
 
+          def nesting(it: Iterator[Token], open: Token => Boolean, close: Token => Boolean): Int =
+            (0 /: it)({ case (d, tok) => if (open(tok)) d + 1 else if (close(tok)) d - 1 else d })
+
+          def indent_begin: Int =
+            (nesting(nav.iterator(current_line - 1, 1).map(_.info), _.is_begin, _.is_end) max 0) *
+              indent_size
+
           val indent =
             head_token(current_line) match {
               case None => indent_structure + indent_extra
               case Some(tok) =>
-                if (keywords.is_command(tok, Keyword.theory)) 0
-                else if (tok.is_command) indent_structure - indent_offset(tok)
+                if (keywords.is_command(tok, Keyword.theory)) indent_begin
+                else if (tok.is_command) indent_structure + indent_begin - indent_offset(tok)
                 else {
                   prev_command match {
                     case None =>
@@ -112,9 +120,9 @@
                           case (true, false) => - indent_extra
                           case (false, true) => indent_extra
                         }
-                      line_indent(prev_line) + extra
+                      line_indent(prev_line) - indent_offset(tok) + extra
                     case Some(prev_tok) =>
-                      indent_structure - indent_offset(prev_tok) -
+                      indent_structure - indent_offset(tok) - indent_offset(prev_tok) -
                       indent_indent(prev_tok) + indent_size
                   }
                }