# HG changeset patch
# User wenzelm
# Date 1377860368 -7200
# Node ID c12a3edcd8e4c98b086ab98a93dd95bfa1607bc8
# Parent  5fa77d6ad63d0dbb3a2ee700d3443c49e3c24ff8
explicit is always immediate;

diff -r 5fa77d6ad63d -r c12a3edcd8e4 src/Pure/Isar/completion.scala
--- a/src/Pure/Isar/completion.scala	Fri Aug 30 12:46:32 2013 +0200
+++ b/src/Pure/Isar/completion.scala	Fri Aug 30 12:59:28 2013 +0200
@@ -121,7 +121,7 @@
           val immediate =
             !Completion.is_word(word) &&
             Character.codePointCount(word, 0, word.length) > 1
-          Some((word, ds.map(s => Completion.Item(word, s, s, immediate))))
+          Some((word, ds.map(s => Completion.Item(word, s, s, explicit || immediate))))
         }
       case None => None
     }