allow implicit semantic completion, notably after delay that exceeds usual round-trip time;
authorwenzelm
Mon Mar 17 10:45:29 2014 +0100 (2014-03-17 ago)
changeset 56170638b29331549
parent 56169 9b0dc5c704c9
child 56171 15351577da10
allow implicit semantic completion, notably after delay that exceeds usual round-trip time;
clarified isabelle.completion action: already open popup is re-opened and thus updated;
src/Tools/jEdit/etc/options
src/Tools/jEdit/src/completion_popup.scala
src/Tools/jEdit/src/isabelle.scala
     1.1 --- a/src/Tools/jEdit/etc/options	Mon Mar 17 10:11:23 2014 +0100
     1.2 +++ b/src/Tools/jEdit/etc/options	Mon Mar 17 10:45:29 2014 +0100
     1.3 @@ -42,7 +42,7 @@
     1.4  public option jedit_completion : bool = true
     1.5    -- "enable completion popup"
     1.6  
     1.7 -public option jedit_completion_delay : real = 0.0
     1.8 +public option jedit_completion_delay : real = 0.5
     1.9    -- "delay for completion popup (seconds)"
    1.10  
    1.11  public option jedit_completion_dismiss_delay : real = 0.0
     2.1 --- a/src/Tools/jEdit/src/completion_popup.scala	Mon Mar 17 10:11:23 2014 +0100
     2.2 +++ b/src/Tools/jEdit/src/completion_popup.scala	Mon Mar 17 10:45:29 2014 +0100
     2.3 @@ -62,6 +62,16 @@
     2.4          case None => None
     2.5        }
     2.6  
     2.7 +    def action(text_area: TextArea): Boolean =
     2.8 +      apply(text_area) match {
     2.9 +        case Some(text_area_completion) =>
    2.10 +          if (text_area_completion.active_range.isDefined)
    2.11 +            text_area_completion.action(immediate = true, explicit = true)
    2.12 +          else text_area_completion.action()
    2.13 +          true
    2.14 +        case None => false
    2.15 +      }
    2.16 +
    2.17      def exit(text_area: JEditTextArea)
    2.18      {
    2.19        Swing_Thread.require()
    2.20 @@ -180,7 +190,7 @@
    2.21      }
    2.22  
    2.23  
    2.24 -    /* completion action */
    2.25 +    /* completion action: text area */
    2.26  
    2.27      private def insert(item: Completion.Item)
    2.28      {
    2.29 @@ -247,25 +257,22 @@
    2.30        }
    2.31  
    2.32        def semantic_completion(): Option[Completion.Result] =
    2.33 -        if (explicit) {
    2.34 -          PIDE.document_view(text_area) match {
    2.35 -            case Some(doc_view) =>
    2.36 -              val rendering = doc_view.get_rendering()
    2.37 -              rendering.completion_names(before_caret_range(rendering)) match {
    2.38 -                case Some(names) =>
    2.39 -                  if (names.no_completion)
    2.40 -                    Some(Completion.Result.empty(names.range))
    2.41 -                  else
    2.42 -                    JEdit_Lib.try_get_text(buffer, names.range) match {
    2.43 -                      case Some(original) => names.complete(history, decode, original)
    2.44 -                      case None => None
    2.45 -                    }
    2.46 -                case None => None
    2.47 -              }
    2.48 -            case None => None
    2.49 -          }
    2.50 +        PIDE.document_view(text_area) match {
    2.51 +          case Some(doc_view) =>
    2.52 +            val rendering = doc_view.get_rendering()
    2.53 +            rendering.completion_names(before_caret_range(rendering)) match {
    2.54 +              case Some(names) =>
    2.55 +                if (names.no_completion)
    2.56 +                  Some(Completion.Result.empty(names.range))
    2.57 +                else
    2.58 +                  JEdit_Lib.try_get_text(buffer, names.range) match {
    2.59 +                    case Some(original) => names.complete(history, decode, original)
    2.60 +                    case None => None
    2.61 +                  }
    2.62 +              case None => None
    2.63 +            }
    2.64 +          case None => None
    2.65          }
    2.66 -        else None
    2.67  
    2.68        if (buffer.isEditable) {
    2.69          semantic_completion() orElse syntax_completion(explicit) match {
    2.70 @@ -401,7 +408,7 @@
    2.71      }
    2.72  
    2.73  
    2.74 -    /* completion action */
    2.75 +    /* completion action: text field */
    2.76  
    2.77      def action()
    2.78      {
     3.1 --- a/src/Tools/jEdit/src/isabelle.scala	Mon Mar 17 10:11:23 2014 +0100
     3.2 +++ b/src/Tools/jEdit/src/isabelle.scala	Mon Mar 17 10:45:29 2014 +0100
     3.3 @@ -247,11 +247,8 @@
     3.4  
     3.5    def complete(view: View)
     3.6    {
     3.7 -    Completion_Popup.Text_Area(view.getTextArea) match {
     3.8 -      case Some(text_area_completion) =>
     3.9 -        text_area_completion.action(immediate = true, explicit = true)
    3.10 -      case None => CompleteWord.completeWord(view)
    3.11 -    }
    3.12 +    if (!Completion_Popup.Text_Area.action(view.getTextArea))
    3.13 +      CompleteWord.completeWord(view)
    3.14    }
    3.15  
    3.16