src/Pure/Thy/completion.scala
author wenzelm
Mon Nov 02 20:50:48 2009 +0100 (2009-11-02)
changeset 33388 d64545e6cba5
parent 31780 d78e5cff9a9f
child 34093 3d654643cf56
permissions -rw-r--r--
modernized structure Proof_Syntax;
wenzelm@31763
     1
/*  Title:      Pure/Thy/completion.scala
wenzelm@31763
     2
    Author:     Makarius
wenzelm@31763
     3
wenzelm@31763
     4
Completion of symbols and keywords.
wenzelm@31763
     5
*/
wenzelm@31763
     6
wenzelm@31763
     7
package isabelle
wenzelm@31763
     8
wenzelm@31763
     9
import scala.util.matching.Regex
wenzelm@31763
    10
import scala.util.parsing.combinator.RegexParsers
wenzelm@31763
    11
wenzelm@31763
    12
wenzelm@31763
    13
private object Completion
wenzelm@31763
    14
{
wenzelm@31763
    15
  /** String/CharSequence utilities */
wenzelm@31763
    16
wenzelm@31763
    17
  def length_ord(s1: String, s2: String): Boolean =
wenzelm@31763
    18
    s1.length < s2.length || s1.length == s2.length && s1 <= s2
wenzelm@31763
    19
wenzelm@31763
    20
  class Reverse(text: CharSequence, start: Int, end: Int) extends CharSequence
wenzelm@31763
    21
  {
wenzelm@31763
    22
    require(0 <= start && start <= end && end <= text.length)
wenzelm@31763
    23
wenzelm@31763
    24
    def this(text: CharSequence) = this(text, 0, text.length)
wenzelm@31763
    25
wenzelm@31763
    26
    def length: Int = end - start
wenzelm@31763
    27
    def charAt(i: Int): Char = text.charAt(end - i - 1)
wenzelm@31763
    28
wenzelm@31763
    29
    def subSequence(i: Int, j: Int): CharSequence =
wenzelm@31763
    30
      if (0 <= i && i <= j && j <= length) new Reverse(text, end - j, end - i)
wenzelm@31763
    31
      else throw new IndexOutOfBoundsException
wenzelm@31763
    32
wenzelm@31763
    33
    override def toString: String =
wenzelm@31763
    34
    {
wenzelm@31763
    35
      val buf = new StringBuffer(length)
wenzelm@31763
    36
      for (i <- 0 until length)
wenzelm@31763
    37
        buf.append(charAt(i))
wenzelm@31763
    38
      buf.toString
wenzelm@31763
    39
    }
wenzelm@31763
    40
  }
wenzelm@31763
    41
wenzelm@31763
    42
wenzelm@31763
    43
  /** word completion **/
wenzelm@31763
    44
wenzelm@31763
    45
  val word_regex = "[a-zA-Z0-9_']+".r
wenzelm@31763
    46
  def is_word(s: CharSequence): Boolean = word_regex.pattern.matcher(s).matches
wenzelm@31763
    47
wenzelm@31763
    48
  object Parse extends RegexParsers
wenzelm@31763
    49
  {
wenzelm@31763
    50
    override val whiteSpace = "".r
wenzelm@31763
    51
wenzelm@31765
    52
    def rev_symbol: Parser[String] = """>[A-Za-z0-9_']+<\\""".r
wenzelm@31765
    53
    def rev_symb: Parser[String] = """[A-Za-z0-9_']{2,}<\\""".r
wenzelm@31763
    54
    def word: Parser[String] = "[a-zA-Z0-9_']{3,}".r
wenzelm@31763
    55
wenzelm@31763
    56
    def read(in: CharSequence): Option[String] =
wenzelm@31763
    57
    {
wenzelm@31765
    58
      val rev_in = new Reverse(in)
wenzelm@31765
    59
      parse((rev_symbol | rev_symb | word) ^^ (_.reverse), rev_in) match {
wenzelm@31763
    60
        case Success(result, _) => Some(result)
wenzelm@31763
    61
        case _ => None
wenzelm@31763
    62
      }
wenzelm@31763
    63
    }
wenzelm@31763
    64
  }
wenzelm@31763
    65
}
wenzelm@31763
    66
