# HG changeset patch
# User wenzelm
# Date 1468267622 -7200
# Node ID 932a3d4702641f66368884a7eb28359d60690081
# Parent  6b82bad2277f33011616ea0c40ae2fde20654dd2# Parent  52349e41d5dc51865d27c0a8b1b41a3af726ad00
merged

diff -r 6b82bad2277f -r 932a3d470264 NEWS
--- a/NEWS	Mon Jul 11 21:02:26 2016 +0200
+++ b/NEWS	Mon Jul 11 22:07:02 2016 +0200
@@ -76,6 +76,9 @@
 
 * Highlighting of entity def/ref positions wrt. cursor.
 
+* Indentation according to Isabelle outer syntax, cf. action
+"indent-lines" (shortcut C+i).
+
 * Action "isabelle.select-entity" (shortcut CS+ENTER) selects all
 occurences of the formal entity at the caret position. This facilitates
 systematic renaming.
diff -r 6b82bad2277f -r 932a3d470264 src/Pure/General/word.scala
--- a/src/Pure/General/word.scala	Mon Jul 11 21:02:26 2016 +0200
+++ b/src/Pure/General/word.scala	Mon Jul 11 22:07:02 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 6b82bad2277f -r 932a3d470264 src/Pure/Isar/keyword.ML
--- a/src/Pure/Isar/keyword.ML	Mon Jul 11 21:02:26 2016 +0200
+++ b/src/Pure/Isar/keyword.ML	Mon Jul 11 22:07:02 2016 +0200
@@ -32,9 +32,11 @@
   val prf_script: string
   val prf_script_goal: string
   val prf_script_asm_goal: string
+  val before_command: string
   val quasi_command: string
   type spec = (string * string list) * string list
   val no_spec: spec
+  val before_command_spec: spec
   val quasi_command_spec: spec
   type keywords
   val minor_keywords: keywords -> Scan.lexicon
@@ -107,6 +109,8 @@
 val prf_script = "prf_script";
 val prf_script_goal = "prf_script_goal";
 val prf_script_asm_goal = "prf_script_asm_goal";
+
+val before_command = "before_command";
 val quasi_command = "quasi_command";
 
 val command_kinds =
@@ -121,6 +125,7 @@
 type spec = (string * string list) * string list;
 
 val no_spec: spec = (("", []), []);
+val before_command_spec: spec = ((before_command, []), []);
 val quasi_command_spec: spec = ((quasi_command, []), []);
 
 type entry =
