(* :mode=isabelle-options: *)
public option jedit_logic : string = ""
-- "default logic session"
public option jedit_print_mode : string = ""
-- "default print modes for output, separated by commas (change requires restart)"
public option jedit_auto_load : bool = false
-- "load all required files automatically to resolve theory imports"
public option jedit_reset_font_size : int = 18
-- "reset font size for main text area"
public option jedit_font_scale : real = 1.0
-- "scale factor of add-on panels wrt. main text area"
public option jedit_popup_font_scale : real = 0.85
-- "scale factor of popups wrt. main text area"
public option jedit_popup_bounds : real = 0.5
-- "relative bounds of popup window wrt. logical screen size"
public option jedit_tooltip_delay : real = 0.75
-- "open/close delay for document tooltips (seconds)"
public option jedit_tooltip_margin : int = 60
-- "margin for tooltip pretty-printing"
public option jedit_text_overview_limit : int = 65536
-- "maximum amount of text to visualize in overview column"
public option jedit_symbols_search_limit : int = 50
-- "maximum number of symbols in search result"
public option jedit_timing_threshold : real = 0.1
-- "default threshold for timing display"
section "Completion"
public option jedit_completion : bool = true
-- "enable completion popup"
public option jedit_completion_delay : real = 0.5
-- "delay for completion popup (seconds)"
public option jedit_completion_immediate : bool = false
-- "insert uniquely completed abbreviation immediately into buffer"
section "Spell Checker"
public option spell_checker : bool = true
-- "enable spell-checker for prose words within document text, comments etc."
public option spell_checker_language : string = "en_US"
-- "spell-checker dictionary name"
public option spell_checker_elements : string = "words,comment,inner_comment,ML_comment,SML_comment"
-- "relevant markup elements for spell-checker, separated by commas"
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 bullet_color : string = "000000FF"
option tooltip_color : string = "FFFFE9FF"
option writeln_color : string = "C0C0C0FF"
option information_color : string = "C1DFEEFF"
option warning_color : string = "FF8C00FF"
option error_color : string = "B22222FF"
option error1_color : string = "B2222232"
option writeln_message_color : string = "F0F0F0FF"
option information_message_color : string = "C1DFEE32"
option tracing_message_color : string = "F0F8FFFF"
option warning_message_color : string = "EEE8AAFF"
option error_message_color : string = "FFC1C1FF"
option spell_checker_color : string = "0000FFFF"
option bad_color : string = "FF6A6A64"
option intensify_color : string = "FFCC6664"
option quoted_color : string = "8B8B8B19"
option antiquoted_color : string = "FFC83219"
option antiquote_color : string = "6600CCFF"
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 keyword3_color : string = "0099FFFF"
option quasi_keyword_color : string = "9966FFFF"
option improper_color : string = "FF5050FF"
option operator_color : string = "323232FF"
option caret_invisible_color : string = "50000080"
option completion_color : string = "0000FFFF"
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_cartouche_color : string = "CC6600FF"
option inner_comment_color : string = "8B0000FF"
option dynamic_color : string = "7BA428FF"
section "Icons"
option tooltip_close_icon : string = "idea-icons/actions/closeHovered.png"
option tooltip_detach_icon : string = "idea-icons/actions/nextfile.png"
option gutter_information_icon : string = "idea-icons/general/balloonInformation.png"
option gutter_warning_icon : string = "idea-icons/runConfigurations/testFailed.png"
option gutter_legacy_icon : string = "idea-icons/general/balloonWarning.png"
option gutter_error_icon : string = "idea-icons/runConfigurations/testError.png"
option process_passive_icon : string = "idea-icons/process/step_passive.png"
option process_active_icons : string = "idea-icons/process/step_1.png:idea-icons/process/step_2.png:idea-icons/process/step_3.png:idea-icons/process/step_4.png:idea-icons/process/step_5.png:idea-icons/process/step_6.png:idea-icons/process/step_7.png:idea-icons/process/step_8.png:idea-icons/process/step_9.png:idea-icons/process/step_10.png:idea-icons/process/step_11.png:idea-icons/process/step_12.png"