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