# HG changeset patch
# User wenzelm
# Date 1396961815 -7200
# Node ID 08982abdcdad7a0b9607b37074e2282074d9bfe5
# Parent  6ad693903e2209c5a94fdceb984ce33b085008ce
obsolete;

diff -r 6ad693903e22 -r 08982abdcdad src/Doc/JEdit/JEdit.thy
--- 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