jedit_completion_immediate is enabled by default: let all users participate in slightly more ambitious symbol insertion;
authorwenzelm
Sat, 28 Jun 2014 18:02:33 +0200
changeset 57425 625a369b4f32
parent 57424 966b12f636b9
child 57426 2cd2ccd81f93
jedit_completion_immediate is enabled by default: let all users participate in slightly more ambitious symbol insertion;
src/Doc/JEdit/JEdit.thy
src/Tools/jEdit/etc/options
--- 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"