indentation in reminiscence to Proof General (see proof-indent.el);
authorwenzelm
Fri Jul 08 22:22:51 2016 +0200 (2016-07-08)
changeset 63428005b490f0ce2
parent 63427 88d62f8b5f6e
child 63429 baedd4724f08
indentation in reminiscence to Proof General (see proof-indent.el);
src/Pure/Isar/keyword.scala
src/Tools/jEdit/src/text_structure.scala
     1.1 --- a/src/Pure/Isar/keyword.scala	Fri Jul 08 09:50:53 2016 +0200
     1.2 +++ b/src/Pure/Isar/keyword.scala	Fri Jul 08 22:22:51 2016 +0200
     1.3 @@ -80,6 +80,7 @@
     1.4  
     1.5    val proof_open = proof_goal + PRF_OPEN
     1.6    val proof_close = qed + PRF_CLOSE
     1.7 +  val proof_enclose = Set(PRF_BLOCK, NEXT_BLOCK, QED_BLOCK, PRF_CLOSE)
     1.8  
     1.9  
    1.10  
     2.1 --- a/src/Tools/jEdit/src/text_structure.scala	Fri Jul 08 09:50:53 2016 +0200
     2.2 +++ b/src/Tools/jEdit/src/text_structure.scala	Fri Jul 08 22:22:51 2016 +0200
     2.3 @@ -37,7 +37,10 @@
     2.4  
     2.5    object Indent_Rule extends IndentRule
     2.6    {
     2.7 -    def apply(buffer: JEditBuffer, line: Int, prev_line: Int, prev_prev_line: Int,
     2.8 +    private val keyword_open = Keyword.theory_goal ++ Keyword.proof_open
     2.9 +    private val keyword_close = Keyword.proof_close
    2.10 +
    2.11 +    def apply(buffer: JEditBuffer, current_line: Int, prev_line: Int, prev_prev_line: Int,
    2.12        actions: java.util.List[IndentAction])
    2.13      {
    2.14        Isabelle.buffer_syntax(buffer) match {
    2.15 @@ -45,7 +48,55 @@
    2.16            val keywords = syntax.keywords
    2.17            val nav = new Navigator(syntax, buffer.asInstanceOf[Buffer])
    2.18  
    2.19 -          val indent = 0  // FIXME
    2.20 +          def head_token(line: Int): Option[Token] =
    2.21 +            nav.iterator(line, 1).toStream.headOption.map(_.info)
    2.22 +
    2.23 +          def prev_command: Option[Token] =
    2.24 +            nav.reverse_iterator(prev_line, 1).
    2.25 +              collectFirst({ case Text.Info(_, tok) if tok.is_command => tok })
    2.26 +
    2.27 +          def line_indent(line: Int): Int =
    2.28 +            if (line < 0 || line >= buffer.getLineCount) 0
    2.29 +            else buffer.getCurrentIndentForLine(line, null)
    2.30 +
    2.31 +          val indent_size = buffer.getIndentSize
    2.32 +
    2.33 +          def indent_indent(tok: Token): Int =
    2.34 +            if (keywords.is_command(tok, keyword_open)) indent_size
    2.35 +            else if (keywords.is_command(tok, keyword_close)) - indent_size
    2.36 +            else 0
    2.37 +
    2.38 +          def indent_offset(tok: Token): Int =
    2.39 +            if (keywords.is_command(tok, Keyword.proof_enclose)) indent_size
    2.40 +            else 0
    2.41 +
    2.42 +          def indent_structure: Int =
    2.43 +            nav.reverse_iterator(current_line - 1).scanLeft((0, false))(
    2.44 +              { case ((ind, _), Text.Info(range, tok)) =>
    2.45 +                  val ind1 = ind + indent_indent(tok)
    2.46 +                  if (tok.is_command) {
    2.47 +                    val line = buffer.getLineOfOffset(range.start)
    2.48 +                    if (head_token(line) == Some(tok))
    2.49 +                      (ind1 + indent_offset(tok) + line_indent(line), true)
    2.50 +                    else (ind1, false)
    2.51 +                  }
    2.52 +                  else (ind1, false)
    2.53 +              }).collectFirst({ case (i, true) => i }).getOrElse(0)
    2.54 +
    2.55 +          val indent =
    2.56 +            head_token(current_line) match {
    2.57 +              case Some(tok) if tok.is_command =>
    2.58 +                if (keywords.is_command(tok, Keyword.theory)) 0
    2.59 +                else indent_structure - indent_offset(tok)
    2.60 +              case _ =>
    2.61 +                if (nav.iterator(current_line, 1).isEmpty) indent_structure
    2.62 +                else
    2.63 +                  prev_command match {
    2.64 +                    case Some(tok) =>
    2.65 +                      indent_structure - indent_offset(tok) - indent_indent(tok) + indent_size
    2.66 +                    case None => line_indent(prev_line)
    2.67 +                  }
    2.68 +            }
    2.69  
    2.70            actions.clear()
    2.71            actions.add(new IndentAction.AlignOffset(indent))