src/Tools/jEdit/etc/options
author wenzelm
Thu, 31 Jan 2013 22:21:05 +0100
changeset 51071 b7e7557e80b5
parent 50554 0493efcc97e9
child 51441 37f699750430
permissions -rw-r--r--
some native Mac OS X support, notably quit_handler (important for dialog on unsaved changes);

(* :mode=isabelle-options: *)

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

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

option jedit_tooltip_font_scale : real = 0.85
  -- "scale factor of tooltips wrt. main text area"

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

option jedit_tooltip_bounds : real = 0.5
  -- "relative bounds of tooltip window wrt. logical screen size"

option jedit_text_overview_limit : int = 100000
  -- "maximum amount of text to visualize in overview column"

option jedit_symbols_search_limit : int = 50
  -- "maximum number of symbols in search result"

option jedit_mac_adapter : bool = true
  -- "some native Mac OS X support (potential conflict with MacOSX plugin)"


section "Rendering of Document Content"

option outdated_color : string = "EEE3E3FF"
option unprocessed_color : string = "FFA0A0FF"
option unprocessed1_color : string = "FFA0A032"
option running_color : string = "610061FF"
option running1_color : string = "61006164"
option light_color : string = "F0F0F0FF"
option tooltip_color : string = "FFFFE9FF"
option writeln_color : string = "C0C0C0FF"
option warning_color : string = "FF8C00FF"
option error_color : string = "B22222FF"
option error1_color : string = "B2222232"
option writeln_message_color : string = "F0F0F0FF"
option tracing_message_color : string = "F0F8FFFF"
option warning_message_color : string = "EEE8AAFF"
option error_message_color : string = "FFC1C1FF"
option bad_color : string = "FF6A6A64"
option intensify_color : string = "FFCC6664"
option quoted_color : string = "8B8B8B19"
option highlight_color : string = "50505032"
option hyperlink_color : string = "000000FF"
option active_color : string = "DCDCDCFF"
option active_hover_color : string = "9DC75DFF"
option active_result_color : string = "999966FF"
option keyword1_color : string = "006699FF"
option keyword2_color : string = "009966FF"

option tfree_color : string = "A020F0FF"
option tvar_color : string = "A020F0FF"
option free_color : string = "0000FFFF"
option skolem_color : string = "D2691EFF"
option bound_color : string = "008000FF"
option var_color : string = "00009BFF"
option inner_numeral_color : string = "FF0000FF"
option inner_quoted_color : string = "D2691EFF"
option inner_comment_color : string = "8B0000FF"
option antiquotation_color : string = "0000FFFF"
option dynamic_color : string = "7BA428FF"