src/Tools/jEdit/etc/options
changeset 49245 cb70157293c0
child 49250 332ab3748350
equal deleted inserted replaced
49244:fb669aff821e 49245:cb70157293c0
       
     1 (* :mode=isabelle-options: *)
       
     2 
       
     3 option jedit_logic : string = ""
       
     4   -- "default logic session"
       
     5 
       
     6 option jedit_auto_start : bool = true
       
     7   -- "auto-start prover session on editor startup"
       
     8 
       
     9 option jedit_relative_font_size : int = 100
       
    10   -- "relative font size of output panel wrt. main text area"
       
    11 
       
    12 option jedit_tooltip_font_size : int = 10
       
    13   -- "tooltip font size (according to HTML)"
       
    14 
       
    15 option jedit_tooltip_margin : int = 60
       
    16   -- "margin for tooltip pretty-printing (in characters)"
       
    17 
       
    18 option jedit_tooltip_dismiss_delay : real = 8.0
       
    19   -- "global delay for Swing tooltips (in seconds)"