# HG changeset patch
# User wenzelm
# Date 1320961172 -3600
# Node ID d29d73117b7366911f973bd4c371fe8afff2e1df
# Parent  41e641a870de7c207849b5b75c204ba756a62685
more generous margin;

diff -r 41e641a870de -r d29d73117b73 src/Tools/jEdit/src/Isabelle.props
--- a/src/Tools/jEdit/src/Isabelle.props	Thu Nov 10 22:32:10 2011 +0100
+++ b/src/Tools/jEdit/src/Isabelle.props	Thu Nov 10 22:39:32 2011 +0100
@@ -30,7 +30,7 @@
 options.isabelle.tooltip-font-size.title=Tooltip Font Size
 options.isabelle.tooltip-font-size=10
 options.isabelle.tooltip-margin.title=Tooltip Margin
-options.isabelle.tooltip-margin=40
+options.isabelle.tooltip-margin=60
 options.isabelle.tooltip-dismiss-delay.title=Tooltip Dismiss Delay (global)
 options.isabelle.tooltip-dismiss-delay=8.0
 options.isabelle.startup-timeout=25.0