src/Pure/Thy/completion.scala
author wenzelm
Sun, 19 Jun 2011 21:43:41 +0200
changeset 43462 7f65a68f8b26
parent 40533 e38e80686ce5
child 43695 5130dfe1b7be
permissions -rw-r--r--
completion for control symbols;
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
  /** word completion **/
c2c2d380729d Completion of symbols and keywords.
wenzelm
parents:
diff changeset
    16
c2c2d380729d Completion of symbols and keywords.
wenzelm
parents:
diff changeset
    17
  val word_regex = "[a-zA-Z0-9_']+".r
c2c2d380729d Completion of symbols and keywords.
wenzelm
parents:
diff changeset
    18
  def is_word(s: CharSequence): Boolean = word_regex.pattern.matcher(s).matches
c2c2d380729d Completion of symbols and keywords.
wenzelm
parents:
diff changeset
    19
c2c2d380729d Completion of symbols and keywords.
wenzelm
parents:
diff changeset
    20
  object Parse extends RegexParsers
c2c2d380729d Completion of symbols and keywords.
wenzelm
parents:
diff changeset
    21
  {
c2c2d380729d Completion of symbols and keywords.
wenzelm
parents:
diff changeset
    22
    override val whiteSpace = "".r
c2c2d380729d Completion of symbols and keywords.
wenzelm
parents:
diff changeset
    23
43462
7f65a68f8b26 completion for control symbols;
wenzelm
parents: 40533
diff changeset
    24
    def reverse_symbol: Parser[String] = """>[A-Za-z0-9_']+\^?<\\""".r
7f65a68f8b26 completion for control symbols;
wenzelm
parents: 40533
diff changeset
    25
    def reverse_symb: Parser[String] = """[A-Za-z0-9_']{2,}\^?<\\""".r
40533
e38e80686ce5 somewhat adhoc replacement for 'thus' and 'hence';
wenzelm
parents: 37072
diff changeset
    26
    def word: Parser[String] = "[a-zA-Z0-9_']{2,}".r
31763
c2c2d380729d Completion of symbols and keywords.
wenzelm
parents:
diff changeset
    27
c2c2d380729d Completion of symbols and keywords.
wenzelm
parents:
diff changeset
    28
    def read(in: CharSequence): Option[String] =
c2c2d380729d Completion of symbols and keywords.
wenzelm
parents:
diff changeset
    29
    {
37072
9105c8237c7a renamed "rev" to "reverse" following usual Scala conventions;
wenzelm
parents: 36012
diff changeset
    30
      val reverse_in = new Library.Reverse(in)
9105c8237c7a renamed "rev" to "reverse" following usual Scala conventions;
wenzelm
parents: 36012
diff changeset
    31
      parse((reverse_symbol | reverse_symb | word) ^^ (_.reverse), reverse_in) match {
31763
c2c2d380729d Completion of symbols and keywords.
wenzelm
parents:
diff changeset
    32
        case Success(result, _) => Some(result)
c2c2d380729d Completion of symbols and keywords.
wenzelm
parents:
diff changeset
    33
        case _ => None
c2c2d380729d Completion of symbols and keywords.
wenzelm
parents:
diff changeset
    34
      }
c2c2d380729d Completion of symbols and keywords.
wenzelm
parents:
diff changeset
    35
    }
c2c2d380729d Completion of symbols and keywords.
wenzelm
parents:
diff changeset
    36
  }
c2c2d380729d Completion of symbols and keywords.
wenzelm
parents:
diff changeset
    37
}
c2c2d380729d Completion of symbols and keywords.
wenzelm
parents:
diff changeset
    38
c2c2d380729d Completion of symbols and keywords.
wenzelm
parents:
diff changeset
    39
