src/Tools/jEdit/src/completion_popup.scala
changeset 55914 c5b752d549e3
parent 55850 7f229b0212fe
child 55978 56645c447ee9
equal deleted inserted replaced
55913:c1409c103b77 55914:c5b752d549e3
   112           val buffer = text_area.getBuffer
   112           val buffer = text_area.getBuffer
   113           if (line_range.contains(text_area.getCaretPosition)) {
   113           if (line_range.contains(text_area.getCaretPosition)) {
   114             before_caret_range(rendering).try_restrict(line_range) match {
   114             before_caret_range(rendering).try_restrict(line_range) match {
   115               case Some(range) if !range.is_singularity =>
   115               case Some(range) if !range.is_singularity =>
   116                 rendering.completion_names(range) match {
   116                 rendering.completion_names(range) match {
   117                   case Some(names) => Some(names.range)
   117                   case Some(names) =>
       
   118                     if (names.no_completion) None
       
   119                     else Some(names.range)
   118                   case None =>
   120                   case None =>
   119                     syntax_completion(false, Some(rendering)) match {
   121                     syntax_completion(false, Some(rendering)) match {
   120                       case Some(result) => Some(result.range)
   122                       case Some(result) => Some(result.range)
   121                       case None => None
   123                       case None => None
   122                     }
   124                     }
   230         if (explicit) {
   232         if (explicit) {
   231           PIDE.document_view(text_area) match {
   233           PIDE.document_view(text_area) match {
   232             case Some(doc_view) =>
   234             case Some(doc_view) =>
   233               val rendering = doc_view.get_rendering()
   235               val rendering = doc_view.get_rendering()
   234               rendering.completion_names(before_caret_range(rendering)) match {
   236               rendering.completion_names(before_caret_range(rendering)) match {
       
   237                 case Some(names) =>
       
   238                   if (names.no_completion)
       
   239                     Some(Completion.Result.empty(names.range))
       
   240                   else
       
   241                     JEdit_Lib.try_get_text(buffer, names.range) match {
       
   242                       case Some(original) => names.complete(history, decode, original)
       
   243                       case None => None
       
   244                     }
   235                 case None => None
   245                 case None => None
   236                 case Some(names) =>
       
   237                   JEdit_Lib.try_get_text(buffer, names.range) match {
       
   238                     case Some(original) => names.complete(history, decode, original)
       
   239                     case None => None
       
   240                   }
       
   241               }
   246               }
   242             case None => None
   247             case None => None
   243           }
   248           }
   244         }
   249         }
   245         else None
   250         else None