# HG changeset patch
# User wenzelm
# Date 1377634811 -7200
# Node ID 837a6ef61fe942b518fb4cdd3f5f197a1cd25912
# Parent  1b6a44859549438bde90eadfb12af8cf80c9f5eb
de-register completion first, which is important to make new popup reliably;

diff -r 1b6a44859549 -r 837a6ef61fe9 src/Tools/jEdit/src/completion_popup.scala
--- a/src/Tools/jEdit/src/completion_popup.scala	Tue Aug 27 22:00:35 2013 +0200
+++ b/src/Tools/jEdit/src/completion_popup.scala	Tue Aug 27 22:20:11 2013 +0200
@@ -72,6 +72,8 @@
     val buffer = text_area.getBuffer
     val painter = text_area.getPainter
 
+    register(root, null)
+
     if (buffer.isEditable) {
       get_syntax match {
         case Some(syntax) =>
@@ -83,7 +85,6 @@
             val text = buffer.getSegment(start, caret - start)
 
             syntax.completion.complete(text) match {
-              case None => None
               case Some((word, cs)) =>
                 val ds =
                   (if (Isabelle_Encoding.is_active(buffer))
@@ -91,6 +92,7 @@
                    else cs).filter(_ != word)
                 if (ds.isEmpty) None
                 else Some((word, ds.map(s => Item(word, s, s))))
+              case None => None
             }
           }
           result match {
@@ -116,13 +118,11 @@
                   }
                 register(root, completion)
               }
-              else register(root, null)
-            case None => register(root, null)
+            case None =>
           }
-        case None => register(root, null)
+        case None =>
       }
     }
-    else register(root, null)
   }
 }