class Completion
c2c2d380729d Completion of symbols and keywords.
wenzelm
parents:
diff changeset
    40
{
c2c2d380729d Completion of symbols and keywords.
wenzelm
parents:
diff changeset
    41
  /* representation */
c2c2d380729d Completion of symbols and keywords.
wenzelm
parents:
diff changeset
    42
31780
d78e5cff9a9f non-public representation;
wenzelm
parents: 31765
diff changeset
    43
  protected val words_lex = Scan.Lexicon()
d78e5cff9a9f non-public representation;
wenzelm
parents: 31765
diff changeset
    44
  protected val words_map = Map[String, String]()
31763
c2c2d380729d Completion of symbols and keywords.
wenzelm
parents:
diff changeset
    45
31780
d78e5cff9a9f non-public representation;
wenzelm
parents: 31765
diff changeset
    46
  protected val abbrevs_lex = Scan.Lexicon()
d78e5cff9a9f non-public representation;
wenzelm
parents: 31765
diff changeset
    47
  protected val abbrevs_map = Map[String, (String, String)]()
31763
c2c2d380729d Completion of symbols and keywords.
wenzelm
parents:
diff changeset
    48
c2c2d380729d Completion of symbols and keywords.
wenzelm
parents:
diff changeset
    49
c2c2d380729d Completion of symbols and keywords.
wenzelm
parents:
diff changeset
    50
  /* adding stuff */
c2c2d380729d Completion of symbols and keywords.
wenzelm
parents:
diff changeset
    51
40533
e38e80686ce5 somewhat adhoc replacement for 'thus' and 'hence';
wenzelm
parents: 37072
diff changeset
    52
  def + (keyword: String, replace: String): Completion =
31763
c2c2d380729d Completion of symbols and keywords.
wenzelm
parents:
diff changeset
    53
  {
c2c2d380729d Completion of symbols and keywords.
wenzelm
parents:
diff changeset
    54
    val old = this
c2c2d380729d Completion of symbols and keywords.
wenzelm
parents:
diff changeset
    55
    new Completion {
c2c2d380729d Completion of symbols and keywords.
wenzelm
parents:
diff changeset
    56
      override val words_lex = old.words_lex + keyword
40533
e38e80686ce5 somewhat adhoc replacement for 'thus' and 'hence';
wenzelm
parents: 37072
diff changeset
    57
      override val words_map = old.words_map + (keyword -> replace)
31763
c2c2d380729d Completion of symbols and keywords.
wenzelm
parents:
diff changeset
    58
      override val abbrevs_lex = old.abbrevs_lex
c2c2d380729d Completion of symbols and keywords.
wenzelm
parents:
diff changeset
    59
      override val abbrevs_map = old.abbrevs_map
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
40533
e38e80686ce5 somewhat adhoc replacement for 'thus' and 'hence';
wenzelm
parents: 37072
diff changeset
    63
  def + (keyword: String): Completion = this + (keyword, keyword)
e38e80686ce5 somewhat adhoc replacement for 'thus' and 'hence';
wenzelm
parents: 37072
diff changeset
    64
31763
c2c2d380729d Completion of symbols and keywords.
wenzelm
parents:
diff changeset
    65
  def + (symbols: Symbol.Interpretation): Completion =
c2c2d380729d Completion of symbols and keywords.
wenzelm
parents:
diff changeset
    66
  {
c2c2d380729d Completion of symbols and keywords.
wenzelm
parents:
diff changeset
    67
    val words =
c2c2d380729d Completion of symbols and keywords.
wenzelm
parents:
diff changeset
    68
      (for ((x, _) <- symbols.names) yield (x, x)).toList :::
c2c2d380729d Completion of symbols and keywords.
wenzelm
parents:
diff changeset
    69
      (for ((x, y) <- symbols.names) yield (y, x)).toList :::
c2c2d380729d Completion of symbols and keywords.
wenzelm
parents:
diff changeset
    70
      (for ((x, y) <- symbols.abbrevs if Completion.is_word(y)) yield (y, x)).toList
c2c2d380729d Completion of symbols and keywords.
wenzelm
parents:
diff changeset
    71
c2c2d380729d Completion of symbols and keywords.
wenzelm
parents:
diff changeset
    72
    val abbrs =
c2c2d380729d Completion of symbols and keywords.
wenzelm
parents:
diff changeset
    73
      (for ((x, y) <- symbols.abbrevs if !Completion.is_word(y))
31765
a5fdf7a76f9d tuned input: require longer symbol prefix;
wenzelm
parents: 31763
diff changeset
    74
        yield (y.reverse.toString, (y, x))).toList
31763
c2c2d380729d Completion of symbols and keywords.
wenzelm
parents:
diff changeset
    75
c2c2d380729d Completion of symbols and keywords.
wenzelm
parents:
diff changeset
    76
    val old = this
c2c2d380729d Completion of symbols and keywords.
wenzelm
parents:
diff changeset
    77
    new Completion {
c2c2d380729d Completion of symbols and keywords.
wenzelm
parents:
diff changeset
    78
      override val words_lex = old.words_lex ++ words.map(_._1)
31765
a5fdf7a76f9d tuned input: require longer symbol prefix;
wenzelm
parents: 31763
diff changeset
    79
      override val words_map = old.words_map ++ words
31763
c2c2d380729d Completion of symbols and keywords.
wenzelm
parents:
diff changeset
    80
      override val abbrevs_lex = old.abbrevs_lex ++ abbrs.map(_._1)
c2c2d380729d Completion of symbols and keywords.
wenzelm
parents:
diff changeset
    81
      override val abbrevs_map = old.abbrevs_map ++ abbrs
c2c2d380729d Completion of symbols and keywords.
wenzelm
parents:
diff changeset
    82
    }
c2c2d380729d Completion of symbols and keywords.
wenzelm
parents:
diff changeset
    83
  }
c2c2d380729d Completion of symbols and keywords.
wenzelm
parents:
diff changeset
    84
c2c2d380729d Completion of symbols and keywords.
wenzelm
parents:
diff changeset
    85
c2c2d380729d Completion of symbols and keywords.
wenzelm
parents:
diff changeset
    86
  /* complete */
c2c2d380729d Completion of symbols and keywords.
wenzelm
parents:
diff changeset
    87
31765
a5fdf7a76f9d tuned input: require longer symbol prefix;
wenzelm
parents: 31763
diff changeset
    88
  def complete(line: CharSequence): Option[(String, List[String])] =
31763
c2c2d380729d Completion of symbols and keywords.
wenzelm
parents:
diff changeset
    89
  {
34141
297b2149077d simiplified result of keyword parser (again);
wenzelm
parents: 34135
diff changeset
    90
    abbrevs_lex.parse(abbrevs_lex.keyword, new Library.Reverse(line)) match {
37072
9105c8237c7a renamed "rev" to "reverse" following usual Scala conventions;
wenzelm
parents: 36012
diff changeset
    91
      case abbrevs_lex.Success(reverse_a, _) =>
9105c8237c7a renamed "rev" to "reverse" following usual Scala conventions;
wenzelm
parents: 36012
diff changeset
    92
        val (word, c) = abbrevs_map(reverse_a)
35004
b89a31957950 filter out identical completions only after symbols.decode -- recover completion of literal symbols (e.g. \<AA>);
wenzelm
parents: 34141
diff changeset
    93
        Some(word, List(c))
31765
a5fdf7a76f9d tuned input: require longer symbol prefix;
wenzelm
parents: 31763
diff changeset
    94
      case _ =>
a5fdf7a76f9d tuned input: require longer symbol prefix;
wenzelm
parents: 31763
diff changeset
    95
        Completion.Parse.read(line) match {
a5fdf7a76f9d tuned input: require longer symbol prefix;
wenzelm
parents: 31763
diff changeset
    96
          case Some(word) =>
35004
b89a31957950 filter out identical completions only after symbols.decode -- recover completion of literal symbols (e.g. \<AA>);
wenzelm
parents: 34141
diff changeset
    97
            words_lex.completions(word).map(words_map(_)) match {
31765
a5fdf7a76f9d tuned input: require longer symbol prefix;
wenzelm
parents: 31763
diff changeset
    98
              case Nil => None
36012
0614676f14d4 replaced some deprecated methods;
wenzelm
parents: 35004
diff changeset
    99
              case cs => Some(word, cs.sortWith(_ < _))
31765
a5fdf7a76f9d tuned input: require longer symbol prefix;
wenzelm
parents: 31763
diff changeset
   100
            }
a5fdf7a76f9d tuned input: require longer symbol prefix;
wenzelm
parents: 31763
diff changeset
   101
          case None => None
a5fdf7a76f9d tuned input: require longer symbol prefix;
wenzelm
parents: 31763
diff changeset
   102
        }
a5fdf7a76f9d tuned input: require longer symbol prefix;
wenzelm
parents: 31763
diff changeset
   103
    }
31763
c2c2d380729d Completion of symbols and keywords.
wenzelm
parents:
diff changeset
   104
  }
c2c2d380729d Completion of symbols and keywords.
wenzelm
parents:
diff changeset
   105
}