@@ -175,7 +180,7 @@
 
 val add_keywords =
   fold (fn ((name, pos), spec as ((kind, _), _)) => map_keywords (fn (minor, major, commands) =>
-    if kind = "" orelse kind = quasi_command then
+    if kind = "" orelse kind = before_command orelse kind = quasi_command then
       let
         val minor' = Scan.extend_lexicon (Symbol.explode name) minor;
       in (minor', major, commands) end
diff -r 6b82bad2277f -r 932a3d470264 src/Pure/Isar/keyword.scala
--- a/src/Pure/Isar/keyword.scala	Mon Jul 11 21:02:26 2016 +0200
+++ b/src/Pure/Isar/keyword.scala	Mon Jul 11 22:07:02 2016 +0200
@@ -39,6 +39,8 @@
   val PRF_SCRIPT = "prf_script"
   val PRF_SCRIPT_GOAL = "prf_script_goal"
   val PRF_SCRIPT_ASM_GOAL = "prf_script_asm_goal"
+
+  val BEFORE_COMMAND = "before_command"
   val QUASI_COMMAND = "quasi_command"
 
 
@@ -90,6 +92,7 @@
   type Spec = ((String, List[String]), List[String])
 
   val no_spec: Spec = (("", Nil), Nil)
+  val before_command_spec: Spec = ((BEFORE_COMMAND, Nil), Nil)
   val quasi_command_spec: Spec = ((QUASI_COMMAND, Nil), Nil)
 
   object Keywords
@@ -100,22 +103,20 @@
   class Keywords private(
     val minor: Scan.Lexicon = Scan.Lexicon.empty,
     val major: Scan.Lexicon = Scan.Lexicon.empty,
-    protected val quasi_commands: Set[String] = Set.empty,
-    protected val commands: Map[String, (String, List[String])] = Map.empty)
+    val kinds: Map[String, String] = Map.empty,
+    val load_commands: Map[String, List[String]] = Map.empty)
   {
     override def toString: String =
     {
-      val keywords1 =
-        for (name <- minor.iterator.toList) yield {
-          if (quasi_commands.contains(name)) (name, quote(name) + " :: \"quasi_command\"")
-          else (name, quote(name))
+      val entries =
+        for ((name, kind) <- kinds.toList.sortBy(_._1)) yield {
+          val exts = load_commands.getOrElse(name, Nil)
+          val kind_decl =
+            if (kind == "") ""
+            else " :: " + quote(kind) + (if (exts.isEmpty) "" else " (" + commas_quote(exts) + ")")
+          quote(name) + kind_decl
         }
-      val keywords2 =
-        for ((name, (kind, files)) <- commands.toList) yield {
-          (name, quote(name) + " :: " + quote(kind) +
-            (if (files.isEmpty) "" else " (" + commas_quote(files) + ")"))
-        }
-      (keywords1 ::: keywords2).sortBy(_._1).map(_._2).mkString("keywords\n  ", " and\n  ", "")
+      entries.mkString("keywords\n  ", " and\n  ", "")
     }
 
 
@@ -129,58 +130,58 @@
       else {
         val minor1 = minor ++ other.minor
         val major1 = major ++ other.major
-        val quasi_commands1 = quasi_commands ++ other.quasi_commands
-        val commands1 =
-          if (commands eq other.commands) commands
-          else if (commands.isEmpty) other.commands
-          else (commands /: other.commands) { case (m, e) => if (m.isDefinedAt(e._1)) m else m + e }
-        new Keywords(minor1, major1, quasi_commands1, commands1)
+        val kinds1 =
+          if (kinds eq other.kinds) kinds
+          else if (kinds.isEmpty) other.kinds
+          else (kinds /: other.kinds) { case (m, e) => if (m.isDefinedAt(e._1)) m else m + e }
+        val load_commands1 =
+          if (load_commands eq other.load_commands) load_commands
+          else if (load_commands.isEmpty) other.load_commands
+          else
+            (load_commands /: other.load_commands) {
+              case (m, e) => if (m.isDefinedAt(e._1)) m else m + e }
+        new Keywords(minor1, major1, kinds1, load_commands1)
       }
 
 
     /* add keywords */
 
-    def + (name: String, kind: String = "", tags: List[String] = Nil): Keywords =
-      if (kind == "") new Keywords(minor + name, major, quasi_commands, commands)
-      else if (kind == QUASI_COMMAND)
-        new Keywords(minor + name, major, quasi_commands + name, commands)
-      else {
-        val major1 = major + name
-        val commands1 = commands + (name -> (kind, tags))
-        new Keywords(minor, major1, quasi_commands, commands1)
-      }
+    def + (name: String, kind: String = "", exts: List[String] = Nil): Keywords =
+    {
+      val kinds1 = kinds + (name -> kind)
+      val (minor1, major1) =
+        if (kind == "" || kind == BEFORE_COMMAND || kind == QUASI_COMMAND)
+          (minor + name, major)
+        else (minor, major + name)
+      val load_commands1 =
+        if (kind == THY_LOAD) load_commands + (name -> exts)
+        else load_commands
+      new Keywords(minor1, major1, kinds1, load_commands1)
+    }
 
     def add_keywords(header: Thy_Header.Keywords): Keywords =
       (this /: header) {
-        case (keywords, (name, ((kind, tags), _), _)) =>
+        case (keywords, (name, ((kind, exts), _), _)) =>
           if (kind == "") keywords + Symbol.decode(name) + Symbol.encode(name)
-          else keywords + (Symbol.decode(name), kind, tags) + (Symbol.encode(name), kind, tags)
+          else keywords + (Symbol.decode(name), kind, exts) + (Symbol.encode(name), kind, exts)
       }
 
 
     /* command kind */
 
-    def command_kind(name: String): Option[String] = commands.get(name).map(_._1)
-
     def is_command(token: Token, check_kind: String => Boolean): Boolean =
       token.is_command &&
-        (command_kind(token.source) match { case Some(k) => check_kind(k) case None => false })
+        (kinds.get(token.source) match { case Some(k) => check_kind(k) case None => false })
+
+    def is_before_command(token: Token): Boolean =
+      token.is_keyword && kinds.get(token.source) == Some(BEFORE_COMMAND)
 
     def is_quasi_command(token: Token): Boolean =
-      token.is_keyword && quasi_commands.contains(token.source)
+      token.is_keyword && kinds.get(token.source) == Some(QUASI_COMMAND)
 
 
     /* load commands */
 
-    def load_command(name: String): Option[List[String]] =
-      commands.get(name) match {
-        case Some((THY_LOAD, exts)) => Some(exts)
-        case _ => None
-      }
-
-    private lazy val load_commands: List[(String, List[String])] =
-      (for ((name, (THY_LOAD, files)) <- commands.iterator) yield (name, files)).toList
-
     def load_commands_in(text: String): Boolean =
       load_commands.exists({ case (cmd, _) => text.containsSlice(cmd) })
   }
diff -r 6b82bad2277f -r 932a3d470264 src/Pure/Isar/outer_syntax.scala
--- a/src/Pure/Isar/outer_syntax.scala	Mon Jul 11 21:02:26 2016 +0200
+++ b/src/Pure/Isar/outer_syntax.scala	Mon Jul 11 22:07:02 2016 +0200
@@ -118,7 +118,7 @@
 
   /* load commands */
 
-  def load_command(name: String): Option[List[String]] = keywords.load_command(name)
+  def load_command(name: String): Option[List[String]] = keywords.load_commands.get(name)
   def load_commands_in(text: String): Boolean = keywords.load_commands_in(text)
 
 
@@ -209,8 +209,9 @@
 
     for (tok <- toks) {
       if (tok.is_improper) improper += tok
-      else if (tok.is_command_modifier ||
-        tok.is_command && (!content.exists(_.is_command_modifier) || content.exists(_.is_command)))
+      else if (keywords.is_before_command(tok) ||
+        tok.is_command &&
+          (!content.exists(keywords.is_before_command(_)) || content.exists(_.is_command)))
       { flush(); content += tok }
       else { content ++= improper; improper.clear; content += tok }
     }
@@ -236,7 +237,7 @@
       case Thy_Header.PARAGRAPH => Some(4)
       case Thy_Header.SUBPARAGRAPH => Some(5)
       case _ =>
-        keywords.command_kind(name) match {
+        keywords.kinds.get(name) match {
           case Some(kind) if Keyword.theory(kind) && !Keyword.theory_end(kind) => Some(6)
           case _ => None
         }
diff -r 6b82bad2277f -r 932a3d470264 src/Pure/Isar/parse.scala
--- a/src/Pure/Isar/parse.scala	Mon Jul 11 21:02:26 2016 +0200
+++ b/src/Pure/Isar/parse.scala	Mon Jul 11 22:07:02 2016 +0200
@@ -59,12 +59,8 @@
     def atom(s: String, pred: Elem => Boolean): Parser[String] =
       token(s, pred) ^^ (_.content)
 
-    def command(name: String): Parser[String] =
-      atom("command " + quote(name), tok => tok.is_command && tok.source == name)
-
-    def $$$(name: String): Parser[String] =
-      atom("keyword " + quote(name), tok => tok.is_keyword && tok.source == name)
-
+    def command(name: String): Parser[String] = atom("command " + quote(name), _.is_command(name))
+    def $$$(name: String): Parser[String] = atom("keyword " + quote(name), _.is_keyword(name))
     def string: Parser[String] = atom("string", _.is_string)
     def nat: Parser[Int] = atom("natural number", _.is_nat) ^^ (s => Integer.parseInt(s))
     def name: Parser[String] = atom("name", _.is_name)
diff -r 6b82bad2277f -r 932a3d470264 src/Pure/Isar/token.scala
--- a/src/Pure/Isar/token.scala	Mon Jul 11 21:02:26 2016 +0200
+++ b/src/Pure/Isar/token.scala	Mon Jul 11 22:07:02 2016 +0200
@@ -225,7 +225,11 @@
 sealed case class Token(kind: Token.Kind.Value, source: String)
 {
   def is_command: Boolean = kind == Token.Kind.COMMAND
+  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
@@ -254,12 +258,11 @@
     source.startsWith(Symbol.open) ||
     source.startsWith(Symbol.open_decoded))
 
-  def is_begin: Boolean = is_keyword && source == "begin"
-  def is_end: Boolean = is_command && source == "end"
+  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(_))
 
-  // FIXME avoid hard-wired stuff
-  def is_command_modifier: Boolean =
-    is_keyword && (source == "public" || source == "private" || source == "qualified")
+  def is_begin: Boolean = is_keyword("begin")
+  def is_end: Boolean = is_command("end")
 
   def content: String =
     if (kind == Token.Kind.STRING) Scan.Parsers.quoted_content("\"", source)
diff -r 6b82bad2277f -r 932a3d470264 src/Pure/Pure.thy
--- a/src/Pure/Pure.thy	Mon Jul 11 21:02:26 2016 +0200
+++ b/src/Pure/Pure.thy	Mon Jul 11 22:07:02 2016 +0200
@@ -8,10 +8,10 @@
 keywords
     "!!" "!" "+" "--" ":" ";" "<" "<=" "=" "=>" "?" "[" "\<comment>" "\<equiv>" "\<leftharpoondown>" "\<rightharpoonup>" "\<rightleftharpoons>"
     "\<subseteq>" "]" "attach" "binder" "for" "if" "in" "infix" "infixl" "infixr" "is"
-    "open" "output" "overloaded" "pervasive" "premises" "private" "qualified"
-    "structure" "unchecked" "where" "when" "|"
+    "open" "output" "overloaded" "pervasive" "premises" "structure" "unchecked" "when"
+  and "private" "qualified" :: before_command
   and "assumes" "constrains" "defines" "fixes" "includes" "notes" "rewrites"
-    "obtains" "shows" :: quasi_command
+    "obtains" "shows" "where" "|" :: quasi_command
   and "text" "txt" :: document_body
   and "text_raw" :: document_raw
   and "default_sort" :: thy_decl == ""
diff -r 6b82bad2277f -r 932a3d470264 src/Pure/System/options.scala
--- a/src/Pure/System/options.scala	Mon Jul 11 21:02:26 2016 +0200
+++ b/src/Pure/System/options.scala	Mon Jul 11 22:07:02 2016 +0200
@@ -76,7 +76,9 @@
 
   lazy val options_syntax =
     Outer_Syntax.init() + ":" + "=" + "--" + Symbol.comment + Symbol.comment_decoded +
-      (SECTION, Keyword.DOCUMENT_HEADING) + PUBLIC + (OPTION, Keyword.THY_DECL)
+      (SECTION, Keyword.DOCUMENT_HEADING) +
+      (PUBLIC, Keyword.BEFORE_COMMAND) +
+      (OPTION, Keyword.THY_DECL)
 
   lazy val prefs_syntax = Outer_Syntax.init() + "="
 
diff -r 6b82bad2277f -r 932a3d470264 src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Mon Jul 11 21:02:26 2016 +0200
+++ b/src/Pure/Thy/sessions.scala	Mon Jul 11 22:07:02 2016 +0200
@@ -163,9 +163,15 @@
   private val DOCUMENT_FILES = "document_files"
 
   lazy val root_syntax =
-    Outer_Syntax.init() + "(" + ")" + "+" + "," + "=" + "[" + "]" +
-      (CHAPTER, Keyword.THY_DECL) + (SESSION, Keyword.THY_DECL) +
-      IN + DESCRIPTION + OPTIONS + GLOBAL_THEORIES + THEORIES + FILES + DOCUMENT_FILES
+    Outer_Syntax.init() + "(" + ")" + "+" + "," + "=" + "[" + "]" + IN +
+      (CHAPTER, Keyword.THY_DECL) +
+      (SESSION, Keyword.THY_DECL) +
+      (DESCRIPTION, Keyword.QUASI_COMMAND) +
+      (OPTIONS, Keyword.QUASI_COMMAND) +
+      (GLOBAL_THEORIES, Keyword.QUASI_COMMAND) +
+      (THEORIES, Keyword.QUASI_COMMAND) +
+      (FILES, Keyword.QUASI_COMMAND) +
+      (DOCUMENT_FILES, Keyword.QUASI_COMMAND)
 
   private object Parser extends Parse.Parser with Options.Parser
   {
diff -r 6b82bad2277f -r 932a3d470264 src/Pure/Thy/thy_header.ML
--- a/src/Pure/Thy/thy_header.ML	Mon Jul 11 21:02:26 2016 +0200
+++ b/src/Pure/Thy/thy_header.ML	Mon Jul 11 22:07:02 2016 +0200
@@ -70,9 +70,9 @@
      (("::", @{here}), Keyword.no_spec),
      (("==", @{here}), Keyword.no_spec),
      (("and", @{here}), Keyword.no_spec),
-     ((beginN, @{here}), Keyword.no_spec),
-     ((importsN, @{here}), Keyword.no_spec),
-     ((keywordsN, @{here}), Keyword.no_spec),
+     ((beginN, @{here}), Keyword.quasi_command_spec),
+     ((importsN, @{here}), Keyword.quasi_command_spec),
+     ((keywordsN, @{here}), Keyword.quasi_command_spec),
      ((chapterN, @{here}), ((Keyword.document_heading, []), [])),
      ((sectionN, @{here}), ((Keyword.document_heading, []), [])),
      ((subsectionN, @{here}), ((Keyword.document_heading, []), [])),
diff -r 6b82bad2277f -r 932a3d470264 src/Pure/Thy/thy_header.scala
--- a/src/Pure/Thy/thy_header.scala	Mon Jul 11 21:02:26 2016 +0200
+++ b/src/Pure/Thy/thy_header.scala	Mon Jul 11 22:07:02 2016 +0200
@@ -44,9 +44,9 @@
       ("::", Keyword.no_spec, None),
       ("==", Keyword.no_spec, None),
       (AND, Keyword.no_spec, None),
-      (BEGIN, Keyword.no_spec, None),
-      (IMPORTS, Keyword.no_spec, None),
-      (KEYWORDS, Keyword.no_spec, None),
+      (BEGIN, Keyword.quasi_command_spec, None),
+      (IMPORTS, Keyword.quasi_command_spec, None),
+      (KEYWORDS, Keyword.quasi_command_spec, None),
       (CHAPTER, (((Keyword.DOCUMENT_HEADING, Nil), Nil)), None),
       (SECTION, (((Keyword.DOCUMENT_HEADING, Nil), Nil)), None),
       (SUBSECTION, (((Keyword.DOCUMENT_HEADING, Nil), Nil)), None),
diff -r 6b82bad2277f -r 932a3d470264 src/Tools/jEdit/src/document_model.scala
--- a/src/Tools/jEdit/src/document_model.scala	Mon Jul 11 21:02:26 2016 +0200
+++ b/src/Tools/jEdit/src/document_model.scala	Mon Jul 11 22:07:02 2016 +0200
@@ -96,8 +96,7 @@
           Token_Markup.line_token_iterator(
             Thy_Header.bootstrap_syntax, buffer, 0, buffer.getLineCount).collectFirst(
               {
-                case Text.Info(range, tok)
-                if tok.is_command && tok.source == Thy_Header.THEORY => range.start
+                case Text.Info(range, tok) if tok.is_command(Thy_Header.THEORY) => range.start
               })
             match {
               case Some(offset) =>
diff -r 6b82bad2277f -r 932a3d470264 src/Tools/jEdit/src/isabelle.scala
--- a/src/Tools/jEdit/src/isabelle.scala	Mon Jul 11 21:02:26 2016 +0200
+++ b/src/Tools/jEdit/src/isabelle.scala	Mon Jul 11 22:07:02 2016 +0200
@@ -87,7 +87,11 @@
   /* text structure */
 
   def indent_rule(mode: String): Option[IndentRule] =
-    if (mode == "isabelle") Some(Text_Structure.Indent_Rule) else None
+    mode match {
+      case "isabelle" | "isabelle-options" | "isabelle-root" =>
+        Some(Text_Structure.Indent_Rule)
+      case _ => None
+    }
 
   def structure_matchers(mode: String): List[StructureMatcher] =
     if (mode == "isabelle") List(Text_Structure.Matcher) else Nil
diff -r 6b82bad2277f -r 932a3d470264 src/Tools/jEdit/src/rendering.scala
--- a/src/Tools/jEdit/src/rendering.scala	Mon Jul 11 21:02:26 2016 +0200
+++ b/src/Tools/jEdit/src/rendering.scala	Mon Jul 11 22:07:02 2016 +0200
@@ -93,7 +93,7 @@
   }
 
   def token_markup(syntax: Outer_Syntax, token: Token): Byte =
-    if (token.is_command) command_style(syntax.keywords.command_kind(token.content).getOrElse(""))
+    if (token.is_command) command_style(syntax.keywords.kinds.getOrElse(token.content, ""))
     else if (token.is_keyword && token.source == Symbol.comment_decoded) JEditToken.NULL
     else if (token.is_delimiter) JEditToken.OPERATOR
     else token_style(token.kind)
diff -r 6b82bad2277f -r 932a3d470264 src/Tools/jEdit/src/text_structure.scala
--- a/src/Tools/jEdit/src/text_structure.scala	Mon Jul 11 21:02:26 2016 +0200
+++ b/src/Tools/jEdit/src/text_structure.scala	Mon Jul 11 22:07:02 2016 +0200
@@ -19,17 +19,21 @@
 {
   /* token navigator */
 
-  class Navigator(syntax: Outer_Syntax, buffer: Buffer)
+  class Navigator(syntax: Outer_Syntax, buffer: Buffer, comments: Boolean)
   {
     val limit = PIDE.options.value.int("jedit_structure_limit") max 0
 
     def iterator(line: Int, lim: Int = limit): Iterator[Text.Info[Token]] =
-      Token_Markup.line_token_iterator(syntax, buffer, line, line + lim).
-        filter(_.info.is_proper)
+    {
+      val it = Token_Markup.line_token_iterator(syntax, buffer, line, line + lim)
+      if (comments) it.filterNot(_.info.is_space) else it.filter(_.info.is_proper)
+    }
 
     def reverse_iterator(line: Int, lim: Int = limit): Iterator[Text.Info[Token]] =
-      Token_Markup.line_token_reverse_iterator(syntax, buffer, line, line - lim).
-        filter(_.info.is_proper)
+    {
+      val it = Token_Markup.line_token_reverse_iterator(syntax, buffer, line, line - lim)
+      if (comments) it.filterNot(_.info.is_space) else it.filter(_.info.is_proper)
+    }
   }
 
 
@@ -46,7 +50,7 @@
       Isabelle.buffer_syntax(buffer) match {
         case Some(syntax) if buffer.isInstanceOf[Buffer] =>
           val keywords = syntax.keywords
-          val nav = new Navigator(syntax, buffer.asInstanceOf[Buffer])
+          val nav = new Navigator(syntax, buffer.asInstanceOf[Buffer], true)
 
           def head_token(line: Int): Option[Token] =
             nav.iterator(line, 1).toStream.headOption.map(_.info)
@@ -64,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
@@ -77,9 +84,16 @@
             else 0
 
           def indent_offset(tok: Token): Int =
-            if (keywords.is_command(tok, Keyword.proof_enclose)) indent_size
+            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
@@ -97,12 +111,20 @@
                   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 None => indent_structure + indent_brackets + 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_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 {
                     case None =>
@@ -112,16 +134,16 @@
                           case (true, false) => - indent_extra
                           case (false, true) => indent_extra
                         }
-                      line_indent(prev_line) + extra
+                      line_indent(prev_line) - indent_offset(tok) + indent_brackets + extra
                     case Some(prev_tok) =>
-                      indent_structure - 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
                   }
                }
             }
 
           actions.clear()
-          actions.add(new IndentAction.AlignOffset(indent))
+          actions.add(new IndentAction.AlignOffset(indent max 0))
         case _ =>
       }
     }
@@ -160,7 +182,7 @@
         case Some(syntax) if buffer.isInstanceOf[Buffer] =>
           val keywords = syntax.keywords
 
-          val nav = new Navigator(syntax, buffer.asInstanceOf[Buffer])
+          val nav = new Navigator(syntax, buffer.asInstanceOf[Buffer], false)
 
           def caret_iterator(): Iterator[Text.Info[Token]] =
             nav.iterator(caret_line).dropWhile(info => !info.range.touches(caret))
diff -r 6b82bad2277f -r 932a3d470264 src/Tools/jEdit/src/token_markup.scala
--- a/src/Tools/jEdit/src/token_markup.scala	Mon Jul 11 21:02:26 2016 +0200
+++ b/src/Tools/jEdit/src/token_markup.scala	Mon Jul 11 22:07:02 2016 +0200
@@ -175,22 +175,23 @@
 
   /* line context */
 
-  private val context_rules = new ParserRuleSet("isabelle", "MAIN")
-
   object Line_Context
   {
-    val init = new Line_Context(Some(Scan.Finished), Outer_Syntax.Line_Structure.init)
+    def init(mode: String): Line_Context =
+      new Line_Context(mode, Some(Scan.Finished), Outer_Syntax.Line_Structure.init)
   }
 
   class Line_Context(
+      val mode: String,
       val context: Option[Scan.Line_Context],
       val structure: Outer_Syntax.Line_Structure)
-    extends TokenMarker.LineContext(context_rules, null)
+    extends TokenMarker.LineContext(new ParserRuleSet(mode, "MAIN"), null)
   {
-    override def hashCode: Int = (context, structure).hashCode
+    override def hashCode: Int = (mode, context, structure).hashCode
     override def equals(that: Any): Boolean =
       that match {
-        case other: Line_Context => context == other.context && structure == other.structure
+        case other: Line_Context =>
+          mode == other.mode && context == other.context && structure == other.structure
         case _ => false
       }
   }
@@ -205,7 +206,7 @@
       }
     context getOrElse {
       buffer.markTokens(line, DummyTokenHandler.INSTANCE)
-      context getOrElse Line_Context.init
+      context getOrElse Line_Context.init(JEdit_Lib.buffer_mode(buffer))
     }
   }
 
