allow empty original, e.g. path "";
authorwenzelm
Mon, 05 May 2014 11:53:07 +0200
changeset 56863 5fdb61a9a010
parent 56862 e6f7ed54d64e
child 56864 0446c7ac2e32
allow empty original, e.g. path "";
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 =>