# 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