yet another completion option, to imitate old less ambitious behavior;
authorwenzelm
Sat, 03 May 2014 20:31:29 +0200
changeset 56842 b6e266574b26
parent 56841 bc6faeadbf82
child 56843 b2bfcd8cda80
yet another completion option, to imitate old less ambitious behavior;
src/Tools/jEdit/etc/options
src/Tools/jEdit/src/completion_popup.scala
--- 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