# HG changeset patch
# User wenzelm
# Date 1468262248 -7200
# Node ID afd657fffdf94a7eedcd0173d26cf84c94def2da
# Parent  b3f6e81cd13bfd2fe6b89c7f4c86a62e6ec2c7e0
indentation of brackets;

diff -r b3f6e81cd13b -r afd657fffdf9 src/Pure/General/word.scala
--- a/src/Pure/General/word.scala	Mon Jul 11 19:03:08 2016 +0200
+++ b/src/Pure/General/word.scala	Mon Jul 11 20:37:28 2016 +0200
@@ -96,4 +96,10 @@
 
   def explode(text: String): List[String] =
     explode(Character.isWhitespace(_), text)
+
+
+  /* brackets */
+
+  val open_brackets = "([{«‹⟨⌈⌊⦇⟦⦃"
+  val close_brackets = ")]}»›⟩⌉⌋⦈⟧⦄"
 }
diff -r b3f6e81cd13b -r afd657fffdf9 src/Pure/Isar/token.scala
--- a/src/Pure/Isar/token.scala	Mon Jul 11 19:03:08 2016 +0200
+++ b/src/Pure/Isar/token.scala	Mon Jul 11 20:37:28 2016 +0200
@@ -228,6 +228,8 @@
   def is_command(name: String): Boolean = kind == Token.Kind.COMMAND && source == name
   def is_keyword: Boolean = kind == Token.Kind.KEYWORD
   def is_keyword(name: String): Boolean = kind == Token.Kind.KEYWORD && source == name
+  def is_keyword(name: Char): Boolean =
+    kind == Token.Kind.KEYWORD && source.length == 1 && source(0) == name
   def is_delimiter: Boolean = is_keyword && !Symbol.is_ascii_identifier(source)
   def is_ident: Boolean = kind == Token.Kind.IDENT
   def is_sym_ident: Boolean = kind == Token.Kind.SYM_IDENT
@@ -256,6 +258,9 @@
     source.startsWith(Symbol.open) ||
     source.startsWith(Symbol.open_decoded))
 
+  def is_open_bracket: Boolean = is_keyword && Word.open_brackets.exists(is_keyword(_))
+  def is_close_bracket: Boolean = is_keyword && Word.close_brackets.exists(is_keyword(_))
+
   def is_begin: Boolean = is_keyword("begin")
   def is_end: Boolean = is_command("end")
 
diff -r b3f6e81cd13b -r afd657fffdf9 src/Tools/jEdit/src/text_structure.scala
--- a/src/Tools/jEdit/src/text_structure.scala	Mon Jul 11 19:03:08 2016 +0200
+++ b/src/Tools/jEdit/src/text_structure.scala	Mon Jul 11 20:37:28 2016 +0200
@@ -68,6 +68,9 @@
           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)
+
 
           def line_indent(line: Int): Int =
             if (line < 0 || line >= buffer.getLineCount) 0
@@ -84,6 +87,13 @@
             if (keywords.is_command(tok, Keyword.proof_enclose) || tok.is_begin) indent_size
             else 0
 
+          def indent_brackets: Int =
+            (0 /: prev_line_span)(
+              { case (i, tok) =>
+                  if (tok.is_open_bracket) i + indent_size
+                  else if (tok.is_close_bracket) i - indent_size
+                  else i })
+
           def indent_extra: Int =
             if (prev_span.exists(keywords.is_quasi_command(_))) indent_size
             else 0
@@ -110,7 +120,7 @@
 
           val indent =
             head_token(current_line) match {
-              case None => indent_structure + indent_extra
+              case None => indent_structure + indent_brackets + indent_extra
               case Some(tok) =>
                 if (keywords.is_before_command(tok) ||
                     keywords.is_command(tok, Keyword.theory)) indent_begin
@@ -124,10 +134,10 @@
                           case (true, false) => - indent_extra
                           case (false, true) => indent_extra
                         }
-                      line_indent(prev_line) - indent_offset(tok) + extra
+                      line_indent(prev_line) - indent_offset(tok) + indent_brackets + extra
                     case Some(prev_tok) =>
-                      indent_structure - indent_offset(tok) - indent_offset(prev_tok) -
-                      indent_indent(prev_tok) + indent_size
+                      indent_structure - indent_offset(tok) - indent_offset(prev_tok) +
+                      indent_brackets - indent_indent(prev_tok) + indent_size
                   }
                }
             }