wenzelm@31763
    67
class Completion
wenzelm@31763
    68
{
wenzelm@31763
    69
  /* representation */
wenzelm@31763
    70
wenzelm@31780
    71
  protected val words_lex = Scan.Lexicon()
wenzelm@31780
    72
  protected val words_map = Map[String, String]()
wenzelm@31763
    73
wenzelm@31780
    74
  protected val abbrevs_lex = Scan.Lexicon()
wenzelm@31780
    75
  protected val abbrevs_map = Map[String, (String, String)]()
wenzelm@31763
    76
wenzelm@31763
    77
wenzelm@31763
    78
  /* adding stuff */
wenzelm@31763
    79
wenzelm@31763
    80
  def + (keyword: String): Completion =
wenzelm@31763
    81
  {
wenzelm@31763
    82
    val old = this
wenzelm@31763
    83
    new Completion {
wenzelm@31763
    84
      override val words_lex = old.words_lex + keyword
wenzelm@31763
    85
      override val words_map = old.words_map + (keyword -> keyword)
wenzelm@31763
    86
      override val abbrevs_lex = old.abbrevs_lex
wenzelm@31763
    87
      override val abbrevs_map = old.abbrevs_map
wenzelm@31763
    88
    }
wenzelm@31763
    89
  }
wenzelm@31763
    90
wenzelm@31763
    91
  def + (symbols: Symbol.Interpretation): Completion =
wenzelm@31763
    92
  {
wenzelm@31763
    93
    val words =
wenzelm@31763
    94
      (for ((x, _) <- symbols.names) yield (x, x)).toList :::
wenzelm@31763
    95
      (for ((x, y) <- symbols.names) yield (y, x)).toList :::
wenzelm@31763
    96
      (for ((x, y) <- symbols.abbrevs if Completion.is_word(y)) yield (y, x)).toList
wenzelm@31763
    97
wenzelm@31763
    98
    val abbrs =
wenzelm@31763
    99
      (for ((x, y) <- symbols.abbrevs if !Completion.is_word(y))
wenzelm@31765
   100
        yield (y.reverse.toString, (y, x))).toList
wenzelm@31763
   101
wenzelm@31763
   102
    val old = this
wenzelm@31763
   103
    new Completion {
wenzelm@31763
   104
      override val words_lex = old.words_lex ++ words.map(_._1)
wenzelm@31765
   105
      override val words_map = old.words_map ++ words
wenzelm@31763
   106
      override val abbrevs_lex = old.abbrevs_lex ++ abbrs.map(_._1)
wenzelm@31763
   107
      override val abbrevs_map = old.abbrevs_map ++ abbrs
wenzelm@31763
   108
    }
wenzelm@31763
   109
  }
wenzelm@31763
   110
wenzelm@31763
   111
wenzelm@31763
   112
  /* complete */
wenzelm@31763
   113
wenzelm@31765
   114
  def complete(line: CharSequence): Option[(String, List[String])] =
wenzelm@31763
   115
  {
wenzelm@31765
   116
    abbrevs_lex.parse(abbrevs_lex.keyword, new Completion.Reverse(line)) match {
wenzelm@31765
   117
      case abbrevs_lex.Success(rev_a, _) =>
wenzelm@31765
   118
        val (word, c) = abbrevs_map(rev_a)
wenzelm@31765
   119
        Some(word, List(c))
wenzelm@31765
   120
      case _ =>
wenzelm@31765
   121
        Completion.Parse.read(line) match {
wenzelm@31765
   122
          case Some(word) =>
wenzelm@31765
   123
            words_lex.completions(word) match {
wenzelm@31765
   124
              case Nil => None
wenzelm@31765
   125
              case cs => Some(word, cs.map(words_map(_)).sort(Completion.length_ord _))
wenzelm@31765
   126
            }
wenzelm@31765
   127
          case None => None
wenzelm@31765
   128
        }
wenzelm@31765
   129
    }
wenzelm@31763
   130
  }
wenzelm@31763
   131
}