src/Tools/jEdit/src/text_structure.scala
author wenzelm
Sun, 04 Dec 2016 13:47:56 +0100
changeset 64536 e61de633a3ed
parent 64518 b87697eec2ac
child 64621 7116f2634e32
permissions -rw-r--r--
more uniform indentation of new line, even if it is empty (relevant for non-proof commands, e.g. 'definition', 'context');
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
63422
5cf8dd98a717 clarified modules;
wenzelm
parents: 59122
diff changeset
     1
/*  Title:      Tools/jEdit/src/text_structure.scala
58748
8f92f17d8781 support for structure matching;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
8f92f17d8781 support for structure matching;
wenzelm
parents:
diff changeset
     3
63422
5cf8dd98a717 clarified modules;
wenzelm
parents: 59122
diff changeset
     4
Text structure based on Isabelle/Isar outer syntax.
58748
8f92f17d8781 support for structure matching;
wenzelm
parents:
diff changeset
     5
*/
8f92f17d8781 support for structure matching;
wenzelm
parents:
diff changeset
     6
8f92f17d8781 support for structure matching;
wenzelm
parents:
diff changeset
     7
package isabelle.jedit
8f92f17d8781 support for structure matching;
wenzelm
parents:
diff changeset
     8
8f92f17d8781 support for structure matching;
wenzelm
parents:
diff changeset
     9
8f92f17d8781 support for structure matching;
wenzelm
parents:
diff changeset
    10
import isabelle._
8f92f17d8781 support for structure matching;
wenzelm
parents:
diff changeset
    11
63422
5cf8dd98a717 clarified modules;
wenzelm
parents: 59122
diff changeset
    12
import org.gjt.sp.jedit.indent.{IndentRule, IndentAction}
58803
7a0f675eb671 proper selectMatch, e.g. relevant for S-click on gutter;
wenzelm
parents: 58800
diff changeset
    13
import org.gjt.sp.jedit.textarea.{TextArea, StructureMatcher, Selection}
63422
5cf8dd98a717 clarified modules;
wenzelm
parents: 59122
diff changeset
    14
import org.gjt.sp.jedit.buffer.JEditBuffer
63423
ed65a6d9929b more operations;
wenzelm
parents: 63422
diff changeset
    15
import org.gjt.sp.jedit.Buffer
58748
8f92f17d8781 support for structure matching;
wenzelm
parents:
diff changeset
    16
8f92f17d8781 support for structure matching;
wenzelm
parents:
diff changeset
    17
63422
5cf8dd98a717 clarified modules;
wenzelm
parents: 59122
diff changeset
    18
