src/Tools/jEdit/src/Isabelle.props
changeset 45446 d29d73117b73
parent 44865 679f0d57e831
child 48014 63021e59cbf0
equal deleted inserted replaced
45445:41e641a870de 45446:d29d73117b73
    28 options.isabelle.relative-font-size.title=Relative Font Size
    28 options.isabelle.relative-font-size.title=Relative Font Size
    29 options.isabelle.relative-font-size=100
    29 options.isabelle.relative-font-size=100
    30 options.isabelle.tooltip-font-size.title=Tooltip Font Size
    30 options.isabelle.tooltip-font-size.title=Tooltip Font Size
    31 options.isabelle.tooltip-font-size=10
    31 options.isabelle.tooltip-font-size=10
    32 options.isabelle.tooltip-margin.title=Tooltip Margin
    32 options.isabelle.tooltip-margin.title=Tooltip Margin
    33 options.isabelle.tooltip-margin=40
    33 options.isabelle.tooltip-margin=60
    34 options.isabelle.tooltip-dismiss-delay.title=Tooltip Dismiss Delay (global)
    34 options.isabelle.tooltip-dismiss-delay.title=Tooltip Dismiss Delay (global)
    35 options.isabelle.tooltip-dismiss-delay=8.0
    35 options.isabelle.tooltip-dismiss-delay=8.0
    36 options.isabelle.startup-timeout=25.0
    36 options.isabelle.startup-timeout=25.0
    37 options.isabelle.auto-start.title=Auto Start
    37 options.isabelle.auto-start.title=Auto Start
    38 options.isabelle.auto-start=true
    38 options.isabelle.auto-start=true