src/Tools/jEdit/src/structure_matching.scala
author wenzelm
Tue Dec 09 21:14:11 2014 +0100 (2014-12-09)
changeset 59122 c1dbcde94cd2
parent 59074 7836d927ffca
permissions -rw-r--r--
tuned signature;
     1 /*  Title:      Tools/jEdit/src/structure_matching.scala
     2     Author:     Makarius
     3 
     4 Structure matcher for Isabelle/Isar outer syntax.
     5 */
     6 
     7 package isabelle.jedit
     8 
     9 
    10 import isabelle._
    11 
    12 import org.gjt.sp.jedit.textarea.{TextArea, StructureMatcher, Selection}
    13 
    14 
    15 object Structure_Matching
    16 {
    17   object Isabelle_Matcher extends StructureMatcher
    18   {
    19     private def find_block(
    20       open: Token => Boolean,
    21       close: Token => Boolean,
    22       reset: Token => Boolean,
    23       restrict: Token => Boolean,
    24       it: Iterator[Text.Info[Token]]): Option[(Text.Range, Text.Range)] =
    25     {
    26       val range1 = it.next.range
    27       it.takeWhile(info => !info.info.is_command || restrict(info.info)).
    28         scanLeft((range1, 1))(
    29           { case ((r, d), Text.Info(range, tok)) =>
    30               if (open(tok)) (range, d + 1)
    31               else if (close(tok)) (range, d - 1)
    32               else if (reset(tok)) (range, 0)
    33               else (r, d) }
    34         ).collectFirst({ case (range2, 0) => (range1, range2) })
    35     }
    36 
    37     private def find_pair(text_area: TextArea): Option[(Text.Range, Text.Range)] =
    38     {
    39       val buffer = text_area.getBuffer
    40       val caret_line = text_area.getCaretLine
    41       val caret = text_area.getCaretPosition
    42 
    43       Isabelle.buffer_syntax(text_area.getBuffer) match {
    44         case Some(syntax) =>
    45           val limit = PIDE.options.value.int("jedit_structure_limit") max 0
    46 
    47           def is_command_kind(token: Token, pred: String => Boolean): Boolean =
    48             token.is_command_kind(syntax.keywords, pred)
    49 
    50           def iterator(line: Int, lim: Int = limit): Iterator[Text.Info[Token]] =
    51             Token_Markup.line_token_iterator(syntax, buffer, line, line + lim).
    52               filter(_.info.is_proper)
    53 
    54           def rev_iterator(line: Int, lim: Int = limit): Iterator[Text.Info[Token]] =
    55             Token_Markup.line_token_reverse_iterator(syntax, buffer, line, line - lim).
    56               filter(_.info.is_proper)
    57 
    58           def caret_iterator(): Iterator[Text.Info[Token]] =
    59             iterator(caret_line).dropWhile(info => !info.range.touches(caret))
    60 
    61           def rev_caret_iterator(): Iterator[Text.Info[Token]] =
    62             rev_iterator(caret_line).dropWhile(info => !info.range.touches(caret))
    63 
    64           iterator(caret_line, 1).find(info => info.range.touches(caret))
    65           match {
    66             case Some(Text.Info(range1, tok)) if is_command_kind(tok, Keyword.theory_goal) =>
    67               find_block(
    68                 is_command_kind(_, Keyword.proof_goal),
    69                 is_command_kind(_, Keyword.qed),
    70                 is_command_kind(_, Keyword.qed_global),
    71                 t =>
    72                   is_command_kind(t, Keyword.diag) ||
    73                   is_command_kind(t, Keyword.proof),
    74                 caret_iterator())
    75 
    76             case Some(Text.Info(range1, tok)) if is_command_kind(tok, Keyword.proof_goal) =>
    77               find_block(
    78                 is_command_kind(_, Keyword.proof_goal),
    79                 is_command_kind(_, Keyword.qed),
    80                 _ => false,
    81                 t =>
    82                   is_command_kind(t, Keyword.diag) ||
    83                   is_command_kind(t, Keyword.proof),
    84                 caret_iterator())
    85 
    86             case Some(Text.Info(range1, tok)) if is_command_kind(tok, Keyword.qed_global) =>
    87               rev_caret_iterator().find(info => is_command_kind(info.info, Keyword.theory))
    88               match {
    89                 case Some(Text.Info(range2, tok))
    90                 if is_command_kind(tok, Keyword.theory_goal) => Some((range1, range2))
    91                 case _ => None
    92               }
    93 
    94             case Some(Text.Info(range1, tok)) if is_command_kind(tok, Keyword.qed) =>
    95               find_block(
    96                 is_command_kind(_, Keyword.qed),
    97                 t =>
    98                   is_command_kind(t, Keyword.proof_goal) ||
    99                   is_command_kind(t, Keyword.theory_goal),
   100                 _ => false,
   101                 t =>
   102                   is_command_kind(t, Keyword.diag) ||
   103                   is_command_kind(t, Keyword.proof) ||
   104                   is_command_kind(t, Keyword.theory_goal),
   105                 rev_caret_iterator())
   106 
   107             case Some(Text.Info(range1, tok)) if tok.is_begin =>
   108               find_block(_.is_begin, _.is_end, _ => false, _ => true, caret_iterator())
   109 
   110             case Some(Text.Info(range1, tok)) if tok.is_end =>
   111               find_block(_.is_end, _.is_begin, _ => false, _ => true, rev_caret_iterator())
   112               match {
   113                 case Some((_, range2)) =>
   114                   rev_caret_iterator().
   115                     dropWhile(info => info.range != range2).
   116                     dropWhile(info => info.range == range2).
   117                     find(info => info.info.is_command || info.info.is_begin)
   118                   match {
   119                     case Some(Text.Info(range3, tok)) =>
   120                       if (is_command_kind(tok, Keyword.theory_block)) Some((range1, range3))
   121                       else Some((range1, range2))
   122                     case None => None
   123                   }
   124                 case None => None
   125               }
   126 
   127             case _ => None
   128           }
   129         case None => None
   130       }
   131     }
   132 
   133     def getMatch(text_area: TextArea): StructureMatcher.Match =
   134       find_pair(text_area) match {
   135         case Some((_, range)) =>
   136           val line = text_area.getBuffer.getLineOfOffset(range.start)
   137           new StructureMatcher.Match(Structure_Matching.Isabelle_Matcher,
   138             line, range.start, line, range.stop)
   139         case None => null
   140       }
   141 
   142     def selectMatch(text_area: TextArea)
   143     {
   144       def get_span(offset: Text.Offset): Option[Text.Range] =
   145         for {
   146           syntax <- Isabelle.buffer_syntax(text_area.getBuffer)
   147           span <- Token_Markup.command_span(syntax, text_area.getBuffer, offset)
   148         } yield span.range
   149 
   150       find_pair(text_area) match {
   151         case Some((r1, r2)) =>
   152           (get_span(r1.start), get_span(r2.start)) match {
   153             case (Some(range1), Some(range2)) =>
   154               val start = range1.start min range2.start
   155               val stop = range1.stop max range2.stop
   156 
   157               text_area.moveCaretPosition(stop, false)
   158               if (!text_area.isMultipleSelectionEnabled) text_area.selectNone
   159               text_area.addToSelection(new Selection.Range(start, stop))
   160             case _ =>
   161           }
   162         case None =>
   163       }
   164     }
   165   }
   166 }
   167