@@ -216,7 +217,7 @@
     : Option[List[Token]] =
   {
     val line_context =
-      if (line == 0) Line_Context.init
+      if (line == 0) Line_Context.init(JEdit_Lib.buffer_mode(buffer))
       else buffer_line_context(buffer, line - 1)
     for {
       ctxt <- line_context.context
@@ -275,13 +276,15 @@
   def command_span(syntax: Outer_Syntax, buffer: JEditBuffer, offset: Text.Offset)
     : Option[Text.Info[Command_Span.Span]] =
   {
+    val keywords = syntax.keywords
+
     def maybe_command_start(i: Text.Offset): Option[Text.Info[Token]] =
       token_reverse_iterator(syntax, buffer, i).
-        find(info => info.info.is_command_modifier || info.info.is_command)
+        find(info => keywords.is_before_command(info.info) || info.info.is_command)
 
     def maybe_command_stop(i: Text.Offset): Option[Text.Info[Token]] =
       token_iterator(syntax, buffer, i).
-        find(info => info.info.is_command_modifier || info.info.is_command)
+        find(info => keywords.is_before_command(info.info) || info.info.is_command)
 
     if (JEdit_Lib.buffer_range(buffer).contains(offset)) {
       val start_info =
@@ -291,15 +294,16 @@
           case Some(Text.Info(range1, tok1)) if tok1.is_command =>
             val info2 = maybe_command_start(range1.start - 1)
             info2 match {
-              case Some(Text.Info(_, tok2)) if tok2.is_command_modifier => info2
+              case Some(Text.Info(_, tok2)) if keywords.is_before_command(tok2) => info2
               case _ => info1
             }
           case _ => info1
         }
       }
-      val (start_is_command_modifier, start, start_next) =
+      val (start_before_command, start, start_next) =
         start_info match {
-          case Some(Text.Info(range, tok)) => (tok.is_command_modifier, range.start, range.stop)
+          case Some(Text.Info(range, tok)) =>
+            (keywords.is_before_command(tok), range.start, range.stop)
           case None => (false, 0, 0)
         }
 
@@ -307,7 +311,7 @@
       {
         val info1 = maybe_command_stop(start_next)
         info1 match {
-          case Some(Text.Info(range1, tok1)) if tok1.is_command && start_is_command_modifier =>
+          case Some(Text.Info(range1, tok1)) if tok1.is_command && start_before_command =>
             maybe_command_stop(range1.stop)
           case _ => info1
         }
@@ -378,7 +382,8 @@
         handler: TokenHandler, raw_line: Segment): TokenMarker.LineContext =
     {
       val line = if (raw_line == null) new Segment else raw_line
-      val line_context = context match { case c: Line_Context => c case _ => Line_Context.init }
+      val line_context =
+        context match { case c: Line_Context => c case _ => Line_Context.init(mode) }
       val structure = line_context.structure
 
       val context1 =
@@ -393,18 +398,18 @@
             case (Some(ctxt), _) if mode == "isabelle-ml" || mode == "sml" =>
               val (tokens, ctxt1) = ML_Lex.tokenize_line(mode == "sml", line, ctxt)
               val styled_tokens = tokens.map(tok => (Rendering.ml_token_markup(tok), tok.source))
-              (styled_tokens, new Line_Context(Some(ctxt1), structure))
+              (styled_tokens, new Line_Context(line_context.mode, Some(ctxt1), structure))
 
             case (Some(ctxt), Some(syntax)) if syntax.has_tokens =>
               val (tokens, ctxt1) = Token.explode_line(syntax.keywords, line, ctxt)
               val structure1 = syntax.line_structure(tokens, structure)
               val styled_tokens =
                 tokens.map(tok => (Rendering.token_markup(syntax, tok), tok.source))
-              (styled_tokens, new Line_Context(Some(ctxt1), structure1))
+              (styled_tokens, new Line_Context(line_context.mode, Some(ctxt1), structure1))
 
             case _ =>
               val styled_token = (JEditToken.NULL, line.subSequence(0, line.count).toString)
-              (List(styled_token), new Line_Context(None, structure))
+              (List(styled_token), new Line_Context(line_context.mode, None, structure))
           }
 
         val extended = extended_styles(line)