# HG changeset patch
# User wenzelm
# Date 1399283587 -7200
# Node ID 5fdb61a9a010ca3673264eb830c282ed42a168ee
# Parent  e6f7ed54d64e19c0f2e9be9e0e0cd2ef62ea3754
allow empty original, e.g. path "";

diff -r e6f7ed54d64e -r 5fdb61a9a010 src/Tools/jEdit/src/completion_popup.scala
--- a/src/Tools/jEdit/src/completion_popup.scala	Mon May 05 10:25:09 2014 +0200
+++ b/src/Tools/jEdit/src/completion_popup.scala	Mon May 05 11:53:07 2014 +0200
@@ -254,7 +254,7 @@
 
       val buffer = text_area.getBuffer
       val range = item.range
-      if (buffer.isEditable && range.length > 0) {
+      if (buffer.isEditable) {
         JEdit_Lib.buffer_edit(buffer) {
           JEdit_Lib.try_get_text(buffer, range) match {
             case Some(text) if text == item.original =>
@@ -524,7 +524,7 @@
       Swing_Thread.require {}
 
       val range = item.range
-      if (text_field.isEditable && range.length > 0) {
+      if (text_field.isEditable) {
         val content = text_field.getText
         JEdit_Lib.try_get_text(content, range) match {
           case Some(text) if text == item.original =>