src/Tools/jEdit/src/completion_popup.scala
changeset 55747 bef19c929ba5
parent 55712 e757e8c8d8ea
child 55748 2e1398b484aa
     1.1 --- a/src/Tools/jEdit/src/completion_popup.scala	Tue Feb 25 18:07:35 2014 +0100
     1.2 +++ b/src/Tools/jEdit/src/completion_popup.scala	Tue Feb 25 20:15:47 2014 +0100
     1.3 @@ -92,6 +92,65 @@
     1.4        }
     1.5  
     1.6  
     1.7 +    /* rendering */
     1.8 +
     1.9 +    def rendering(rendering: Rendering, line_range: Text.Range): Option[Text.Info[Color]] =
    1.10 +    {
    1.11 +      active_range match {
    1.12 +        case Some(range) => range.try_restrict(line_range)
    1.13 +        case None =>
    1.14 +          val buffer = text_area.getBuffer
    1.15 +          val caret = text_area.getCaretPosition
    1.16 +
    1.17 +          if (line_range.contains(caret)) {
    1.18 +            JEdit_Lib.stretch_point_range(buffer, caret).try_restrict(line_range) match {
    1.19 +              case Some(range) if !range.is_singularity =>
    1.20 +                rendering.completion_names(range) match {
    1.21 +                  case Some(names) => Some(names.range)
    1.22 +                  case None =>
    1.23 +                    syntax_completion(Some(rendering), false) match {
    1.24 +                      case Some(result) => Some(result.range)
    1.25 +                      case None => None
    1.26 +                    }
    1.27 +                }
    1.28 +              case _ => None
    1.29 +            }
    1.30 +          }
    1.31 +          else None
    1.32 +      }
    1.33 +    }.map(range => Text.Info(range, rendering.completion_color))
    1.34 +
    1.35 +
    1.36 +    /* syntax completion */
    1.37 +
    1.38 +    def syntax_completion(
    1.39 +      opt_rendering: Option[Rendering], explicit: Boolean): Option[Completion.Result] =
    1.40 +    {
    1.41 +      val buffer = text_area.getBuffer
    1.42 +      val history = PIDE.completion_history.value
    1.43 +      val decode = Isabelle_Encoding.is_active(buffer)
    1.44 +
    1.45 +      Isabelle.mode_syntax(JEdit_Lib.buffer_mode(buffer)) match {
    1.46 +        case Some(syntax) =>
    1.47 +          val caret = text_area.getCaretPosition
    1.48 +          val line = buffer.getLineOfOffset(caret)
    1.49 +          val start = buffer.getLineStartOffset(line)
    1.50 +          val text = buffer.getSegment(start, caret - start)
    1.51 +
    1.52 +          val context =
    1.53 +            (opt_rendering orElse PIDE.document_view(text_area).map(_.get_rendering()) match {
    1.54 +              case Some(rendering) =>
    1.55 +                rendering.completion_context(JEdit_Lib.stretch_point_range(buffer, caret))
    1.56 +              case None => None
    1.57 +            }) getOrElse syntax.completion_context
    1.58 +
    1.59 +          syntax.completion.complete(history, decode, explicit, start, text, context)
    1.60 +
    1.61 +        case None => None
    1.62 +      }
    1.63 +    }
    1.64 +
    1.65 +
    1.66      /* completion action */
    1.67  
    1.68      private def insert(item: Completion.Item)
    1.69 @@ -179,41 +238,20 @@
    1.70            }
    1.71          }
    1.72  
    1.73 -      def syntax_completion(): Boolean =
    1.74 -      {
    1.75 -        Isabelle.mode_syntax(JEdit_Lib.buffer_mode(buffer)) match {
    1.76 -          case Some(syntax) =>
    1.77 -            val line = buffer.getLineOfOffset(caret)
    1.78 -            val start = buffer.getLineStartOffset(line)
    1.79 -            val text = buffer.getSegment(start, caret - start)
    1.80 -
    1.81 -            val context =
    1.82 -              (PIDE.document_view(text_area) match {
    1.83 -                case None => None
    1.84 -                case Some(doc_view) =>
    1.85 -                  val rendering = doc_view.get_rendering()
    1.86 -                  rendering.completion_context(JEdit_Lib.stretch_point_range(buffer, caret))
    1.87 -              }) getOrElse syntax.completion_context
    1.88 -
    1.89 -            syntax.completion.complete(history, decode, explicit, start, text, context) match {
    1.90 -              case Some(result) =>
    1.91 -                result.items match {
    1.92 -                  case List(item) if result.unique && item.immediate && immediate =>
    1.93 -                    insert(item)
    1.94 -                    true
    1.95 -                  case _ :: _ =>
    1.96 -                    open_popup(result)
    1.97 -                    true
    1.98 -                  case _ => false
    1.99 -                }
   1.100 -              case None => false
   1.101 +      def syntactic_completion(): Boolean =
   1.102 +        syntax_completion(None, explicit) match {
   1.103 +          case Some(result) =>
   1.104 +            result.items match {
   1.105 +              case List(item) if result.unique && item.immediate && immediate =>
   1.106 +                insert(item); true
   1.107 +              case _ :: _ => open_popup(result); true
   1.108 +              case _ => false
   1.109              }
   1.110            case None => false
   1.111          }
   1.112 -      }
   1.113  
   1.114        if (buffer.isEditable)
   1.115 -        semantic_completion() || syntax_completion()
   1.116 +        semantic_completion() || syntactic_completion()
   1.117      }
   1.118  
   1.119