# HG changeset patch
# User wenzelm
# Date 1468429489 -7200
# Node ID f5c81436b93020ce708faa2f11b88a5cee9bdc86
# Parent  ff1d86b077519ae1bd09b7c67c8e1c6fdabd0e76
clarified indentation: 'begin' is treated like a separate command without indent;

diff -r ff1d86b07751 -r f5c81436b930 src/Pure/Isar/token.scala
--- a/src/Pure/Isar/token.scala	Wed Jul 13 19:02:23 2016 +0200
+++ b/src/Pure/Isar/token.scala	Wed Jul 13 19:04:49 2016 +0200
@@ -263,6 +263,7 @@
 
   def is_begin: Boolean = is_keyword("begin")
   def is_end: Boolean = is_command("end")
+  def is_begin_or_command: Boolean = is_begin || is_command
 
   def content: String =
     if (kind == Token.Kind.STRING) Scan.Parsers.quoted_content("\"", source)
diff -r ff1d86b07751 -r f5c81436b930 src/Tools/jEdit/src/isabelle.scala
--- a/src/Tools/jEdit/src/isabelle.scala	Wed Jul 13 19:02:23 2016 +0200
+++ b/src/Tools/jEdit/src/isabelle.scala	Wed Jul 13 19:04:49 2016 +0200
@@ -282,9 +282,10 @@
             val (tokens1, context1) = line_content(line_range.start, caret, context0)
             val (tokens2, _) = line_content(caret, line_range.stop, context1)
 
-            if (tokens1.nonEmpty && tokens1.head.is_command) buffer.indentLine(line, true)
+            if (tokens1.nonEmpty && tokens1.head.is_begin_or_command)
+              buffer.indentLine(line, true)
 
-            if (tokens2.isEmpty || tokens2.head.is_command)
+            if (tokens2.isEmpty || tokens2.head.is_begin_or_command)
               JEdit_Lib.buffer_edit(buffer) {
                 text_area.setSelectedText("\n")
                 if (!buffer.indentLine(line + 1, true)) text_area.goToStartOfWhiteSpace(false)
diff -r ff1d86b07751 -r f5c81436b930 src/Tools/jEdit/src/text_structure.scala
--- a/src/Tools/jEdit/src/text_structure.scala	Wed Jul 13 19:02:23 2016 +0200
+++ b/src/Tools/jEdit/src/text_structure.scala	Wed Jul 13 19:04:49 2016 +0200
@@ -68,15 +68,15 @@
               case Some(Text.Info(_, tok)) => keywords.is_quasi_command(tok)
             }
 
-          def prev_command: Option[Token] =
+          def prev_line_command: Option[Token] =
             nav.reverse_iterator(prev_line, 1).
-              collectFirst({ case Text.Info(_, tok) if tok.is_command => tok })
+              collectFirst({ case Text.Info(_, tok) if tok.is_begin_or_command => tok })
+
+          def prev_line_span: Iterator[Token] =
+            nav.reverse_iterator(prev_line, 1).map(_.info).takeWhile(tok => !tok.is_begin_or_command)
 
           def prev_span: Iterator[Token] =
-            nav.reverse_iterator(prev_line).map(_.info).takeWhile(tok => !tok.is_command)
-
-          def prev_line_span: Iterator[Token] =
-            nav.reverse_iterator(prev_line, 1).map(_.info).takeWhile(tok => !tok.is_command)
+            nav.reverse_iterator(prev_line).map(_.info).takeWhile(tok => !tok.is_begin_or_command)
 
 
           val script_indent: Text.Range => Int =
@@ -104,7 +104,7 @@
             else 0
 
           def indent_offset(tok: Token): Int =
-            if (keywords.is_command(tok, Keyword.proof_enclose) || tok.is_begin) indent_size
+            if (keywords.is_command(tok, Keyword.proof_enclose)) indent_size
             else 0
 
           def indent_brackets: Int =
@@ -122,7 +122,7 @@
             nav.reverse_iterator(current_line - 1).scanLeft((0, false))(
               { case ((ind, _), Text.Info(range, tok)) =>
                   val ind1 = ind + indent_indent(tok)
-                  if (tok.is_command && !keywords.is_command(tok, Keyword.PRF_SCRIPT == _)) {
+                  if (tok.is_begin_or_command && !keywords.is_command(tok, Keyword.PRF_SCRIPT == _)) {
                     val line = buffer.getLineOfOffset(range.start)
                     line_head(line) match {
                       case Some(info) if info.info == tok =>
@@ -133,25 +133,18 @@
                   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 =
             line_head(current_line) match {
               case None => indent_structure + indent_brackets + indent_extra
               case Some(Text.Info(range, tok)) =>
-                if (keywords.is_before_command(tok) ||
-                    keywords.is_command(tok, Keyword.theory)) indent_begin
+                if (tok.is_begin ||
+                    keywords.is_before_command(tok) ||
+                    keywords.is_command(tok, Keyword.theory)) 0
                 else if (keywords.is_command(tok, Keyword.PRF_SCRIPT == _))
                   indent_structure + script_indent(range)
-                else if (tok.is_command)
-                  indent_structure + indent_begin - indent_offset(tok)
+                else if (tok.is_command) indent_structure - indent_offset(tok)
                 else {
-                  prev_command match {
+                  prev_line_command match {
                     case None =>
                       val extra =
                         (keywords.is_quasi_command(tok), head_is_quasi_command(prev_line)) match {