# HG changeset patch
# User wenzelm
# Date 1468009371 -7200
# Node ID 005b490f0ce2e31a330b2e128d40a6a4ceed0b30
# Parent  88d62f8b5f6e0b2e9ce4d609331de6fcb182ea42
indentation in reminiscence to Proof General (see proof-indent.el);

diff -r 88d62f8b5f6e -r 005b490f0ce2 src/Pure/Isar/keyword.scala
--- a/src/Pure/Isar/keyword.scala	Fri Jul 08 09:50:53 2016 +0200
+++ b/src/Pure/Isar/keyword.scala	Fri Jul 08 22:22:51 2016 +0200
@@ -80,6 +80,7 @@
 
   val proof_open = proof_goal + PRF_OPEN
   val proof_close = qed + PRF_CLOSE
+  val proof_enclose = Set(PRF_BLOCK, NEXT_BLOCK, QED_BLOCK, PRF_CLOSE)
 
 
 
diff -r 88d62f8b5f6e -r 005b490f0ce2 src/Tools/jEdit/src/text_structure.scala
--- a/src/Tools/jEdit/src/text_structure.scala	Fri Jul 08 09:50:53 2016 +0200
+++ b/src/Tools/jEdit/src/text_structure.scala	Fri Jul 08 22:22:51 2016 +0200
@@ -37,7 +37,10 @@
 
   object Indent_Rule extends IndentRule
   {
-    def apply(buffer: JEditBuffer, line: Int, prev_line: Int, prev_prev_line: Int,
+    private val keyword_open = Keyword.theory_goal ++ Keyword.proof_open
+    private val keyword_close = Keyword.proof_close
+
+    def apply(buffer: JEditBuffer, current_line: Int, prev_line: Int, prev_prev_line: Int,
       actions: java.util.List[IndentAction])
     {
       Isabelle.buffer_syntax(buffer) match {
@@ -45,7 +48,55 @@
           val keywords = syntax.keywords
           val nav = new Navigator(syntax, buffer.asInstanceOf[Buffer])
 
-          val indent = 0  // FIXME
+          def head_token(line: Int): Option[Token] =
+            nav.iterator(line, 1).toStream.headOption.map(_.info)
+
+          def prev_command: Option[Token] =
+            nav.reverse_iterator(prev_line, 1).
+              collectFirst({ case Text.Info(_, tok) if tok.is_command => tok })
+
+          def line_indent(line: Int): Int =
+            if (line < 0 || line >= buffer.getLineCount) 0
+            else buffer.getCurrentIndentForLine(line, null)
+
+          val indent_size = buffer.getIndentSize
+
+          def indent_indent(tok: Token): Int =
+            if (keywords.is_command(tok, keyword_open)) indent_size
+            else if (keywords.is_command(tok, keyword_close)) - indent_size
+            else 0
+
+          def indent_offset(tok: Token): Int =
+            if (keywords.is_command(tok, Keyword.proof_enclose)) indent_size
+            else 0
+
+          def indent_structure: Int =
+            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) {
+                    val line = buffer.getLineOfOffset(range.start)
+                    if (head_token(line) == Some(tok))
+                      (ind1 + indent_offset(tok) + line_indent(line), true)
+                    else (ind1, false)
+                  }
+                  else (ind1, false)
+              }).collectFirst({ case (i, true) => i }).getOrElse(0)
+
+          val indent =
+            head_token(current_line) match {
+              case Some(tok) if tok.is_command =>
+                if (keywords.is_command(tok, Keyword.theory)) 0
+                else indent_structure - indent_offset(tok)
+              case _ =>
+                if (nav.iterator(current_line, 1).isEmpty) indent_structure
+                else
+                  prev_command match {
+                    case Some(tok) =>
+                      indent_structure - indent_offset(tok) - indent_indent(tok) + indent_size
+                    case None => line_indent(prev_line)
+                  }
+            }
 
           actions.clear()
           actions.add(new IndentAction.AlignOffset(indent))