src/Tools/jEdit/src/text_structure.scala
author wenzelm
Mon Jan 09 20:26:59 2017 +0100 (2017-01-09)
changeset 64854 f5aa712e6250
parent 64621 7116f2634e32
child 64882 c3b42ac0cf81
permissions -rw-r--r--
tuned signature;
     1 /*  Title:      Tools/jEdit/src/text_structure.scala
     2     Author:     Makarius
     3 
     4 Text structure based on Isabelle/Isar outer syntax.
     5 */
     6 
     7 package isabelle.jedit
     8 
     9 
    10 import isabelle._
    11 
    12 import org.gjt.sp.jedit.indent.{IndentRule, IndentAction}
    13 import org.gjt.sp.jedit.textarea.{TextArea, StructureMatcher, Selection}
    14 import org.gjt.sp.jedit.buffer.JEditBuffer
    15 import org.gjt.sp.jedit.Buffer
    16 
    17 
    18 object Text_Structure
    19 {
    20   /* token navigator */
    21 
    22   class Navigator(syntax: Outer_Syntax, buffer: Buffer, comments: Boolean)
    23   {
    24     val limit = PIDE.options.value.int("jedit_structure_limit") max 0
    25 
    26     def iterator(line: Int, lim: Int = limit): Iterator[Text.Info[Token]] =
    27     {
    28       val it = Token_Markup.line_token_iterator(syntax, buffer, line, line + lim)
    29       if (comments) it.filterNot(_.info.is_space) else it.filterNot(_.info.is_improper)
    30     }
    31 
    32     def reverse_iterator(line: Int, lim: Int = limit): Iterator[Text.Info[Token]] =
    33     {
    34       val it = Token_Markup.line_token_reverse_iterator(syntax, buffer, line, line - lim)
    35       if (comments) it.filterNot(_.info.is_space) else it.filterNot(_.info.is_improper)
    36     }
    37   }
    38 
    39 
    40   /* indentation */
    41 
    42   object Indent_Rule extends IndentRule
    43   {
    44     private val keyword_open = Keyword.theory_goal ++ Keyword.proof_open
    45     private val keyword_close = Keyword.proof_close
    46 
    47     def apply(buffer: JEditBuffer, current_line: Int, prev_line0: Int, prev_prev_line0: Int,
    48       actions: java.util.List[IndentAction])
    49     {
    50       Isabelle.buffer_syntax(buffer) match {
    51         case Some(syntax) if buffer.isInstanceOf[Buffer] =>
    52           val keywords = syntax.keywords
    53           val nav = new Navigator(syntax, buffer.asInstanceOf[Buffer], true)
    54 
    55           val indent_size = buffer.getIndentSize
    56 
    57 
    58           def line_indent(line: Int): Int =
    59             if (line < 0 || line >= buffer.getLineCount) 0
    60             else buffer.getCurrentIndentForLine(line, null)
    61 
    62           def line_head(line: Int): Option[Text.Info[Token]] =
    63             nav.iterator(line, 1).toStream.headOption
    64 
    65           def head_is_quasi_command(line: Int): Boolean =
    66             line_head(line) match {
    67               case None => false
    68               case Some(Text.Info(_, tok)) => keywords.is_quasi_command(tok)
    69             }
    70 
    71           val prev_line: Int =
    72             Range.inclusive(current_line - 1, 0, -1).find(line =>
    73               Token_Markup.Line_Context.prev(buffer, line).get_context == Scan.Finished &&
    74               !Token_Markup.Line_Context.next(buffer, line).structure.improper) getOrElse -1
    75 
    76           def prev_line_command: Option[Token] =
    77             nav.reverse_iterator(prev_line, 1).
    78               collectFirst({ case Text.Info(_, tok) if tok.is_begin_or_command => tok })
    79 
    80           def prev_line_span: Iterator[Token] =
    81             nav.reverse_iterator(prev_line, 1).map(_.info).takeWhile(tok => !tok.is_begin_or_command)
    82 
    83           def prev_span: Iterator[Token] =
    84             nav.reverse_iterator(prev_line).map(_.info).takeWhile(tok => !tok.is_begin_or_command)
    85 
    86 
    87           val script_indent: Text.Info[Token] => Int =
    88           {
    89             val opt_rendering: Option[JEdit_Rendering] =
    90               if (PIDE.options.value.bool("jedit_indent_script"))
    91                 GUI_Thread.now {
    92                   (for {
    93                     text_area <- JEdit_Lib.jedit_text_areas(buffer)
    94                     doc_view <- PIDE.document_view(text_area)
    95                   } yield doc_view.get_rendering).toStream.headOption
    96                 }
    97               else None
    98             val limit = PIDE.options.value.int("jedit_indent_script_limit")
    99             (info: Text.Info[Token]) =>
   100               opt_rendering match {
   101                 case Some(rendering) if keywords.is_command(info.info, Keyword.prf_script) =>
   102                   (rendering.indentation(info.range) min limit) max 0
   103                 case _ => 0
   104               }
   105           }
   106 
   107           def indent_indent(tok: Token): Int =
   108             if (keywords.is_command(tok, keyword_open)) indent_size
   109             else if (keywords.is_command(tok, keyword_close)) - indent_size
   110             else 0
   111 
   112           def indent_offset(tok: Token): Int =
   113             if (keywords.is_command(tok, Keyword.proof_enclose)) indent_size
   114             else 0
   115 
   116           def indent_structure: Int =
   117             nav.reverse_iterator(current_line - 1).scanLeft((0, false))(
   118               { case ((ind, _), Text.Info(range, tok)) =>
   119                   val ind1 = ind + indent_indent(tok)
   120                   if (tok.is_begin_or_command && !keywords.is_command(tok, Keyword.prf_script)) {
   121                     val line = buffer.getLineOfOffset(range.start)
   122                     line_head(line) match {
   123                       case Some(info) if info.info == tok =>
   124                         (ind1 + indent_offset(tok) + line_indent(line), true)
   125                       case _ => (ind1, false)
   126                     }
   127                   }
   128                   else (ind1, false)
   129               }).collectFirst({ case (i, true) => i }).getOrElse(0)
   130 
   131           def indent_brackets: Int =
   132             (0 /: prev_line_span)(
   133               { case (i, tok) =>
   134                   if (tok.is_open_bracket) i + indent_size
   135                   else if (tok.is_close_bracket) i - indent_size
   136                   else i })
   137 
   138           def indent_extra: Int =
   139             if (prev_span.exists(keywords.is_quasi_command(_))) indent_size
   140             else 0
   141 
   142           val indent =
   143             if (Token_Markup.Line_Context.prev(buffer, current_line).get_context == Scan.Finished) {
   144               line_head(current_line) match {
   145                 case Some(info @ Text.Info(range, tok)) =>
   146                   if (tok.is_begin ||
   147                       keywords.is_before_command(tok) ||
   148                       keywords.is_command(tok, Keyword.theory)) 0
   149                   else if (keywords.is_command(tok, Keyword.proof_enclose))
   150                     indent_structure + script_indent(info) - indent_offset(tok)
   151                   else if (keywords.is_command(tok, Keyword.proof))
   152                     (indent_structure + script_indent(info) - indent_offset(tok)) max indent_size
   153                   else if (tok.is_command) indent_structure - indent_offset(tok)
   154                   else {
   155                     prev_line_command match {
   156                       case None =>
   157                         val extra =
   158                           (keywords.is_quasi_command(tok), head_is_quasi_command(prev_line)) match {
   159                             case (true, true) | (false, false) => 0
   160                             case (true, false) => - indent_extra
   161                             case (false, true) => indent_extra
   162                           }
   163                         line_indent(prev_line) + indent_brackets + extra - indent_offset(tok)
   164                       case Some(prev_tok) =>
   165                         indent_structure + indent_brackets + indent_size - indent_offset(tok) -
   166                         indent_offset(prev_tok) - indent_indent(prev_tok)
   167                     }
   168                   }
   169                 case None =>
   170                   prev_line_command match {
   171                     case None =>
   172                       val extra = if (head_is_quasi_command(prev_line)) indent_extra else 0
   173                       line_indent(prev_line) + indent_brackets + extra
   174                     case Some(prev_tok) =>
   175                       indent_structure + indent_brackets + indent_size -
   176                       indent_offset(prev_tok) - indent_indent(prev_tok)
   177                   }
   178               }
   179             }
   180             else line_indent(current_line)
   181 
   182           actions.clear()
   183           actions.add(new IndentAction.AlignOffset(indent max 0))
   184         case _ =>
   185       }
   186     }
   187   }
   188 
   189 
   190   /* structure matching */
   191 
   192   object Matcher extends StructureMatcher
   193   {
   194     private def find_block(
   195       open: Token => Boolean,
   196       close: Token => Boolean,
   197       reset: Token => Boolean,
   198       restrict: Token => Boolean,
   199       it: Iterator[Text.Info[Token]]): Option[(Text.Range, Text.Range)] =
   200     {
   201       val range1 = it.next.range
   202       it.takeWhile(info => !info.info.is_command || restrict(info.info)).
   203         scanLeft((range1, 1))(
   204           { case ((r, d), Text.Info(range, tok)) =>
   205               if (open(tok)) (range, d + 1)
   206               else if (close(tok)) (range, d - 1)
   207               else if (reset(tok)) (range, 0)
   208               else (r, d) }
   209         ).collectFirst({ case (range2, 0) => (range1, range2) })
   210     }
   211 
   212     private def find_pair(text_area: TextArea): Option[(Text.Range, Text.Range)] =
   213     {
   214       val buffer = text_area.getBuffer
   215       val caret_line = text_area.getCaretLine
   216       val caret = text_area.getCaretPosition
   217 
   218       Isabelle.buffer_syntax(text_area.getBuffer) match {
   219         case Some(syntax) if buffer.isInstanceOf[Buffer] =>
   220           val keywords = syntax.keywords
   221 
   222           val nav = new Navigator(syntax, buffer.asInstanceOf[Buffer], false)
   223 
   224           def caret_iterator(): Iterator[Text.Info[Token]] =
   225             nav.iterator(caret_line).dropWhile(info => !info.range.touches(caret))
   226 
   227           def reverse_caret_iterator(): Iterator[Text.Info[Token]] =
   228             nav.reverse_iterator(caret_line).dropWhile(info => !info.range.touches(caret))
   229 
   230           nav.iterator(caret_line, 1).find(info => info.range.touches(caret))
   231           match {
   232             case Some(Text.Info(range1, tok)) if keywords.is_command(tok, Keyword.theory_goal) =>
   233               find_block(
   234                 keywords.is_command(_, Keyword.proof_goal),
   235                 keywords.is_command(_, Keyword.qed),
   236                 keywords.is_command(_, Keyword.qed_global),
   237                 t =>
   238                   keywords.is_command(t, Keyword.diag) ||
   239                   keywords.is_command(t, Keyword.proof),
   240                 caret_iterator())
   241 
   242             case Some(Text.Info(range1, tok)) if keywords.is_command(tok, Keyword.proof_goal) =>
   243               find_block(
   244                 keywords.is_command(_, Keyword.proof_goal),
   245                 keywords.is_command(_, Keyword.qed),
   246                 _ => false,
   247                 t =>
   248                   keywords.is_command(t, Keyword.diag) ||
   249                   keywords.is_command(t, Keyword.proof),
   250                 caret_iterator())
   251 
   252             case Some(Text.Info(range1, tok)) if keywords.is_command(tok, Keyword.qed_global) =>
   253               reverse_caret_iterator().find(info => keywords.is_command(info.info, Keyword.theory))
   254               match {
   255                 case Some(Text.Info(range2, tok))
   256                 if keywords.is_command(tok, Keyword.theory_goal) => Some((range1, range2))
   257                 case _ => None
   258               }
   259 
   260             case Some(Text.Info(range1, tok)) if keywords.is_command(tok, Keyword.qed) =>
   261               find_block(
   262                 keywords.is_command(_, Keyword.qed),
   263                 t =>
   264                   keywords.is_command(t, Keyword.proof_goal) ||
   265                   keywords.is_command(t, Keyword.theory_goal),
   266                 _ => false,
   267                 t =>
   268                   keywords.is_command(t, Keyword.diag) ||
   269                   keywords.is_command(t, Keyword.proof) ||
   270                   keywords.is_command(t, Keyword.theory_goal),
   271                 reverse_caret_iterator())
   272 
   273             case Some(Text.Info(range1, tok)) if tok.is_begin =>
   274               find_block(_.is_begin, _.is_end, _ => false, _ => true, caret_iterator())
   275 
   276             case Some(Text.Info(range1, tok)) if tok.is_end =>
   277               find_block(_.is_end, _.is_begin, _ => false, _ => true, reverse_caret_iterator())
   278               match {
   279                 case Some((_, range2)) =>
   280                   reverse_caret_iterator().
   281                     dropWhile(info => info.range != range2).
   282                     dropWhile(info => info.range == range2).
   283                     find(info => info.info.is_command || info.info.is_begin)
   284                   match {
   285                     case Some(Text.Info(range3, tok)) =>
   286                       if (keywords.is_command(tok, Keyword.theory_block)) Some((range1, range3))
   287                       else Some((range1, range2))
   288                     case None => None
   289                   }
   290                 case None => None
   291               }
   292 
   293             case _ => None
   294           }
   295         case _ => None
   296       }
   297     }
   298 
   299     def getMatch(text_area: TextArea): StructureMatcher.Match =
   300       find_pair(text_area) match {
   301         case Some((_, range)) =>
   302           val line = text_area.getBuffer.getLineOfOffset(range.start)
   303           new StructureMatcher.Match(Matcher, line, range.start, line, range.stop)
   304         case None => null
   305       }
   306 
   307     def selectMatch(text_area: TextArea)
   308     {
   309       def get_span(offset: Text.Offset): Option[Text.Range] =
   310         for {
   311           syntax <- Isabelle.buffer_syntax(text_area.getBuffer)
   312           span <- Token_Markup.command_span(syntax, text_area.getBuffer, offset)
   313         } yield span.range
   314 
   315       find_pair(text_area) match {
   316         case Some((r1, r2)) =>
   317           (get_span(r1.start), get_span(r2.start)) match {
   318             case (Some(range1), Some(range2)) =>
   319               val start = range1.start min range2.start
   320               val stop = range1.stop max range2.stop
   321 
   322               text_area.moveCaretPosition(stop, false)
   323               if (!text_area.isMultipleSelectionEnabled) text_area.selectNone
   324               text_area.addToSelection(new Selection.Range(start, stop))
   325             case _ =>
   326           }
   327         case None =>
   328       }
   329     }
   330   }
   331 }