# HG changeset patch
# User wenzelm
# Date 1403971353 -7200
# Node ID 625a369b4f325dd8cd623b1a8fc34584450eabd9
# Parent  966b12f636b96c7efc64e45efcfac26524397859
jedit_completion_immediate is enabled by default: let all users participate in slightly more ambitious symbol insertion;

diff -r 966b12f636b9 -r 625a369b4f32 src/Doc/JEdit/JEdit.thy
--- a/src/Doc/JEdit/JEdit.thy	Sat Jun 28 17:54:34 2014 +0200
+++ b/src/Doc/JEdit/JEdit.thy	Sat Jun 28 18:02:33 2014 +0200
@@ -1265,7 +1265,7 @@
   information, notably the context (\secref{sec:completion-context}).
 
   \item The system option @{system_option_ref jedit_completion_immediate}
-  (disabled by default) controls whether replacement text should be inserted
+  (enabled by default) controls whether replacement text should be inserted
   immediately without popup, regardless of @{system_option
   jedit_completion_delay}. This aggressive mode of completion is restricted to
   Isabelle symbols and their abbreviations (\secref{sec:symbols}).
diff -r 966b12f636b9 -r 625a369b4f32 src/Tools/jEdit/etc/options
--- a/src/Tools/jEdit/etc/options	Sat Jun 28 17:54:34 2014 +0200
+++ b/src/Tools/jEdit/etc/options	Sat Jun 28 18:02:33 2014 +0200
@@ -48,7 +48,7 @@
 public option jedit_completion_delay : real = 0.5
   -- "delay for completion popup (seconds)"
 
-public option jedit_completion_immediate : bool = false
+public option jedit_completion_immediate : bool = true
   -- "insert uniquely completed abbreviation immediately into buffer"
 
 public option jedit_completion_path_ignore : string = "*~:*.marks:*.orig:*.rej:.DS_Store"