object Text_Structure
58748
8f92f17d8781 support for structure matching;
wenzelm
parents:
diff changeset
    19
{
63425
wenzelm
parents: 63424
diff changeset
    20
  /* token navigator */
wenzelm
parents: 63424
diff changeset
    21
63447
55b1bed86c44 proper filter;
wenzelm
parents: 63446
diff changeset
    22
  class Navigator(syntax: Outer_Syntax, buffer: Buffer, comments: Boolean)
63425
wenzelm
parents: 63424
diff changeset
    23
  {
wenzelm
parents: 63424
diff changeset
    24
    val limit = PIDE.options.value.int("jedit_structure_limit") max 0
wenzelm
parents: 63424
diff changeset
    25
wenzelm
parents: 63424
diff changeset
    26
    def iterator(line: Int, lim: Int = limit): Iterator[Text.Info[Token]] =
63445
5761bb8592dc observe comments in indentation, but not in fold structure;
wenzelm
parents: 63442
diff changeset
    27
    {
5761bb8592dc observe comments in indentation, but not in fold structure;
wenzelm
parents: 63442
diff changeset
    28
      val it = Token_Markup.line_token_iterator(syntax, buffer, line, line + lim)
63480
wenzelm
parents: 63479
diff changeset
    29
      if (comments) it.filterNot(_.info.is_space) else it.filterNot(_.info.is_improper)
63445
5761bb8592dc observe comments in indentation, but not in fold structure;
wenzelm
parents: 63442
diff changeset
    30
    }
63425
wenzelm
parents: 63424
diff changeset
    31
63427
wenzelm
parents: 63425
diff changeset
    32
    def reverse_iterator(line: Int, lim: Int = limit): Iterator[Text.Info[Token]] =
63445
5761bb8592dc observe comments in indentation, but not in fold structure;
wenzelm
parents: 63442
diff changeset
    33
    {
5761bb8592dc observe comments in indentation, but not in fold structure;
wenzelm
parents: 63442
diff changeset
    34
      val it = Token_Markup.line_token_reverse_iterator(syntax, buffer, line, line - lim)
63480
wenzelm
parents: 63479
diff changeset
    35
      if (comments) it.filterNot(_.info.is_space) else it.filterNot(_.info.is_improper)
63445
5761bb8592dc observe comments in indentation, but not in fold structure;
wenzelm
parents: 63442
diff changeset
    36
    }
63425
wenzelm
parents: 63424
diff changeset
    37
  }
wenzelm
parents: 63424
diff changeset
    38
wenzelm
parents: 63424
diff changeset
    39
63422
5cf8dd98a717 clarified modules;
wenzelm
parents: 59122
diff changeset
    40
  /* indentation */
5cf8dd98a717 clarified modules;
wenzelm
parents: 59122
diff changeset
    41
5cf8dd98a717 clarified modules;
wenzelm
parents: 59122
diff changeset
    42
  object Indent_Rule extends IndentRule
5cf8dd98a717 clarified modules;
wenzelm
parents: 59122
diff changeset
    43
  {
63428
005b490f0ce2 indentation in reminiscence to Proof General (see proof-indent.el);
wenzelm
parents: 63427
diff changeset
    44
    private val keyword_open = Keyword.theory_goal ++ Keyword.proof_open
005b490f0ce2 indentation in reminiscence to Proof General (see proof-indent.el);
wenzelm
parents: 63427
diff changeset
    45
    private val keyword_close = Keyword.proof_close
005b490f0ce2 indentation in reminiscence to Proof General (see proof-indent.el);
wenzelm
parents: 63427
diff changeset
    46
64518
b87697eec2ac skip over inner syntax for indentation;
wenzelm
parents: 63483
diff changeset
    47
    def apply(buffer: JEditBuffer, current_line: Int, prev_line0: Int, prev_prev_line0: Int,
63422
5cf8dd98a717 clarified modules;
wenzelm
parents: 59122
diff changeset
    48
      actions: java.util.List[IndentAction])
5cf8dd98a717 clarified modules;
wenzelm
parents: 59122
diff changeset
    49
    {
63425
wenzelm
parents: 63424
diff changeset
    50
      Isabelle.buffer_syntax(buffer) match {
wenzelm
parents: 63424
diff changeset
    51
        case Some(syntax) if buffer.isInstanceOf[Buffer] =>
wenzelm
parents: 63424
diff changeset
    52
          val keywords = syntax.keywords
63445
5761bb8592dc observe comments in indentation, but not in fold structure;
wenzelm
parents: 63442
diff changeset
    53
          val nav = new Navigator(syntax, buffer.asInstanceOf[Buffer], true)
63422
5cf8dd98a717 clarified modules;
wenzelm
parents: 59122
diff changeset
    54
63474
f66e3c3b0fb1 semantic indentation for unstructured proof scripts;
wenzelm
parents: 63450
diff changeset
    55
          val indent_size = buffer.getIndentSize
f66e3c3b0fb1 semantic indentation for unstructured proof scripts;
wenzelm
parents: 63450
diff changeset
    56
f66e3c3b0fb1 semantic indentation for unstructured proof scripts;
wenzelm
parents: 63450
diff changeset
    57
f66e3c3b0fb1 semantic indentation for unstructured proof scripts;
wenzelm
parents: 63450
diff changeset
    58
          def line_indent(line: Int): Int =
f66e3c3b0fb1 semantic indentation for unstructured proof scripts;
wenzelm
parents: 63450
diff changeset
    59
            if (line < 0 || line >= buffer.getLineCount) 0
f66e3c3b0fb1 semantic indentation for unstructured proof scripts;
wenzelm
parents: 63450
diff changeset
    60
            else buffer.getCurrentIndentForLine(line, null)
f66e3c3b0fb1 semantic indentation for unstructured proof scripts;
wenzelm
parents: 63450
diff changeset
    61
f66e3c3b0fb1 semantic indentation for unstructured proof scripts;
wenzelm
parents: 63450
diff changeset
    62
          def line_head(line: Int): Option[Text.Info[Token]] =
f66e3c3b0fb1 semantic indentation for unstructured proof scripts;
wenzelm
parents: 63450
diff changeset
    63
            nav.iterator(line, 1).toStream.headOption
63428
005b490f0ce2 indentation in reminiscence to Proof General (see proof-indent.el);
wenzelm
parents: 63427
diff changeset
    64
63434
c956d995bec6 more indentation for quasi_command keywords;
wenzelm
parents: 63431
diff changeset
    65
          def head_is_quasi_command(line: Int): Boolean =
63474
f66e3c3b0fb1 semantic indentation for unstructured proof scripts;
wenzelm
parents: 63450
diff changeset
    66
            line_head(line) match {
63434
c956d995bec6 more indentation for quasi_command keywords;
wenzelm
parents: 63431
diff changeset
    67
              case None => false
63474
f66e3c3b0fb1 semantic indentation for unstructured proof scripts;
wenzelm
parents: 63450
diff changeset
    68
              case Some(Text.Info(_, tok)) => keywords.is_quasi_command(tok)
63434
c956d995bec6 more indentation for quasi_command keywords;
wenzelm
parents: 63431
diff changeset
    69
            }
c956d995bec6 more indentation for quasi_command keywords;
wenzelm
parents: 63431
diff changeset
    70
64518
b87697eec2ac skip over inner syntax for indentation;
wenzelm
parents: 63483
diff changeset
    71
          val prev_line: Int =
b87697eec2ac skip over inner syntax for indentation;
wenzelm
parents: 63483
diff changeset
    72
            Range.inclusive(current_line - 1, 0, -1).find(line =>
b87697eec2ac skip over inner syntax for indentation;
wenzelm
parents: 63483
diff changeset
    73
              Token_Markup.Line_Context.prev(buffer, line).get_context == Scan.Finished &&
b87697eec2ac skip over inner syntax for indentation;
wenzelm
parents: 63483
diff changeset
    74
              !Token_Markup.Line_Context.next(buffer, line).structure.improper) getOrElse -1
b87697eec2ac skip over inner syntax for indentation;
wenzelm
parents: 63483
diff changeset
    75
63477
f5c81436b930 clarified indentation: 'begin' is treated like a separate command without indent;
wenzelm
parents: 63474
diff changeset
    76
          def prev_line_command: Option[Token] =
63428
005b490f0ce2 indentation in reminiscence to Proof General (see proof-indent.el);
wenzelm
parents: 63427
diff changeset
    77
            nav.reverse_iterator(prev_line, 1).
63477
f5c81436b930 clarified indentation: 'begin' is treated like a separate command without indent;
wenzelm
parents: 63474
diff changeset
    78
              collectFirst({ case Text.Info(_, tok) if tok.is_begin_or_command => tok })
f5c81436b930 clarified indentation: 'begin' is treated like a separate command without indent;
wenzelm
parents: 63474
diff changeset
    79
f5c81436b930 clarified indentation: 'begin' is treated like a separate command without indent;
wenzelm
parents: 63474
diff changeset
    80
          def prev_line_span: Iterator[Token] =
f5c81436b930 clarified indentation: 'begin' is treated like a separate command without indent;
wenzelm
parents: 63474
diff changeset
    81
            nav.reverse_iterator(prev_line, 1).map(_.info).takeWhile(tok => !tok.is_begin_or_command)
63428
005b490f0ce2 indentation in reminiscence to Proof General (see proof-indent.el);
wenzelm
parents: 63427
diff changeset
    82
63434
c956d995bec6 more indentation for quasi_command keywords;
wenzelm
parents: 63431
diff changeset
    83
          def prev_span: Iterator[Token] =
63477
f5c81436b930 clarified indentation: 'begin' is treated like a separate command without indent;
wenzelm
parents: 63474
diff changeset
    84
            nav.reverse_iterator(prev_line).map(_.info).takeWhile(tok => !tok.is_begin_or_command)
63450
afd657fffdf9 indentation of brackets;
wenzelm
parents: 63447
diff changeset
    85
63434
c956d995bec6 more indentation for quasi_command keywords;
wenzelm
parents: 63431
diff changeset
    86
63481
wenzelm
parents: 63480
diff changeset
    87
          val script_indent: Text.Info[Token] => Int =
63474
f66e3c3b0fb1 semantic indentation for unstructured proof scripts;
wenzelm
parents: 63450
diff changeset
    88
          {
f66e3c3b0fb1 semantic indentation for unstructured proof scripts;
wenzelm
parents: 63450
diff changeset
    89
            val opt_rendering: Option[Rendering] =
f66e3c3b0fb1 semantic indentation for unstructured proof scripts;
wenzelm
parents: 63450
diff changeset
    90
              if (PIDE.options.value.bool("jedit_indent_script"))
f66e3c3b0fb1 semantic indentation for unstructured proof scripts;
wenzelm
parents: 63450
diff changeset
    91
                GUI_Thread.now {
f66e3c3b0fb1 semantic indentation for unstructured proof scripts;
wenzelm
parents: 63450
diff changeset
    92
                  (for {
f66e3c3b0fb1 semantic indentation for unstructured proof scripts;
wenzelm
parents: 63450
diff changeset
    93
                    text_area <- JEdit_Lib.jedit_text_areas(buffer)
f66e3c3b0fb1 semantic indentation for unstructured proof scripts;
wenzelm
parents: 63450
diff changeset
    94
                    doc_view <- PIDE.document_view(text_area)
f66e3c3b0fb1 semantic indentation for unstructured proof scripts;
wenzelm
parents: 63450
diff changeset
    95
                  } yield doc_view.get_rendering).toStream.headOption
f66e3c3b0fb1 semantic indentation for unstructured proof scripts;
wenzelm
parents: 63450
diff changeset
    96
                }
f66e3c3b0fb1 semantic indentation for unstructured proof scripts;
wenzelm
parents: 63450
diff changeset
    97
              else None
f66e3c3b0fb1 semantic indentation for unstructured proof scripts;
wenzelm
parents: 63450
diff changeset
    98
            val limit = PIDE.options.value.int("jedit_indent_script_limit")
63481
wenzelm
parents: 63480
diff changeset
    99
            (info: Text.Info[Token]) =>
63474
f66e3c3b0fb1 semantic indentation for unstructured proof scripts;
wenzelm
parents: 63450
diff changeset
   100
              opt_rendering match {
63481
wenzelm
parents: 63480
diff changeset
   101
                case Some(rendering) if keywords.is_command(info.info, Keyword.prf_script) =>
wenzelm
parents: 63480
diff changeset
   102
                  (rendering.indentation(info.range) min limit) max 0
wenzelm
parents: 63480
diff changeset
   103
                case _ => 0
63474
f66e3c3b0fb1 semantic indentation for unstructured proof scripts;
wenzelm
parents: 63450
diff changeset
   104
              }
f66e3c3b0fb1 semantic indentation for unstructured proof scripts;
wenzelm
parents: 63450
diff changeset
   105
          }
63428
005b490f0ce2 indentation in reminiscence to Proof General (see proof-indent.el);
wenzelm
parents: 63427
diff changeset
   106
005b490f0ce2 indentation in reminiscence to Proof General (see proof-indent.el);
wenzelm
parents: 63427
diff changeset
   107
          def indent_indent(tok: Token): Int =
005b490f0ce2 indentation in reminiscence to Proof General (see proof-indent.el);
wenzelm
parents: 63427
diff changeset
   108
            if (keywords.is_command(tok, keyword_open)) indent_size
005b490f0ce2 indentation in reminiscence to Proof General (see proof-indent.el);
wenzelm
parents: 63427
diff changeset
   109
            else if (keywords.is_command(tok, keyword_close)) - indent_size
005b490f0ce2 indentation in reminiscence to Proof General (see proof-indent.el);
wenzelm
parents: 63427
diff changeset
   110
            else 0
005b490f0ce2 indentation in reminiscence to Proof General (see proof-indent.el);
wenzelm
parents: 63427
diff changeset
   111
005b490f0ce2 indentation in reminiscence to Proof General (see proof-indent.el);
wenzelm
parents: 63427
diff changeset
   112
          def indent_offset(tok: Token): Int =
63477
f5c81436b930 clarified indentation: 'begin' is treated like a separate command without indent;
wenzelm
parents: 63474
diff changeset
   113
            if (keywords.is_command(tok, Keyword.proof_enclose)) indent_size
63428
005b490f0ce2 indentation in reminiscence to Proof General (see proof-indent.el);
wenzelm
parents: 63427
diff changeset
   114
            else 0
005b490f0ce2 indentation in reminiscence to Proof General (see proof-indent.el);
wenzelm
parents: 63427
diff changeset
   115
005b490f0ce2 indentation in reminiscence to Proof General (see proof-indent.el);
wenzelm
parents: 63427
diff changeset
   116
          def indent_structure: Int =
005b490f0ce2 indentation in reminiscence to Proof General (see proof-indent.el);
wenzelm
parents: 63427
diff changeset
   117
            nav.reverse_iterator(current_line - 1).scanLeft((0, false))(
005b490f0ce2 indentation in reminiscence to Proof General (see proof-indent.el);
wenzelm
parents: 63427
diff changeset
   118
              { case ((ind, _), Text.Info(range, tok)) =>
005b490f0ce2 indentation in reminiscence to Proof General (see proof-indent.el);
wenzelm
parents: 63427
diff changeset
   119
                  val ind1 = ind + indent_indent(tok)
63479
wenzelm
parents: 63478
diff changeset
   120
                  if (tok.is_begin_or_command && !keywords.is_command(tok, Keyword.prf_script)) {
63428
005b490f0ce2 indentation in reminiscence to Proof General (see proof-indent.el);
wenzelm
parents: 63427
diff changeset
   121
                    val line = buffer.getLineOfOffset(range.start)
63474
f66e3c3b0fb1 semantic indentation for unstructured proof scripts;
wenzelm
parents: 63450
diff changeset
   122
                    line_head(line) match {
f66e3c3b0fb1 semantic indentation for unstructured proof scripts;
wenzelm
parents: 63450
diff changeset
   123
                      case Some(info) if info.info == tok =>
f66e3c3b0fb1 semantic indentation for unstructured proof scripts;
wenzelm
parents: 63450
diff changeset
   124
                        (ind1 + indent_offset(tok) + line_indent(line), true)
f66e3c3b0fb1 semantic indentation for unstructured proof scripts;
wenzelm
parents: 63450
diff changeset
   125
                      case _ => (ind1, false)
f66e3c3b0fb1 semantic indentation for unstructured proof scripts;
wenzelm
parents: 63450
diff changeset
   126
                    }
63428
005b490f0ce2 indentation in reminiscence to Proof General (see proof-indent.el);
wenzelm
parents: 63427
diff changeset
   127
                  }
005b490f0ce2 indentation in reminiscence to Proof General (see proof-indent.el);
wenzelm
parents: 63427
diff changeset
   128
                  else (ind1, false)
005b490f0ce2 indentation in reminiscence to Proof General (see proof-indent.el);
wenzelm
parents: 63427
diff changeset
   129
              }).collectFirst({ case (i, true) => i }).getOrElse(0)
005b490f0ce2 indentation in reminiscence to Proof General (see proof-indent.el);
wenzelm
parents: 63427
diff changeset
   130
63480
wenzelm
parents: 63479
diff changeset
   131
          def indent_brackets: Int =
wenzelm
parents: 63479
diff changeset
   132
            (0 /: prev_line_span)(
wenzelm
parents: 63479
diff changeset
   133
              { case (i, tok) =>
wenzelm
parents: 63479
diff changeset
   134
                  if (tok.is_open_bracket) i + indent_size
wenzelm
parents: 63479
diff changeset
   135
                  else if (tok.is_close_bracket) i - indent_size
wenzelm
parents: 63479
diff changeset
   136
                  else i })
wenzelm
parents: 63479
diff changeset
   137
wenzelm
parents: 63479
diff changeset
   138
          def indent_extra: Int =
wenzelm
parents: 63479
diff changeset
   139
            if (prev_span.exists(keywords.is_quasi_command(_))) indent_size
wenzelm
parents: 63479
diff changeset
   140
            else 0
wenzelm
parents: 63479
diff changeset
   141
63428
005b490f0ce2 indentation in reminiscence to Proof General (see proof-indent.el);
wenzelm
parents: 63427
diff changeset
   142
          val indent =
64518
b87697eec2ac skip over inner syntax for indentation;
wenzelm
parents: 63483
diff changeset
   143
            if (Token_Markup.Line_Context.prev(buffer, current_line).get_context == Scan.Finished) {
b87697eec2ac skip over inner syntax for indentation;
wenzelm
parents: 63483
diff changeset
   144
              line_head(current_line) match {
b87697eec2ac skip over inner syntax for indentation;
wenzelm
parents: 63483
diff changeset
   145
                case Some(info @ Text.Info(range, tok)) =>
b87697eec2ac skip over inner syntax for indentation;
wenzelm
parents: 63483
diff changeset
   146
                  if (tok.is_begin ||
b87697eec2ac skip over inner syntax for indentation;
wenzelm
parents: 63483
diff changeset
   147
                      keywords.is_before_command(tok) ||
b87697eec2ac skip over inner syntax for indentation;
wenzelm
parents: 63483
diff changeset
   148
                      keywords.is_command(tok, Keyword.theory)) 0
b87697eec2ac skip over inner syntax for indentation;
wenzelm
parents: 63483
diff changeset
   149
                  else if (keywords.is_command(tok, Keyword.proof_enclose))
b87697eec2ac skip over inner syntax for indentation;
wenzelm
parents: 63483
diff changeset
   150
                    indent_structure + script_indent(info) - indent_offset(tok)
b87697eec2ac skip over inner syntax for indentation;
wenzelm
parents: 63483
diff changeset
   151
                  else if (keywords.is_command(tok, Keyword.proof))
b87697eec2ac skip over inner syntax for indentation;
wenzelm
parents: 63483
diff changeset
   152
                    (indent_structure + script_indent(info) - indent_offset(tok)) max indent_size
b87697eec2ac skip over inner syntax for indentation;
wenzelm
parents: 63483
diff changeset
   153
                  else if (tok.is_command) indent_structure - indent_offset(tok)
b87697eec2ac skip over inner syntax for indentation;
wenzelm
parents: 63483
diff changeset
   154
                  else {
b87697eec2ac skip over inner syntax for indentation;
wenzelm
parents: 63483
diff changeset
   155
                    prev_line_command match {
b87697eec2ac skip over inner syntax for indentation;
wenzelm
parents: 63483
diff changeset
   156
                      case None =>
b87697eec2ac skip over inner syntax for indentation;
wenzelm
parents: 63483
diff changeset
   157
                        val extra =
b87697eec2ac skip over inner syntax for indentation;
wenzelm
parents: 63483
diff changeset
   158
                          (keywords.is_quasi_command(tok), head_is_quasi_command(prev_line)) match {
b87697eec2ac skip over inner syntax for indentation;
wenzelm
parents: 63483
diff changeset
   159
                            case (true, true) | (false, false) => 0
b87697eec2ac skip over inner syntax for indentation;
wenzelm
parents: 63483
diff changeset
   160
                            case (true, false) => - indent_extra
b87697eec2ac skip over inner syntax for indentation;
wenzelm
parents: 63483
diff changeset
   161
                            case (false, true) => indent_extra
b87697eec2ac skip over inner syntax for indentation;
wenzelm
parents: 63483
diff changeset
   162
                          }
b87697eec2ac skip over inner syntax for indentation;
wenzelm
parents: 63483
diff changeset
   163
                        line_indent(prev_line) + indent_brackets + extra - indent_offset(tok)
b87697eec2ac skip over inner syntax for indentation;
wenzelm
parents: 63483
diff changeset
   164
                      case Some(prev_tok) =>
b87697eec2ac skip over inner syntax for indentation;
wenzelm
parents: 63483
diff changeset
   165
                        indent_structure + indent_brackets + indent_size - indent_offset(tok) -
b87697eec2ac skip over inner syntax for indentation;
wenzelm
parents: 63483
diff changeset
   166
                        indent_offset(prev_tok) - indent_indent(prev_tok)
b87697eec2ac skip over inner syntax for indentation;
wenzelm
parents: 63483
diff changeset
   167
                    }
64536
e61de633a3ed more uniform indentation of new line, even if it is empty (relevant for non-proof commands, e.g. 'definition', 'context');
wenzelm
parents: 64518
diff changeset
   168
                  }
e61de633a3ed more uniform indentation of new line, even if it is empty (relevant for non-proof commands, e.g. 'definition', 'context');
wenzelm
parents: 64518
diff changeset
   169
                case None =>
e61de633a3ed more uniform indentation of new line, even if it is empty (relevant for non-proof commands, e.g. 'definition', 'context');
wenzelm
parents: 64518
diff changeset
   170
                  prev_line_command match {
e61de633a3ed more uniform indentation of new line, even if it is empty (relevant for non-proof commands, e.g. 'definition', 'context');
wenzelm
parents: 64518
diff changeset
   171
                    case None =>
e61de633a3ed more uniform indentation of new line, even if it is empty (relevant for non-proof commands, e.g. 'definition', 'context');
wenzelm
parents: 64518
diff changeset
   172
                      val extra = if (head_is_quasi_command(prev_line)) indent_extra else 0
e61de633a3ed more uniform indentation of new line, even if it is empty (relevant for non-proof commands, e.g. 'definition', 'context');
wenzelm
parents: 64518
diff changeset
   173
                      line_indent(prev_line) + indent_brackets + extra
e61de633a3ed more uniform indentation of new line, even if it is empty (relevant for non-proof commands, e.g. 'definition', 'context');
wenzelm
parents: 64518
diff changeset
   174
                    case Some(prev_tok) =>
e61de633a3ed more uniform indentation of new line, even if it is empty (relevant for non-proof commands, e.g. 'definition', 'context');
wenzelm
parents: 64518
diff changeset
   175
                      indent_structure + indent_brackets + indent_size -
e61de633a3ed more uniform indentation of new line, even if it is empty (relevant for non-proof commands, e.g. 'definition', 'context');
wenzelm
parents: 64518
diff changeset
   176
                      indent_offset(prev_tok) - indent_indent(prev_tok)
e61de633a3ed more uniform indentation of new line, even if it is empty (relevant for non-proof commands, e.g. 'definition', 'context');
wenzelm
parents: 64518
diff changeset
   177
                  }
64518
b87697eec2ac skip over inner syntax for indentation;
wenzelm
parents: 63483
diff changeset
   178
              }
63428
005b490f0ce2 indentation in reminiscence to Proof General (see proof-indent.el);
wenzelm
parents: 63427
diff changeset
   179
            }
64518
b87697eec2ac skip over inner syntax for indentation;
wenzelm
parents: 63483
diff changeset
   180
            else line_indent(current_line)
63423
ed65a6d9929b more operations;
wenzelm
parents: 63422
diff changeset
   181
63425
wenzelm
parents: 63424
diff changeset
   182
          actions.clear()
63439
5ad98525e918 more robust;
wenzelm
parents: 63434
diff changeset
   183
          actions.add(new IndentAction.AlignOffset(indent max 0))
63423
ed65a6d9929b more operations;
wenzelm
parents: 63422
diff changeset
   184
        case _ =>
ed65a6d9929b more operations;
wenzelm
parents: 63422
diff changeset
   185
      }
63422
5cf8dd98a717 clarified modules;
wenzelm
parents: 59122
diff changeset
   186
    }
5cf8dd98a717 clarified modules;
wenzelm
parents: 59122
diff changeset
   187
  }
5cf8dd98a717 clarified modules;
wenzelm
parents: 59122
diff changeset
   188
5cf8dd98a717 clarified modules;
wenzelm
parents: 59122
diff changeset
   189
5cf8dd98a717 clarified modules;
wenzelm
parents: 59122
diff changeset
   190
  /* structure matching */
5cf8dd98a717 clarified modules;
wenzelm
parents: 59122
diff changeset
   191
5cf8dd98a717 clarified modules;
wenzelm
parents: 59122
diff changeset
   192
  object Matcher extends StructureMatcher
58748
8f92f17d8781 support for structure matching;
wenzelm
parents:
diff changeset
   193
  {
58803
7a0f675eb671 proper selectMatch, e.g. relevant for S-click on gutter;
wenzelm
parents: 58800
diff changeset
   194
    private def find_block(
58752
2077bc9558cf support for begin/end matching;
wenzelm
parents: 58750
diff changeset
   195
      open: Token => Boolean,
2077bc9558cf support for begin/end matching;
wenzelm
parents: 58750
diff changeset
   196
      close: Token => Boolean,
2077bc9558cf support for begin/end matching;
wenzelm
parents: 58750
diff changeset
   197
      reset: Token => Boolean,
58762
4fedc5d4b2fe restricted scanning;
wenzelm
parents: 58756
diff changeset
   198
      restrict: Token => Boolean,
58754
wenzelm
parents: 58752
diff changeset
   199
      it: Iterator[Text.Info[Token]]): Option[(Text.Range, Text.Range)] =
58752
2077bc9558cf support for begin/end matching;
wenzelm
parents: 58750
diff changeset
   200
    {
58754
wenzelm
parents: 58752
diff changeset
   201
      val range1 = it.next.range
58762
4fedc5d4b2fe restricted scanning;
wenzelm
parents: 58756
diff changeset
   202
      it.takeWhile(info => !info.info.is_command || restrict(info.info)).
4fedc5d4b2fe restricted scanning;
wenzelm
parents: 58756
diff changeset
   203
        scanLeft((range1, 1))(
4fedc5d4b2fe restricted scanning;
wenzelm
parents: 58756
diff changeset
   204
          { case ((r, d), Text.Info(range, tok)) =>
4fedc5d4b2fe restricted scanning;
wenzelm
parents: 58756
diff changeset
   205
              if (open(tok)) (range, d + 1)
4fedc5d4b2fe restricted scanning;
wenzelm
parents: 58756
diff changeset
   206
              else if (close(tok)) (range, d - 1)
4fedc5d4b2fe restricted scanning;
wenzelm
parents: 58756
diff changeset
   207
              else if (reset(tok)) (range, 0)
4fedc5d4b2fe restricted scanning;
wenzelm
parents: 58756
diff changeset
   208
              else (r, d) }
4fedc5d4b2fe restricted scanning;
wenzelm
parents: 58756
diff changeset
   209
        ).collectFirst({ case (range2, 0) => (range1, range2) })
58752
2077bc9558cf support for begin/end matching;
wenzelm
parents: 58750
diff changeset
   210
    }
2077bc9558cf support for begin/end matching;
wenzelm
parents: 58750
diff changeset
   211
58803
7a0f675eb671 proper selectMatch, e.g. relevant for S-click on gutter;
wenzelm
parents: 58800
diff changeset
   212
    private def find_pair(text_area: TextArea): Option[(Text.Range, Text.Range)] =
58748
8f92f17d8781 support for structure matching;
wenzelm
parents:
diff changeset
   213
    {
8f92f17d8781 support for structure matching;
wenzelm
parents:
diff changeset
   214
      val buffer = text_area.getBuffer
8f92f17d8781 support for structure matching;
wenzelm
parents:
diff changeset
   215
      val caret_line = text_area.getCaretLine
58749
83b0f633190e some structure matching, based on line token iterators;
wenzelm
parents: 58748
diff changeset
   216
      val caret = text_area.getCaretPosition
58748
8f92f17d8781 support for structure matching;
wenzelm
parents:
diff changeset
   217
59074
7836d927ffca tuned signature;
wenzelm
parents: 58901
diff changeset
   218
      Isabelle.buffer_syntax(text_area.getBuffer) match {
63425
wenzelm
parents: 63424
diff changeset
   219
        case Some(syntax) if buffer.isInstanceOf[Buffer] =>
63424
e4e15bbfb3e2 clarified signature;
wenzelm
parents: 63423
diff changeset
   220
          val keywords = syntax.keywords
58750
1b4b005d73c1 added option jedit_structure_limit;
wenzelm
parents: 58749
diff changeset
   221
63445
5761bb8592dc observe comments in indentation, but not in fold structure;
wenzelm
parents: 63442
diff changeset
   222
          val nav = new Navigator(syntax, buffer.asInstanceOf[Buffer], false)
58750
1b4b005d73c1 added option jedit_structure_limit;
wenzelm
parents: 58749
diff changeset
   223
58752
2077bc9558cf support for begin/end matching;
wenzelm
parents: 58750
diff changeset
   224
          def caret_iterator(): Iterator[Text.Info[Token]] =
63425
wenzelm
parents: 63424
diff changeset
   225
            nav.iterator(caret_line).dropWhile(info => !info.range.touches(caret))
58752
2077bc9558cf support for begin/end matching;
wenzelm
parents: 58750
diff changeset
   226
63427
wenzelm
parents: 63425
diff changeset
   227
          def reverse_caret_iterator(): Iterator[Text.Info[Token]] =
wenzelm
parents: 63425
diff changeset
   228
            nav.reverse_iterator(caret_line).dropWhile(info => !info.range.touches(caret))
58752
2077bc9558cf support for begin/end matching;
wenzelm
parents: 58750
diff changeset
   229
63425
wenzelm
parents: 63424
diff changeset
   230
          nav.iterator(caret_line, 1).find(info => info.range.touches(caret))
58756
eb5d0c58564d ignore improper tokens to avoid ambiguity of Range.touches (assuming that relevant tokens are separated properly);
wenzelm
parents: 58755
diff changeset
   231
          match {
63424
e4e15bbfb3e2 clarified signature;
wenzelm
parents: 63423
diff changeset
   232
            case Some(Text.Info(range1, tok)) if keywords.is_command(tok, Keyword.theory_goal) =>
58755
fc822ca2428a support for proof structure matching;
wenzelm
parents: 58754
diff changeset
   233
              find_block(
63424
e4e15bbfb3e2 clarified signature;
wenzelm
parents: 63423
diff changeset
   234
                keywords.is_command(_, Keyword.proof_goal),
e4e15bbfb3e2 clarified signature;
wenzelm
parents: 63423
diff changeset
   235
                keywords.is_command(_, Keyword.qed),
e4e15bbfb3e2 clarified signature;
wenzelm
parents: 63423
diff changeset
   236
                keywords.is_command(_, Keyword.qed_global),
58762
4fedc5d4b2fe restricted scanning;
wenzelm
parents: 58756
diff changeset
   237
                t =>
63424
e4e15bbfb3e2 clarified signature;
wenzelm
parents: 63423
diff changeset
   238
                  keywords.is_command(t, Keyword.diag) ||
e4e15bbfb3e2 clarified signature;
wenzelm
parents: 63423
diff changeset
   239
                  keywords.is_command(t, Keyword.proof),
58755
fc822ca2428a support for proof structure matching;
wenzelm
parents: 58754
diff changeset
   240
                caret_iterator())
fc822ca2428a support for proof structure matching;
wenzelm
parents: 58754
diff changeset
   241
63424
e4e15bbfb3e2 clarified signature;
wenzelm
parents: 63423
diff changeset
   242
            case Some(Text.Info(range1, tok)) if keywords.is_command(tok, Keyword.proof_goal) =>
58755
fc822ca2428a support for proof structure matching;
wenzelm
parents: 58754
diff changeset
   243
              find_block(
63424
e4e15bbfb3e2 clarified signature;
wenzelm
parents: 63423
diff changeset
   244
                keywords.is_command(_, Keyword.proof_goal),
e4e15bbfb3e2 clarified signature;
wenzelm
parents: 63423
diff changeset
   245
                keywords.is_command(_, Keyword.qed),
58755
fc822ca2428a support for proof structure matching;
wenzelm
parents: 58754
diff changeset
   246
                _ => false,
58762
4fedc5d4b2fe restricted scanning;
wenzelm
parents: 58756
diff changeset
   247
                t =>
63424
e4e15bbfb3e2 clarified signature;
wenzelm
parents: 63423
diff changeset
   248
                  keywords.is_command(t, Keyword.diag) ||
e4e15bbfb3e2 clarified signature;
wenzelm
parents: 63423
diff changeset
   249
                  keywords.is_command(t, Keyword.proof),
58755
fc822ca2428a support for proof structure matching;
wenzelm
parents: 58754
diff changeset
   250
                caret_iterator())
fc822ca2428a support for proof structure matching;
wenzelm
parents: 58754
diff changeset
   251
63424
e4e15bbfb3e2 clarified signature;
wenzelm
parents: 63423
diff changeset
   252
            case Some(Text.Info(range1, tok)) if keywords.is_command(tok, Keyword.qed_global) =>
63427
wenzelm
parents: 63425
diff changeset
   253
              reverse_caret_iterator().find(info => keywords.is_command(info.info, Keyword.theory))
58749
83b0f633190e some structure matching, based on line token iterators;
wenzelm
parents: 58748
diff changeset
   254
              match {
58750
1b4b005d73c1 added option jedit_structure_limit;
wenzelm
parents: 58749
diff changeset
   255
                case Some(Text.Info(range2, tok))
63424
e4e15bbfb3e2 clarified signature;
wenzelm
parents: 63423
diff changeset
   256
                if keywords.is_command(tok, Keyword.theory_goal) => Some((range1, range2))
58749
83b0f633190e some structure matching, based on line token iterators;
wenzelm
parents: 58748
diff changeset
   257
                case _ => None
83b0f633190e some structure matching, based on line token iterators;
wenzelm
parents: 58748
diff changeset
   258
              }
58752
2077bc9558cf support for begin/end matching;
wenzelm
parents: 58750
diff changeset
   259
63424
e4e15bbfb3e2 clarified signature;
wenzelm
parents: 63423
diff changeset
   260
            case Some(Text.Info(range1, tok)) if keywords.is_command(tok, Keyword.qed) =>
58755
fc822ca2428a support for proof structure matching;
wenzelm
parents: 58754
diff changeset
   261
              find_block(
63424
e4e15bbfb3e2 clarified signature;
wenzelm
parents: 63423
diff changeset
   262
                keywords.is_command(_, Keyword.qed),
58755
fc822ca2428a support for proof structure matching;
wenzelm
parents: 58754
diff changeset
   263
                t =>
63424
e4e15bbfb3e2 clarified signature;
wenzelm
parents: 63423
diff changeset
   264
                  keywords.is_command(t, Keyword.proof_goal) ||
e4e15bbfb3e2 clarified signature;
wenzelm
parents: 63423
diff changeset
   265
                  keywords.is_command(t, Keyword.theory_goal),
58755
fc822ca2428a support for proof structure matching;
wenzelm
parents: 58754
diff changeset
   266
                _ => false,
58762
4fedc5d4b2fe restricted scanning;
wenzelm
parents: 58756
diff changeset
   267
                t =>
63424
e4e15bbfb3e2 clarified signature;
wenzelm
parents: 63423
diff changeset
   268
                  keywords.is_command(t, Keyword.diag) ||
e4e15bbfb3e2 clarified signature;
wenzelm
parents: 63423
diff changeset
   269
                  keywords.is_command(t, Keyword.proof) ||
e4e15bbfb3e2 clarified signature;
wenzelm
parents: 63423
diff changeset
   270
                  keywords.is_command(t, Keyword.theory_goal),
63427
wenzelm
parents: 63425
diff changeset
   271
                reverse_caret_iterator())
58755
fc822ca2428a support for proof structure matching;
wenzelm
parents: 58754
diff changeset
   272
58752
2077bc9558cf support for begin/end matching;
wenzelm
parents: 58750
diff changeset
   273
            case Some(Text.Info(range1, tok)) if tok.is_begin =>
58762
4fedc5d4b2fe restricted scanning;
wenzelm
parents: 58756
diff changeset
   274
              find_block(_.is_begin, _.is_end, _ => false, _ => true, caret_iterator())
58752
2077bc9558cf support for begin/end matching;
wenzelm
parents: 58750
diff changeset
   275
2077bc9558cf support for begin/end matching;
wenzelm
parents: 58750
diff changeset
   276
            case Some(Text.Info(range1, tok)) if tok.is_end =>
63427
wenzelm
parents: 63425
diff changeset
   277
              find_block(_.is_end, _.is_begin, _ => false, _ => true, reverse_caret_iterator())
58763
1b943a82d5ed find main command keyword of 'begin';
wenzelm
parents: 58762
diff changeset
   278
              match {
1b943a82d5ed find main command keyword of 'begin';
wenzelm
parents: 58762
diff changeset
   279
                case Some((_, range2)) =>
63427
wenzelm
parents: 63425
diff changeset
   280
                  reverse_caret_iterator().
58800
bfed1c26caed explicit keyword category for commands that may start a block;
wenzelm
parents: 58763
diff changeset
   281
                    dropWhile(info => info.range != range2).
bfed1c26caed explicit keyword category for commands that may start a block;
wenzelm
parents: 58763
diff changeset
   282
                    dropWhile(info => info.range == range2).
bfed1c26caed explicit keyword category for commands that may start a block;
wenzelm
parents: 58763
diff changeset
   283
                    find(info => info.info.is_command || info.info.is_begin)
58763
1b943a82d5ed find main command keyword of 'begin';
wenzelm
parents: 58762
diff changeset
   284
                  match {
58800
bfed1c26caed explicit keyword category for commands that may start a block;
wenzelm
parents: 58763
diff changeset
   285
                    case Some(Text.Info(range3, tok)) =>
63424
e4e15bbfb3e2 clarified signature;
wenzelm
parents: 63423
diff changeset
   286
                      if (keywords.is_command(tok, Keyword.theory_block)) Some((range1, range3))
58800
bfed1c26caed explicit keyword category for commands that may start a block;
wenzelm
parents: 58763
diff changeset
   287
                      else Some((range1, range2))
58763
1b943a82d5ed find main command keyword of 'begin';
wenzelm
parents: 58762
diff changeset
   288
                    case None => None
1b943a82d5ed find main command keyword of 'begin';
wenzelm
parents: 58762
diff changeset
   289
                  }
1b943a82d5ed find main command keyword of 'begin';
wenzelm
parents: 58762
diff changeset
   290
                case None => None
1b943a82d5ed find main command keyword of 'begin';
wenzelm
parents: 58762
diff changeset
   291
              }
58752
2077bc9558cf support for begin/end matching;
wenzelm
parents: 58750
diff changeset
   292
58749
83b0f633190e some structure matching, based on line token iterators;
wenzelm
parents: 58748
diff changeset
   293
            case _ => None
58748
8f92f17d8781 support for structure matching;
wenzelm
parents:
diff changeset
   294
          }
63425
wenzelm
parents: 63424
diff changeset
   295
        case _ => None
58748
8f92f17d8781 support for structure matching;
wenzelm
parents:
diff changeset
   296
      }
8f92f17d8781 support for structure matching;
wenzelm
parents:
diff changeset
   297
    }
8f92f17d8781 support for structure matching;
wenzelm
parents:
diff changeset
   298
58749
83b0f633190e some structure matching, based on line token iterators;
wenzelm
parents: 58748
diff changeset
   299
    def getMatch(text_area: TextArea): StructureMatcher.Match =
83b0f633190e some structure matching, based on line token iterators;
wenzelm
parents: 58748
diff changeset
   300
      find_pair(text_area) match {
83b0f633190e some structure matching, based on line token iterators;
wenzelm
parents: 58748
diff changeset
   301
        case Some((_, range)) =>
83b0f633190e some structure matching, based on line token iterators;
wenzelm
parents: 58748
diff changeset
   302
          val line = text_area.getBuffer.getLineOfOffset(range.start)
63422
5cf8dd98a717 clarified modules;
wenzelm
parents: 59122
diff changeset
   303
          new StructureMatcher.Match(Matcher, line, range.start, line, range.stop)
58749
83b0f633190e some structure matching, based on line token iterators;
wenzelm
parents: 58748
diff changeset
   304
        case None => null
83b0f633190e some structure matching, based on line token iterators;
wenzelm
parents: 58748
diff changeset
   305
      }
83b0f633190e some structure matching, based on line token iterators;
wenzelm
parents: 58748
diff changeset
   306
58748
8f92f17d8781 support for structure matching;
wenzelm
parents:
diff changeset
   307
    def selectMatch(text_area: TextArea)
8f92f17d8781 support for structure matching;
wenzelm
parents:
diff changeset
   308
    {
58803
7a0f675eb671 proper selectMatch, e.g. relevant for S-click on gutter;
wenzelm
parents: 58800
diff changeset
   309
      def get_span(offset: Text.Offset): Option[Text.Range] =
7a0f675eb671 proper selectMatch, e.g. relevant for S-click on gutter;
wenzelm
parents: 58800
diff changeset
   310
        for {
59074
7836d927ffca tuned signature;
wenzelm
parents: 58901
diff changeset
   311
          syntax <- Isabelle.buffer_syntax(text_area.getBuffer)
58803
7a0f675eb671 proper selectMatch, e.g. relevant for S-click on gutter;
wenzelm
parents: 58800
diff changeset
   312
          span <- Token_Markup.command_span(syntax, text_area.getBuffer, offset)
7a0f675eb671 proper selectMatch, e.g. relevant for S-click on gutter;
wenzelm
parents: 58800
diff changeset
   313
        } yield span.range
7a0f675eb671 proper selectMatch, e.g. relevant for S-click on gutter;
wenzelm
parents: 58800
diff changeset
   314
7a0f675eb671 proper selectMatch, e.g. relevant for S-click on gutter;
wenzelm
parents: 58800
diff changeset
   315
      find_pair(text_area) match {
7a0f675eb671 proper selectMatch, e.g. relevant for S-click on gutter;
wenzelm
parents: 58800
diff changeset
   316
        case Some((r1, r2)) =>
7a0f675eb671 proper selectMatch, e.g. relevant for S-click on gutter;
wenzelm
parents: 58800
diff changeset
   317
          (get_span(r1.start), get_span(r2.start)) match {
7a0f675eb671 proper selectMatch, e.g. relevant for S-click on gutter;
wenzelm
parents: 58800
diff changeset
   318
            case (Some(range1), Some(range2)) =>
7a0f675eb671 proper selectMatch, e.g. relevant for S-click on gutter;
wenzelm
parents: 58800
diff changeset
   319
              val start = range1.start min range2.start
7a0f675eb671 proper selectMatch, e.g. relevant for S-click on gutter;
wenzelm
parents: 58800
diff changeset
   320
              val stop = range1.stop max range2.stop
7a0f675eb671 proper selectMatch, e.g. relevant for S-click on gutter;
wenzelm
parents: 58800
diff changeset
   321
7a0f675eb671 proper selectMatch, e.g. relevant for S-click on gutter;
wenzelm
parents: 58800
diff changeset
   322
              text_area.moveCaretPosition(stop, false)
7a0f675eb671 proper selectMatch, e.g. relevant for S-click on gutter;
wenzelm
parents: 58800
diff changeset
   323
              if (!text_area.isMultipleSelectionEnabled) text_area.selectNone
7a0f675eb671 proper selectMatch, e.g. relevant for S-click on gutter;
wenzelm
parents: 58800
diff changeset
   324
              text_area.addToSelection(new Selection.Range(start, stop))
7a0f675eb671 proper selectMatch, e.g. relevant for S-click on gutter;
wenzelm
parents: 58800
diff changeset
   325
            case _ =>
7a0f675eb671 proper selectMatch, e.g. relevant for S-click on gutter;
wenzelm
parents: 58800
diff changeset
   326
          }
7a0f675eb671 proper selectMatch, e.g. relevant for S-click on gutter;
wenzelm
parents: 58800
diff changeset
   327
        case None =>
7a0f675eb671 proper selectMatch, e.g. relevant for S-click on gutter;
wenzelm
parents: 58800
diff changeset
   328
      }
58748
8f92f17d8781 support for structure matching;
wenzelm
parents:
diff changeset
   329
    }
8f92f17d8781 support for structure matching;
wenzelm
parents:
diff changeset
   330
  }
8f92f17d8781 support for structure matching;
wenzelm
parents:
diff changeset
   331
}