src/Tools/jEdit/src/completion_popup.scala
changeset 56175 79c29244b377
parent 56173 62f10624339a
child 56177 bfa9dfb722de
equal deleted inserted replaced
56174:23ec13bb3db6 56175:79c29244b377
   138           val buffer = text_area.getBuffer
   138           val buffer = text_area.getBuffer
   139           if (line_range.contains(text_area.getCaretPosition)) {
   139           if (line_range.contains(text_area.getCaretPosition)) {
   140             before_caret_range(rendering).try_restrict(line_range) match {
   140             before_caret_range(rendering).try_restrict(line_range) match {
   141               case Some(range) if !range.is_singularity =>
   141               case Some(range) if !range.is_singularity =>
   142                 rendering.semantic_completion(range) match {
   142                 rendering.semantic_completion(range) match {
   143                   case Some(semantic) =>
   143                   case Some(Text.Info(_, Completion.No_Completion)) => None
   144                     if (semantic.info.no_completion) None
   144                   case Some(Text.Info(range1, _: Completion.Names)) => Some(range1)
   145                     else Some(semantic.range)
       
   146                   case None =>
   145                   case None =>
   147                     syntax_completion(false, Some(rendering)) match {
   146                     syntax_completion(Completion.History.empty, false, Some(rendering)).map(_.range)
   148                       case Some(result) => Some(result.range)
       
   149                       case None => None
       
   150                     }
       
   151                 }
   147                 }
   152               case _ => None
   148               case _ => None
   153             }
   149             }
   154           }
   150           }
   155           else None
   151           else None
   158 
   154 
   159 
   155 
   160     /* syntax completion */
   156     /* syntax completion */
   161 
   157 
   162     def syntax_completion(
   158     def syntax_completion(
   163       explicit: Boolean, opt_rendering: Option[Rendering] = None): Option[Completion.Result] =
   159       history: Completion.History,
       
   160       explicit: Boolean,
       
   161       opt_rendering: Option[Rendering]): Option[Completion.Result] =
   164     {
   162     {
   165       val buffer = text_area.getBuffer
   163       val buffer = text_area.getBuffer
   166       val history = PIDE.completion_history.value
       
   167       val decode = Isabelle_Encoding.is_active(buffer)
   164       val decode = Isabelle_Encoding.is_active(buffer)
   168 
   165 
   169       Isabelle.mode_syntax(JEdit_Lib.buffer_mode(buffer)) match {
   166       Isabelle.mode_syntax(JEdit_Lib.buffer_mode(buffer)) match {
   170         case Some(syntax) =>
   167         case Some(syntax) =>
   171           val caret = text_area.getCaretPosition
   168           val caret = text_area.getCaretPosition
   174           val line_start = buffer.getLineStartOffset(line)
   171           val line_start = buffer.getLineStartOffset(line)
   175           val line_length = (buffer.getLineEndOffset(line) min buffer.getLength) - line_start
   172           val line_length = (buffer.getLineEndOffset(line) min buffer.getLength) - line_start
   176           val line_text = buffer.getSegment(line_start, line_length)
   173           val line_text = buffer.getSegment(line_start, line_length)
   177 
   174 
   178           val context =
   175           val context =
   179             (opt_rendering orElse PIDE.document_view(text_area).map(_.get_rendering()) match {
   176             (opt_rendering match {
   180               case Some(rendering) =>
   177               case Some(rendering) =>
   181                 rendering.language_context(before_caret_range(rendering))
   178                 rendering.language_context(before_caret_range(rendering))
   182               case None => None
   179               case None => None
   183             }) getOrElse syntax.language_context
   180             }) getOrElse syntax.language_context
   184 
   181 
   254           invalidate()
   251           invalidate()
   255           completion.show_popup()
   252           completion.show_popup()
   256         }
   253         }
   257       }
   254       }
   258 
   255 
   259       def semantic_completion(): Option[Completion.Result] =
       
   260         PIDE.document_view(text_area) match {
       
   261           case Some(doc_view) =>
       
   262             val rendering = doc_view.get_rendering()
       
   263             rendering.semantic_completion(before_caret_range(rendering)) match {
       
   264               case Some(semantic) =>
       
   265                 if (semantic.info.no_completion)
       
   266                   Some(Completion.Result.empty(semantic.range))
       
   267                 else
       
   268                   JEdit_Lib.try_get_text(buffer, semantic.range) match {
       
   269                     case Some(original) =>
       
   270                       semantic.info.complete(semantic.range, history, decode, original)
       
   271                     case None => None
       
   272                   }
       
   273               case None => None
       
   274             }
       
   275           case None => None
       
   276         }
       
   277 
       
   278       if (buffer.isEditable) {
   256       if (buffer.isEditable) {
   279         semantic_completion() orElse syntax_completion(explicit) match {
   257         val (no_completion, semantic_completion, opt_rendering) =
   280           case Some(result) =>
   258         {
   281             result.items match {
   259           PIDE.document_view(text_area) match {
   282               case List(item) if result.unique && item.immediate && immediate =>
   260             case Some(doc_view) =>
   283                 insert(item)
   261               val rendering = doc_view.get_rendering()
   284               case _ :: _ =>
   262               val (no_completion, result) =
   285                 open_popup(result)
   263                 rendering.semantic_completion(before_caret_range(rendering)) match {
   286               case _ =>
   264                   case Some(Text.Info(_, Completion.No_Completion)) =>
   287             }
   265                     (true, None)
   288           case None =>
   266                   case Some(Text.Info(range, names: Completion.Names)) =>
       
   267                     val result =
       
   268                       JEdit_Lib.try_get_text(buffer, range) match {
       
   269                         case Some(original) => names.complete(range, history, decode, original)
       
   270                         case None => None
       
   271                       }
       
   272                     (false, result)
       
   273                   case None =>
       
   274                     (false, None)
       
   275                 }
       
   276               (no_completion, result, Some(rendering))
       
   277             case None =>
       
   278               (false, None, None)
       
   279           }
       
   280         }
       
   281         if (!no_completion) {
       
   282           val result =
       
   283             Completion.Result.merge(history,
       
   284               semantic_completion, syntax_completion(history, explicit, opt_rendering))
       
   285 
       
   286           result match {
       
   287             case Some(result) =>
       
   288               result.items match {
       
   289                 case List(item) if result.unique && item.immediate && immediate =>
       
   290                   insert(item)
       
   291                 case _ :: _ =>
       
   292                   open_popup(result)
       
   293                 case _ =>
       
   294               }
       
   295             case None =>
       
   296           }
   289         }
   297         }
   290       }
   298       }
   291     }
   299     }
   292 
   300 
   293 
   301