some completion options;
authorwenzelm
Thu Aug 29 10:24:43 2013 +0200 (2013-08-29 ago)
changeset 53273473ea1ed7503
parent 53272 0dfd78ff7696
child 53274 1760c01f1c78
some completion options;
NEWS
src/Tools/jEdit/etc/options
src/Tools/jEdit/src/completion_popup.scala
     1.1 --- a/NEWS	Thu Aug 29 10:01:59 2013 +0200
     1.2 +++ b/NEWS	Thu Aug 29 10:24:43 2013 +0200
     1.3 @@ -90,10 +90,11 @@
     1.4  according to Isabelle/Scala plugin option "jedit_font_reset_size"
     1.5  (cf. keyboard shortcut C+0).
     1.6  
     1.7 -* More reactive and less intrusive completion.  Plain words need to be
     1.8 -at least 3 characters long to be completed (was 2 before).  Symbols
     1.9 -are only completed in backslash forms, e.g. \forall or \<forall> that
    1.10 -both produce the Isabelle symbol \<forall> in its Unicode rendering.
    1.11 +* More reactive and less intrusive completion, managed by
    1.12 +Isabelle/jEdit instead of SideKick.  Plain words need to be at least 3
    1.13 +characters long to be completed (was 2 before).  Symbols are only
    1.14 +completed in backslash forms, e.g. \forall or \<forall> that both
    1.15 +produce the Isabelle symbol \<forall> in its Unicode rendering.
    1.16  
    1.17  * Improved support for Linux look-and-feel "GTK+", see also "Utilities
    1.18  / Global Options / Appearance".
     2.1 --- a/src/Tools/jEdit/etc/options	Thu Aug 29 10:01:59 2013 +0200
     2.2 +++ b/src/Tools/jEdit/etc/options	Thu Aug 29 10:24:43 2013 +0200
     2.3 @@ -16,7 +16,7 @@
     2.4    -- "relative bounds of popup window wrt. logical screen size"
     2.5  
     2.6  public option jedit_tooltip_delay : real = 0.75
     2.7 -  -- "open/close delay for document tooltips"
     2.8 +  -- "open/close delay for document tooltips (seconds)"
     2.9  
    2.10  public option jedit_tooltip_margin : int = 60
    2.11    -- "margin for tooltip pretty-printing"
    2.12 @@ -33,6 +33,12 @@
    2.13  public option jedit_timing_threshold : real = 0.1
    2.14    -- "default threshold for timing display"
    2.15  
    2.16 +public option jedit_completion : bool = true
    2.17 +  -- "enable completion popup"
    2.18 +
    2.19 +public option jedit_completion_delay : real = 0.0
    2.20 +  -- "delay for completion popup (seconds)"
    2.21 +
    2.22  
    2.23  section "Rendering of Document Content"
    2.24  
     3.1 --- a/src/Tools/jEdit/src/completion_popup.scala	Thu Aug 29 10:01:59 2013 +0200
     3.2 +++ b/src/Tools/jEdit/src/completion_popup.scala	Thu Aug 29 10:24:43 2013 +0200
     3.3 @@ -38,6 +38,8 @@
     3.4  
     3.5    class Text_Area private(text_area: JEditTextArea, get_syntax: => Option[Outer_Syntax])
     3.6    {
     3.7 +    /* popup state */
     3.8 +
     3.9      private var completion_popup: Option[Completion_Popup] = None
    3.10  
    3.11      def dismissed(): Boolean =
    3.12 @@ -54,6 +56,9 @@
    3.13        }
    3.14      }
    3.15  
    3.16 +
    3.17 +    /* insert selected item */
    3.18 +
    3.19      private def insert(item: Item)
    3.20      {
    3.21        Swing_Thread.require()
    3.22 @@ -73,65 +78,83 @@
    3.23        }
    3.24      }
    3.25  
    3.26 +
    3.27 +    /* input of key events */
    3.28 +
    3.29      def input(evt: KeyEvent)
    3.30      {
    3.31        Swing_Thread.require()
    3.32  
    3.33 -      val view = text_area.getView
    3.34 -      val layered = view.getLayeredPane
    3.35 -      val buffer = text_area.getBuffer
    3.36 -      val painter = text_area.getPainter
    3.37 -
    3.38 -      if (buffer.isEditable && !evt.isConsumed) {
    3.39 -        dismissed()
    3.40 -
    3.41 -        get_syntax match {
    3.42 -          case Some(syntax) =>
    3.43 -            val caret = text_area.getCaretPosition
    3.44 -            val result =
    3.45 -            {
    3.46 -              val line = buffer.getLineOfOffset(caret)
    3.47 -              val start = buffer.getLineStartOffset(line)
    3.48 -              val text = buffer.getSegment(start, caret - start)
    3.49 -
    3.50 -              syntax.completion.complete(text) match {
    3.51 -                case Some((word, cs)) =>
    3.52 -                  val ds =
    3.53 -                    (if (Isabelle_Encoding.is_active(buffer))
    3.54 -                      cs.map(Symbol.decode(_)).sorted
    3.55 -                     else cs).filter(_ != word)
    3.56 -                  if (ds.isEmpty) None
    3.57 -                  else Some((word, ds.map(s => Item(word, s, s))))
    3.58 -                case None => None
    3.59 -              }
    3.60 -            }
    3.61 -            result match {
    3.62 -              case Some((original, items)) =>
    3.63 -                val font = painter.getFont.deriveFont(Rendering.font_size("jedit_popup_font_scale"))
    3.64 -
    3.65 -                val loc1 = text_area.offsetToXY(caret - original.length)
    3.66 -                if (loc1 != null) {
    3.67 -                  val loc2 =
    3.68 -                    SwingUtilities.convertPoint(painter,
    3.69 -                      loc1.x, loc1.y + painter.getFontMetrics.getHeight, layered)
    3.70 -                  val completion =
    3.71 -                    new Completion_Popup(layered, loc2, font, items) {
    3.72 -                      override def complete(item: Item) { insert(item) }
    3.73 -                      override def propagate(e: KeyEvent) {
    3.74 -                        JEdit_Lib.propagate_key(view, e)
    3.75 -                        input(e)
    3.76 -                      }
    3.77 -                      override def refocus() { text_area.requestFocus }
    3.78 -                    }
    3.79 -                  completion_popup = Some(completion)
    3.80 -                  completion.show_popup()
    3.81 -                }
    3.82 -              case None =>
    3.83 -            }
    3.84 -          case None =>
    3.85 +      if (PIDE.options.bool("jedit_completion")) {
    3.86 +        if (!evt.isConsumed) {
    3.87 +          dismissed()
    3.88 +          input_delay.invoke()
    3.89          }
    3.90        }
    3.91 +      else {
    3.92 +        dismissed()
    3.93 +        input_delay.revoke()
    3.94 +      }
    3.95      }
    3.96 +
    3.97 +    private val input_delay =
    3.98 +      Swing_Thread.delay_last(PIDE.options.seconds("jedit_completion_delay"))
    3.99 +      {
   3.100 +        val view = text_area.getView
   3.101 +        val layered = view.getLayeredPane
   3.102 +        val buffer = text_area.getBuffer
   3.103 +        val painter = text_area.getPainter
   3.104 +
   3.105 +        if (buffer.isEditable) {
   3.106 +          get_syntax match {
   3.107 +            case Some(syntax) =>
   3.108 +              val caret = text_area.getCaretPosition
   3.109 +              val result =
   3.110 +              {
   3.111 +                val line = buffer.getLineOfOffset(caret)
   3.112 +                val start = buffer.getLineStartOffset(line)
   3.113 +                val text = buffer.getSegment(start, caret - start)
   3.114 +
   3.115 +                syntax.completion.complete(text) match {
   3.116 +                  case Some((word, cs)) =>
   3.117 +                    val ds =
   3.118 +                      (if (Isabelle_Encoding.is_active(buffer))
   3.119 +                        cs.map(Symbol.decode(_)).sorted
   3.120 +                       else cs).filter(_ != word)
   3.121 +                    if (ds.isEmpty) None
   3.122 +                    else Some((word, ds.map(s => Item(word, s, s))))
   3.123 +                  case None => None
   3.124 +                }
   3.125 +              }
   3.126 +              result match {
   3.127 +                case Some((original, items)) =>
   3.128 +                  val font =
   3.129 +                    painter.getFont.deriveFont(Rendering.font_size("jedit_popup_font_scale"))
   3.130 +
   3.131 +                  val loc1 = text_area.offsetToXY(caret - original.length)
   3.132 +                  if (loc1 != null) {
   3.133 +                    val loc2 =
   3.134 +                      SwingUtilities.convertPoint(painter,
   3.135 +                        loc1.x, loc1.y + painter.getFontMetrics.getHeight, layered)
   3.136 +
   3.137 +                    val completion =
   3.138 +                      new Completion_Popup(layered, loc2, font, items) {
   3.139 +                        override def complete(item: Item) { insert(item) }
   3.140 +                        override def propagate(e: KeyEvent) {
   3.141 +                          JEdit_Lib.propagate_key(view, e)
   3.142 +                          input(e)
   3.143 +                        }
   3.144 +                        override def refocus() { text_area.requestFocus }
   3.145 +                      }
   3.146 +                    completion_popup = Some(completion)
   3.147 +                    completion.show_popup()
   3.148 +                  }
   3.149 +                case None =>
   3.150 +              }
   3.151 +            case None =>
   3.152 +          }
   3.153 +        }
   3.154 +      }
   3.155    }
   3.156  }
   3.157