--- 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".
--- 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"
--- 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 =>
+ }
+ }
+ }
}
}