jedit_completion_immediate is enabled by default: let all users participate in slightly more ambitious symbol insertion;
--- 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}).
--- 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"