diff -r 8662b9b1f123 -r 09270033330e src/Tools/jEdit/plugin/Isabelle.props --- a/src/Tools/jEdit/plugin/Isabelle.props Wed Dec 01 20:34:40 2010 +0100 +++ b/src/Tools/jEdit/plugin/Isabelle.props Wed Dec 01 21:07:50 2010 +0100 @@ -32,7 +32,7 @@ options.isabelle.tooltip-margin.title=Tooltip Margin options.isabelle.tooltip-margin=40 options.isabelle.tooltip-dismiss-delay.title=Tooltip Dismiss Delay (global) -options.isabelle.tooltip-dismiss-delay=8000 +options.isabelle.tooltip-dismiss-delay=8.0 options.isabelle.startup-timeout=10.0 options.isabelle.auto-start.title=Auto Start options.isabelle.auto-start=true