src/Tools/jEdit/src/completion_popup.scala
changeset 55767 96ddf9bf12ac
parent 55752 43d0e2a34c9d
child 55813 08a1c860bc12
equal deleted inserted replaced
55766:6a16443e520e 55767:96ddf9bf12ac
    90           }
    90           }
    91         case None => None
    91         case None => None
    92       }
    92       }
    93 
    93 
    94 
    94 
       
    95     /* caret */
       
    96 
       
    97     def before_caret_range(rendering: Rendering): Text.Range =
       
    98     {
       
    99       val snapshot = rendering.snapshot
       
   100       val former_caret = snapshot.revert(text_area.getCaretPosition)
       
   101       snapshot.convert(Text.Range(former_caret - 1, former_caret))
       
   102     }
       
   103 
       
   104 
    95     /* rendering */
   105     /* rendering */
    96 
   106 
    97     def rendering(rendering: Rendering, line_range: Text.Range): Option[Text.Info[Color]] =
   107     def rendering(rendering: Rendering, line_range: Text.Range): Option[Text.Info[Color]] =
    98     {
   108     {
    99       active_range match {
   109       active_range match {
   100         case Some(range) => range.try_restrict(line_range)
   110         case Some(range) => range.try_restrict(line_range)
   101         case None =>
   111         case None =>
   102           val buffer = text_area.getBuffer
   112           val buffer = text_area.getBuffer
   103           val caret = text_area.getCaretPosition
   113           if (line_range.contains(text_area.getCaretPosition)) {
   104 
   114             before_caret_range(rendering).try_restrict(line_range) match {
   105           if (line_range.contains(caret)) {
       
   106             JEdit_Lib.stretch_point_range(buffer, caret).try_restrict(line_range) match {
       
   107               case Some(range) if !range.is_singularity =>
   115               case Some(range) if !range.is_singularity =>
   108                 rendering.completion_names(range) match {
   116                 rendering.completion_names(range) match {
   109                   case Some(names) => Some(names.range)
   117                   case Some(names) => Some(names.range)
   110                   case None =>
   118                   case None =>
   111                     syntax_completion(false, Some(rendering)) match {
   119                     syntax_completion(false, Some(rendering)) match {
   142               JEdit_Lib.try_get_text(buffer, JEdit_Lib.point_range(buffer, caret)))
   150               JEdit_Lib.try_get_text(buffer, JEdit_Lib.point_range(buffer, caret)))
   143 
   151 
   144           val context =
   152           val context =
   145             (opt_rendering orElse PIDE.document_view(text_area).map(_.get_rendering()) match {
   153             (opt_rendering orElse PIDE.document_view(text_area).map(_.get_rendering()) match {
   146               case Some(rendering) =>
   154               case Some(rendering) =>
   147                 rendering.language_context(JEdit_Lib.stretch_point_range(buffer, caret))
   155                 rendering.language_context(before_caret_range(rendering))
   148               case None => None
   156               case None => None
   149             }) getOrElse syntax.language_context
   157             }) getOrElse syntax.language_context
   150 
   158 
   151           syntax.completion.complete(history, decode, explicit, start, text, word_context, context)
   159           syntax.completion.complete(history, decode, explicit, start, text, word_context, context)
   152 
   160 
   180     {
   188     {
   181       val view = text_area.getView
   189       val view = text_area.getView
   182       val layered = view.getLayeredPane
   190       val layered = view.getLayeredPane
   183       val buffer = text_area.getBuffer
   191       val buffer = text_area.getBuffer
   184       val painter = text_area.getPainter
   192       val painter = text_area.getPainter
   185       val caret = text_area.getCaretPosition
       
   186 
   193 
   187       val history = PIDE.completion_history.value
   194       val history = PIDE.completion_history.value
   188       val decode = Isabelle_Encoding.is_active(buffer)
   195       val decode = Isabelle_Encoding.is_active(buffer)
   189 
   196 
   190       def open_popup(result: Completion.Result)
   197       def open_popup(result: Completion.Result)
   222       def semantic_completion(): Option[Completion.Result] =
   229       def semantic_completion(): Option[Completion.Result] =
   223         if (explicit) {
   230         if (explicit) {
   224           PIDE.document_view(text_area) match {
   231           PIDE.document_view(text_area) match {
   225             case Some(doc_view) =>
   232             case Some(doc_view) =>
   226               val rendering = doc_view.get_rendering()
   233               val rendering = doc_view.get_rendering()
   227               rendering.completion_names(JEdit_Lib.stretch_point_range(buffer, caret)) match {
   234               rendering.completion_names(before_caret_range(rendering)) match {
   228                 case None => None
   235                 case None => None
   229                 case Some(names) =>
   236                 case Some(names) =>
   230                   JEdit_Lib.try_get_text(buffer, names.range) match {
   237                   JEdit_Lib.try_get_text(buffer, names.range) match {
   231                     case Some(original) => names.complete(history, decode, original)
   238                     case Some(original) => names.complete(history, decode, original)
   232                     case None => None
   239                     case None => None