# HG changeset patch
# User wenzelm
# Date 1377764683 -7200
# Node ID 473ea1ed7503b80f4e8e40e229c0a10ba5e58e44
# Parent  0dfd78ff76961c9f27898e45f26972af0ebd949d
some completion options;

diff -r 0dfd78ff7696 -r 473ea1ed7503 NEWS
--- a/NEWS	Thu Aug 29 10:01:59 2013 +0200
+++ b/NEWS	Thu Aug 29 10:24:43 2013 +0200
@@ -90,10 +90,11 @@
 according to Isabelle/Scala plugin option "jedit_font_reset_size"
 (cf. keyboard shortcut C+0).
 
-* More reactive and less intrusive completion.  Plain words need to be
-at least 3 characters long to be completed (was 2 before).  Symbols
-are only completed in backslash forms, e.g. \forall or \<forall> that
-both produce the Isabelle symbol \<forall> in its Unicode rendering.
+* More reactive and less intrusive completion, managed by
+Isabelle/jEdit instead of SideKick.  Plain words need to be at least 3
+characters long to be completed (was 2 before).  Symbols are only
+completed in backslash forms, e.g. \forall or \<forall> that both
+produce the Isabelle symbol \<forall> in its Unicode rendering.
 
 * Improved support for Linux look-and-feel "GTK+", see also "Utilities
 / Global Options / Appearance".
diff -r 0dfd78ff7696 -r 473ea1ed7503 src/Tools/jEdit/etc/options
--- a/src/Tools/jEdit/etc/options	Thu Aug 29 10:01:59 2013 +0200
+++ b/src/Tools/jEdit/etc/options	Thu Aug 29 10:24:43 2013 +0200
@@ -16,7 +16,7 @@
   -- "relative bounds of popup window wrt. logical screen size"
 
 public option jedit_tooltip_delay : real = 0.75
-  -- "open/close delay for document tooltips"
+  -- "open/close delay for document tooltips (seconds)"
 
 public option jedit_tooltip_margin : int = 60
   -- "margin for tooltip pretty-printing"
@@ -33,6 +33,12 @@
 public option jedit_timing_threshold : real = 0.1
   -- "default threshold for timing display"
 
+public option jedit_completion : bool = true
+  -- "enable completion popup"
+
+public option jedit_completion_delay : real = 0.0
+  -- "delay for completion popup (seconds)"
+
 
 section "Rendering of Document Content"
 
diff -r 0dfd78ff7696 -r 473ea1ed7503 src/Tools/jEdit/src/completion_popup.scala
--- a/src/Tools/jEdit/src/completion_popup.scala	Thu Aug 29 10:01:59 2013 +0200
+++ b/src/Tools/jEdit/src/completion_popup.scala	Thu Aug 29 10:24:43 2013 +0200
@@ -38,6 +38,8 @@
 
   class Text_Area private(text_area: JEditTextArea, get_syntax: => Option[Outer_Syntax])
   {
+    /* popup state */
+
     private var completion_popup: Option[Completion_Popup] = None
 
     def dismissed(): Boolean =
@@ -54,6 +56,9 @@
       }
     }
 
+
+    /* insert selected item */
+
     private def insert(item: Item)
     {
       Swing_Thread.require()
@@ -73,65 +78,83 @@
       }
     }
 
+
+    /* input of key events */
+
     def input(evt: KeyEvent)
     {
       Swing_Thread.require()
 
-      val view = text_area.getView
-      val layered = view.getLayeredPane
-      val buffer = text_area.getBuffer
-      val painter = text_area.getPainter
-
-      if (buffer.isEditable && !evt.isConsumed) {
-        dismissed()
-
-        get_syntax match {
-          case Some(syntax) =>
-            val caret = text_area.getCaretPosition
-            val result =
-            {
-              val line = buffer.getLineOfOffset(caret)
-              val start = buffer.getLineStartOffset(line)
-              val text = buffer.getSegment(start, caret - start)
-
-              syntax.completion.complete(text) match {
-                case Some((word, cs)) =>
-                  val ds =
-                    (if (Isabelle_Encoding.is_active(buffer))
-                      cs.map(Symbol.decode(_)).sorted
-                     else cs).filter(_ != word)
-                  if (ds.isEmpty) None
-                  else Some((word, ds.map(s => Item(word, s, s))))
-                case None => None
-              }
-            }
-            result match {
-              case Some((original, items)) =>
-                val font = painter.getFont.deriveFont(Rendering.font_size("jedit_popup_font_scale"))
-
-                val loc1 = text_area.offsetToXY(caret - original.length)
-                if (loc1 != null) {
-                  val loc2 =
-                    SwingUtilities.convertPoint(painter,
-                      loc1.x, loc1.y + painter.getFontMetrics.getHeight, layered)
-                  val completion =
-                    new Completion_Popup(layered, loc2, font, items) {
-                      override def complete(item: Item) { insert(item) }
-                      override def propagate(e: KeyEvent) {
-                        JEdit_Lib.propagate_key(view, e)
-                        input(e)
-                      }
-                      override def refocus() { text_area.requestFocus }
-                    }
-                  completion_popup = Some(completion)
-                  completion.show_popup()
-                }
-              case None =>
-            }
-          case None =>
+      if (PIDE.options.bool("jedit_completion")) {
+        if (!evt.isConsumed) {
+          dismissed()
+          input_delay.invoke()
         }
       }
+      else {
+        dismissed()
+        input_delay.revoke()
+      }
     }
+
+    private val input_delay =
+      Swing_Thread.delay_last(PIDE.options.seconds("jedit_completion_delay"))
+      {
+        val view = text_area.getView
+        val layered = view.getLayeredPane
+        val buffer = text_area.getBuffer
+        val painter = text_area.getPainter
+
+        if (buffer.isEditable) {
+          get_syntax match {
+            case Some(syntax) =>
+              val caret = text_area.getCaretPosition
+              val result =
+              {
+                val line = buffer.getLineOfOffset(caret)
+                val start = buffer.getLineStartOffset(line)
+                val text = buffer.getSegment(start, caret - start)
+
+                syntax.completion.complete(text) match {
+                  case Some((word, cs)) =>
+                    val ds =
+                      (if (Isabelle_Encoding.is_active(buffer))
+                        cs.map(Symbol.decode(_)).sorted
+                       else cs).filter(_ != word)
+                    if (ds.isEmpty) None
+                    else Some((word, ds.map(s => Item(word, s, s))))
+                  case None => None
+                }
+              }
+              result match {
+                case Some((original, items)) =>
+                  val font =
+                    painter.getFont.deriveFont(Rendering.font_size("jedit_popup_font_scale"))
+
+                  val loc1 = text_area.offsetToXY(caret - original.length)
+                  if (loc1 != null) {
+                    val loc2 =
+                      SwingUtilities.convertPoint(painter,
+                        loc1.x, loc1.y + painter.getFontMetrics.getHeight, layered)
+
+                    val completion =
+                      new Completion_Popup(layered, loc2, font, items) {
+                        override def complete(item: Item) { insert(item) }
+                        override def propagate(e: KeyEvent) {
+                          JEdit_Lib.propagate_key(view, e)
+                          input(e)
+                        }
+                        override def refocus() { text_area.requestFocus }
+                      }
+                    completion_popup = Some(completion)
+                    completion.show_popup()
+                  }
+                case None =>
+              }
+            case None =>
+          }
+        }
+      }
   }
 }