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