misc tuning and clarification;
authorwenzelm
Fri Mar 07 19:56:31 2014 +0100 (2014-03-07)
changeset 55983fc5977bd4829
parent 55982 b719781c7396
child 55984 2aaecd737d75
misc tuning and clarification;
src/Pure/General/completion.scala
     1.1 --- a/src/Pure/General/completion.scala	Fri Mar 07 19:28:34 2014 +0100
     1.2 +++ b/src/Pure/General/completion.scala	Fri Mar 07 19:56:31 2014 +0100
     1.3 @@ -263,7 +263,7 @@
     1.4    abbrevs_lex: Scan.Lexicon = Scan.Lexicon.empty,
     1.5    abbrevs_map: Multi_Map[String, (String, String)] = Multi_Map.empty)
     1.6  {
     1.7 -  /* adding stuff */
     1.8 +  /* keywords */
     1.9  
    1.10    def + (keyword: String, replace: String): Completion =
    1.11      new Completion(
    1.12 @@ -275,6 +275,9 @@
    1.13  
    1.14    def + (keyword: String): Completion = this + (keyword, keyword)
    1.15  
    1.16 +
    1.17 +  /* symbols with abbreviations */
    1.18 +
    1.19    private def add_symbols(): Completion =
    1.20    {
    1.21      val words =
    1.22 @@ -361,33 +364,36 @@
    1.23        }
    1.24  
    1.25      (abbrevs_result orElse words_result) match {
    1.26 -      case Some(((word, cs), end)) =>
    1.27 -        val range = Text.Range(- word.length, 0) + end + start
    1.28 -        val ds = cs.map(decode(_)).filter(_ != word)
    1.29 -        if (ds.isEmpty) None
    1.30 -        else {
    1.31 +      case Some(((original, completions0), end)) =>
    1.32 +        val completions1 = completions0.map(decode(_))
    1.33 +        if (completions1.exists(_ != original)) {
    1.34 +          val range = Text.Range(- original.length, 0) + end + start
    1.35            val immediate =
    1.36 -            !Completion.Word_Parsers.is_word(word) &&
    1.37 -            Character.codePointCount(word, 0, word.length) > 1
    1.38 +            explicit ||
    1.39 +              (!Completion.Word_Parsers.is_word(original) &&
    1.40 +                Character.codePointCount(original, 0, original.length) > 1)
    1.41 +          val unique = completions0.length == 1
    1.42            val items =
    1.43 -            for { (name, name1) <- cs zip ds }
    1.44 -            yield {
    1.45 -              val (s1, s2) =
    1.46 +            for {
    1.47 +              (name0, name1) <- completions0 zip completions1
    1.48 +              if name1 != original
    1.49 +              (s1, s2) =
    1.50                  space_explode(Completion.caret_indicator, name1) match {
    1.51                    case List(s1, s2) => (s1, s2)
    1.52                    case _ => (name1, "")
    1.53                  }
    1.54 -              val move = - s2.length
    1.55 -              val description =
    1.56 +              move = - s2.length
    1.57 +              description =
    1.58                  if (move != 0) List(name1, "(template)")
    1.59 -                else if (words_result.isDefined && keywords(name)) List(name1, "(keyword)")
    1.60 -                else if (Symbol.names.isDefinedAt(name) && name != name1)
    1.61 -                  List(name1, "(symbol " + quote(name) + ")")
    1.62 +                else if (words_result.isDefined && keywords(name0)) List(name1, "(keyword)")
    1.63 +                else if (Symbol.names.isDefinedAt(name0) && name0 != name1)
    1.64 +                  List(name1, "(symbol " + quote(name0) + ")")
    1.65                  else List(name1)
    1.66 -              Completion.Item(range, word, name1, description, s1 + s2, move, explicit || immediate)
    1.67              }
    1.68 -          Some(Completion.Result(range, word, cs.length == 1, items.sorted(history.ordering)))
    1.69 +            yield Completion.Item(range, original, name1, description, s1 + s2, move, immediate)
    1.70 +          Some(Completion.Result(range, original, unique, items.sorted(history.ordering)))
    1.71          }
    1.72 +        else None
    1.73        case None => None
    1.74      }
    1.75    }