# HG changeset patch
# User wenzelm
# Date 1245784494 -7200
# Node ID 71fb6ab6ec57ab55c7e2e6789f7dc5c40a88af1a
# Parent  5a03dc7a19e17590e6eea337e1bf2cfd461702c2
default sidekick.complete-delay;

diff -r 5a03dc7a19e1 -r 71fb6ab6ec57 src/Tools/jEdit/dist-template/properties/jedit.props
--- a/src/Tools/jEdit/dist-template/properties/jedit.props	Tue Jun 23 20:49:56 2009 +0200
+++ b/src/Tools/jEdit/dist-template/properties/jedit.props	Tue Jun 23 21:14:54 2009 +0200
@@ -25,6 +25,7 @@
 view.showToolbar=false
 buffer.sidekick.keystroke-parse=true
 sidekick.buffer-save-parse=true
+sidekick.complete-delay=300
 mode.isabelle.sidekick.showStatusWindow.label=true
 sidekick-tree.dock-position=right
 isabelle-state.dock-position=bottom