# HG changeset patch
# User wenzelm
# Date 1394275812 -3600
# Node ID 1e7f04ba8196febc9bf15ddffd09ba81bb2462eb
# Parent  3fa6e6c817889f67f441cff9c532f2f4a5efe122
tuned;

diff -r 3fa6e6c81788 -r 1e7f04ba8196 src/Pure/General/completion.scala
--- a/src/Pure/General/completion.scala	Fri Mar 07 23:28:05 2014 +0100
+++ b/src/Pure/General/completion.scala	Sat Mar 08 11:50:12 2014 +0100
@@ -3,7 +3,8 @@
 
 Semantic completion within the formal context (reported names).
 Syntactic completion of keywords and symbols, with abbreviations
-(based on language context).  */
+(based on language context).
+*/
 
 package isabelle
 
@@ -346,31 +347,29 @@
         val end =
           if (extend_word) Completion.Word_Parsers.extend_word(text, caret)
           else caret
-        (Completion.Word_Parsers.read_symbol(text.subSequence(0, end)) match {
-          case Some(symbol) => Some(symbol)
-          case None =>
-            val word_context =
-              end < length && Completion.Word_Parsers.is_word_char(text.charAt(end))
-            if (word_context) None
-            else Completion.Word_Parsers.read_word(explicit, text.subSequence(0, end))
-        }) match {
-          case Some(word) =>
+        val opt_word =
+          Completion.Word_Parsers.read_symbol(text.subSequence(0, end)) match {
+            case Some(symbol) => Some(symbol)
+            case None =>
+              val word_context =
+                end < length && Completion.Word_Parsers.is_word_char(text.charAt(end))
+              if (word_context) None
+              else Completion.Word_Parsers.read_word(explicit, text.subSequence(0, end))
+          }
+        opt_word.map(word =>
+          {
             val completions =
               for {
                 s <- words_lex.completions(word)
                 if (if (is_keyword(s)) language_context.is_outer else language_context.symbols)
                 r <- words_map.get_list(s)
               } yield r
-            if (completions.isEmpty) None
-            else Some(((word, completions), end))
-          case None => None
-        }
+            (((word, completions), end))
+          })
       }
 
     (abbrevs_result orElse words_result) match {
-      case Some(((original, completions0), end)) =>
-        val completions1 = completions0.map(decode(_))
-
+      case Some(((original, completions0), end)) if !completions0.isEmpty =>
         val range = Text.Range(- original.length, 0) + end + start
         val immediate =
           explicit ||
@@ -378,6 +377,7 @@
               Character.codePointCount(original, 0, original.length) > 1)
         val unique = completions0.length == 1
 
+        val completions1 = completions0.map(decode(_))
         val items =
           for {
             (name0, name1) <- completions0 zip completions1
@@ -404,7 +404,7 @@
         if (items.isEmpty) None
         else Some(Completion.Result(range, original, unique, items.sorted(history.ordering)))
 
-      case None => None
+      case _ => None
     }
   }
 }