--- a/src/Tools/jEdit/etc/options Sat May 03 20:20:55 2014 +0200
+++ b/src/Tools/jEdit/etc/options Sat May 03 20:31:29 2014 +0200
@@ -42,6 +42,9 @@
public option jedit_completion : bool = true
-- "enable completion popup"
+public option jedit_completion_context : bool = true
+ -- "use semantic language context for completion"
+
public option jedit_completion_delay : real = 0.5
-- "delay for completion popup (seconds)"
--- a/src/Tools/jEdit/src/completion_popup.scala Sat May 03 20:20:55 2014 +0200
+++ b/src/Tools/jEdit/src/completion_popup.scala Sat May 03 20:31:29 2014 +0200
@@ -154,6 +154,7 @@
val context =
(for {
rendering <- opt_rendering
+ if PIDE.options.bool("jedit_completion_context")
range = JEdit_Lib.before_caret_range(text_area, rendering)
context <- rendering.language_context(range)
} yield context) getOrElse syntax.language_context