--- a/src/Doc/JEdit/JEdit.thy Tue Apr 08 14:15:48 2014 +0200
+++ b/src/Doc/JEdit/JEdit.thy Tue Apr 08 14:56:55 2014 +0200
@@ -564,13 +564,6 @@
determines an additional delay (0.0 by default), before opening a
completion popup.
- \item The system option @{system_option
- jedit_completion_dismiss_delay} determines an additional delay (0.0
- by default), before dismissing an earlier completion popup. A value
- like 0.1 is occasionally useful to reduce the chance of loosing key
- strokes when the speed of typing exceeds that of repainting GUI
- components.
-
\item The system option @{system_option jedit_completion_immediate}
(disabled by default) controls whether replacement text should be
inserted immediately without popup. This is restricted to Isabelle