src/Tools/jEdit/etc/options
author wenzelm
Tue, 11 Sep 2012 19:19:39 +0200
changeset 49288 2c9272cb4568
parent 49272 97f8cb455691
child 49294 a600c017f814
permissions -rw-r--r--
more options;

(* :mode=isabelle-options: *)

option jedit_logic : string = ""
  -- "default logic session"

option jedit_auto_start : bool = true
  -- "auto-start prover session on editor startup"

option jedit_font_scale : real = 1.0
  -- "scale factor of add-on panels wrt. main text area"

option jedit_tooltip_font_size : int = 10
  -- "tooltip font size (according to HTML)"

option jedit_tooltip_margin : int = 60
  -- "margin for tooltip pretty-printing"

option jedit_tooltip_dismiss_delay : real = 8.0
  -- "global delay for Swing tooltips"