tuned;
authorwenzelm
Fri Mar 07 20:24:14 2014 +0100 (2014-03-07)
changeset 55985594afef0dd89
parent 55984 2aaecd737d75
child 55986 61b0021ed674
tuned;
src/Pure/General/completion.scala
     1.1 --- a/src/Pure/General/completion.scala	Fri Mar 07 20:12:38 2014 +0100
     1.2 +++ b/src/Pure/General/completion.scala	Fri Mar 07 20:24:14 2014 +0100
     1.3 @@ -265,8 +265,8 @@
     1.4  {
     1.5    /* keywords */
     1.6  
     1.7 -  def is_keyword(name: String): Boolean = keywords.isDefinedAt(name)
     1.8 -  def is_keyword_template(name: String): Boolean = keywords.get(name) == Some(true)
     1.9 +  private def is_keyword(name: String): Boolean = keywords.isDefinedAt(name)
    1.10 +  private def is_keyword_template(name: String): Boolean = keywords.get(name) == Some(true)
    1.11  
    1.12    def + (keyword: String, template: String): Completion =
    1.13      new Completion(
    1.14 @@ -281,6 +281,9 @@
    1.15  
    1.16    /* symbols with abbreviations */
    1.17  
    1.18 +  private def is_symbol(name: String): Boolean =
    1.19 +    Symbol.names.isDefinedAt(name)
    1.20 +
    1.21    private def add_symbols(): Completion =
    1.22    {
    1.23      val words =
    1.24 @@ -369,38 +372,40 @@
    1.25      (abbrevs_result orElse words_result) match {
    1.26        case Some(((original, completions0), end)) =>
    1.27          val completions1 = completions0.map(decode(_))
    1.28 -        if (completions1.exists(_ != original)) {
    1.29 -          val range = Text.Range(- original.length, 0) + end + start
    1.30 -          val immediate =
    1.31 -            explicit ||
    1.32 -              (!Completion.Word_Parsers.is_word(original) &&
    1.33 -                Character.codePointCount(original, 0, original.length) > 1)
    1.34 -          val unique = completions0.length == 1
    1.35 -          val items =
    1.36 -            for {
    1.37 -              (name0, name1) <- completions0 zip completions1
    1.38 -              if name1 != original
    1.39 -              (s1, s2) =
    1.40 -                space_explode(Completion.caret_indicator, name1) match {
    1.41 -                  case List(s1, s2) => (s1, s2)
    1.42 -                  case _ => (name1, "")
    1.43 -                }
    1.44 -              move = - s2.length
    1.45 -              description =
    1.46 -                if (Symbol.names.isDefinedAt(name0)) {
    1.47 -                  if (name0 == name1) List(name0)
    1.48 -                  else List(name1, "(symbol " + quote(name0) + ")")
    1.49 -                }
    1.50 -                else if (move != 0 || is_keyword_template(name0))
    1.51 -                  List(name1, "(template)")
    1.52 -                else if (is_keyword(name0))
    1.53 -                  List(name1, "(keyword)")
    1.54 -                else List(name1)
    1.55 -            }
    1.56 -            yield Completion.Item(range, original, name1, description, s1 + s2, move, immediate)
    1.57 -          Some(Completion.Result(range, original, unique, items.sorted(history.ordering)))
    1.58 -        }
    1.59 -        else None
    1.60 +
    1.61 +        val range = Text.Range(- original.length, 0) + end + start
    1.62 +        val immediate =
    1.63 +          explicit ||
    1.64 +            (!Completion.Word_Parsers.is_word(original) &&
    1.65 +              Character.codePointCount(original, 0, original.length) > 1)
    1.66 +        val unique = completions0.length == 1
    1.67 +
    1.68 +        val items =
    1.69 +          for {
    1.70 +            (name0, name1) <- completions0 zip completions1
    1.71 +            if name1 != original
    1.72 +            (s1, s2) =
    1.73 +              space_explode(Completion.caret_indicator, name1) match {
    1.74 +                case List(s1, s2) => (s1, s2)
    1.75 +                case _ => (name1, "")
    1.76 +              }
    1.77 +            move = - s2.length
    1.78 +            description =
    1.79 +              if (is_symbol(name0)) {
    1.80 +                if (name0 == name1) List(name0)
    1.81 +                else List(name1, "(symbol " + quote(name0) + ")")
    1.82 +              }
    1.83 +              else if (move != 0 || is_keyword_template(name0))
    1.84 +                List(name1, "(template)")
    1.85 +              else if (is_keyword(name0))
    1.86 +                List(name1, "(keyword)")
    1.87 +              else List(name1)
    1.88 +          }
    1.89 +          yield Completion.Item(range, original, name1, description, s1 + s2, move, immediate)
    1.90 +
    1.91 +        if (items.isEmpty) None
    1.92 +        else Some(Completion.Result(range, original, unique, items.sorted(history.ordering)))
    1.93 +
    1.94        case None => None
    1.95      }
    1.96    }