de-register completion first, which is important to make new popup reliably;
authorwenzelm
Tue Aug 27 22:20:11 2013 +0200 (2013-08-27 ago)
changeset 53236837a6ef61fe9
parent 53235 1b6a44859549
child 53237 6bfe54791591
de-register completion first, which is important to make new popup reliably;
src/Tools/jEdit/src/completion_popup.scala
     1.1 --- a/src/Tools/jEdit/src/completion_popup.scala	Tue Aug 27 22:00:35 2013 +0200
     1.2 +++ b/src/Tools/jEdit/src/completion_popup.scala	Tue Aug 27 22:20:11 2013 +0200
     1.3 @@ -72,6 +72,8 @@
     1.4      val buffer = text_area.getBuffer
     1.5      val painter = text_area.getPainter
     1.6  
     1.7 +    register(root, null)
     1.8 +
     1.9      if (buffer.isEditable) {
    1.10        get_syntax match {
    1.11          case Some(syntax) =>
    1.12 @@ -83,7 +85,6 @@
    1.13              val text = buffer.getSegment(start, caret - start)
    1.14  
    1.15              syntax.completion.complete(text) match {
    1.16 -              case None => None
    1.17                case Some((word, cs)) =>
    1.18                  val ds =
    1.19                    (if (Isabelle_Encoding.is_active(buffer))
    1.20 @@ -91,6 +92,7 @@
    1.21                     else cs).filter(_ != word)
    1.22                  if (ds.isEmpty) None
    1.23                  else Some((word, ds.map(s => Item(word, s, s))))
    1.24 +              case None => None
    1.25              }
    1.26            }
    1.27            result match {
    1.28 @@ -116,13 +118,11 @@
    1.29                    }
    1.30                  register(root, completion)
    1.31                }
    1.32 -              else register(root, null)
    1.33 -            case None => register(root, null)
    1.34 +            case None =>
    1.35            }
    1.36 -        case None => register(root, null)
    1.37 +        case None =>
    1.38        }
    1.39      }
    1.40 -    else register(root, null)
    1.41    }
    1.42  }
    1.43