# HG changeset patch
# User wenzelm
# Date 1399141889 -7200
# Node ID b6e266574b2626db184dc64937d482497474490c
# Parent  bc6faeadbf82e65caa5cb3975fcca2e123756240
yet another completion option, to imitate old less ambitious behavior;

diff -r bc6faeadbf82 -r b6e266574b26 src/Tools/jEdit/etc/options
--- 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)"
 
diff -r bc6faeadbf82 -r b6e266574b26 src/Tools/jEdit/src/completion_popup.scala
--- 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