tuned;
authorwenzelm
Sat Mar 08 11:50:12 2014 +0100 (2014-03-08)
changeset 559921e7f04ba8196
parent 55991 3fa6e6c81788
child 55993 4c17e46c44c1
tuned;
src/Pure/General/completion.scala
     1.1 --- a/src/Pure/General/completion.scala	Fri Mar 07 23:28:05 2014 +0100
     1.2 +++ b/src/Pure/General/completion.scala	Sat Mar 08 11:50:12 2014 +0100
     1.3 @@ -3,7 +3,8 @@
     1.4  
     1.5  Semantic completion within the formal context (reported names).
     1.6  Syntactic completion of keywords and symbols, with abbreviations
     1.7 -(based on language context).  */
     1.8 +(based on language context).
     1.9 +*/
    1.10  
    1.11  package isabelle
    1.12  
    1.13 @@ -346,31 +347,29 @@
    1.14          val end =
    1.15            if (extend_word) Completion.Word_Parsers.extend_word(text, caret)
    1.16            else caret
    1.17 -        (Completion.Word_Parsers.read_symbol(text.subSequence(0, end)) match {
    1.18 -          case Some(symbol) => Some(symbol)
    1.19 -          case None =>
    1.20 -            val word_context =
    1.21 -              end < length && Completion.Word_Parsers.is_word_char(text.charAt(end))
    1.22 -            if (word_context) None
    1.23 -            else Completion.Word_Parsers.read_word(explicit, text.subSequence(0, end))
    1.24 -        }) match {
    1.25 -          case Some(word) =>
    1.26 +        val opt_word =
    1.27 +          Completion.Word_Parsers.read_symbol(text.subSequence(0, end)) match {
    1.28 +            case Some(symbol) => Some(symbol)
    1.29 +            case None =>
    1.30 +              val word_context =
    1.31 +                end < length && Completion.Word_Parsers.is_word_char(text.charAt(end))
    1.32 +              if (word_context) None
    1.33 +              else Completion.Word_Parsers.read_word(explicit, text.subSequence(0, end))
    1.34 +          }
    1.35 +        opt_word.map(word =>
    1.36 +          {
    1.37              val completions =
    1.38                for {
    1.39                  s <- words_lex.completions(word)
    1.40                  if (if (is_keyword(s)) language_context.is_outer else language_context.symbols)
    1.41                  r <- words_map.get_list(s)
    1.42                } yield r
    1.43 -            if (completions.isEmpty) None
    1.44 -            else Some(((word, completions), end))
    1.45 -          case None => None
    1.46 -        }
    1.47 +            (((word, completions), end))
    1.48 +          })
    1.49        }
    1.50  
    1.51      (abbrevs_result orElse words_result) match {
    1.52 -      case Some(((original, completions0), end)) =>
    1.53 -        val completions1 = completions0.map(decode(_))
    1.54 -
    1.55 +      case Some(((original, completions0), end)) if !completions0.isEmpty =>
    1.56          val range = Text.Range(- original.length, 0) + end + start
    1.57          val immediate =
    1.58            explicit ||
    1.59 @@ -378,6 +377,7 @@
    1.60                Character.codePointCount(original, 0, original.length) > 1)
    1.61          val unique = completions0.length == 1
    1.62  
    1.63 +        val completions1 = completions0.map(decode(_))
    1.64          val items =
    1.65            for {
    1.66              (name0, name1) <- completions0 zip completions1
    1.67 @@ -404,7 +404,7 @@
    1.68          if (items.isEmpty) None
    1.69          else Some(Completion.Result(range, original, unique, items.sorted(history.ordering)))
    1.70  
    1.71 -      case None => None
    1.72 +      case _ => None
    1.73      }
    1.74    }
    1.75  }