src/Tools/jEdit/etc/options
author wenzelm
Thu Apr 14 22:55:53 2016 +0200 (2016-04-14)
changeset 62986 9d2fae6b31cc
parent 62792 340428bebdb8
child 62988 224e8d8a4fb8
permissions -rw-r--r--
background color for entity def/ref focus;
     1 (* :mode=isabelle-options: *)
     2 
     3 public option jedit_logic : string = ""
     4   -- "default logic session"
     5 
     6 public option jedit_print_mode : string = ""
     7   -- "default print modes for output, separated by commas (change requires restart)"
     8 
     9 public option jedit_auto_load : bool = false
    10   -- "load all required files automatically to resolve theory imports"
    11 
    12 public option jedit_auto_resolve : bool = false
    13   -- "automatically resolve auxiliary files within the editor"
    14 
    15 public option jedit_reset_font_size : int = 18
    16   -- "reset main text font size"
    17 
    18 public option jedit_font_scale : real = 1.0
    19   -- "scale factor of add-on panels wrt. main text font"
    20 
    21 public option jedit_popup_font_scale : real = 0.85
    22   -- "scale factor of popups wrt. main text font"
    23 
    24 public option jedit_popup_bounds : real = 0.5
    25   -- "relative bounds of popup window wrt. logical screen size"
    26 
    27 public option jedit_tooltip_delay : real = 0.75
    28   -- "open/close delay for document tooltips (seconds)"
    29 
    30 public option jedit_tooltip_margin : int = 60
    31   -- "margin for tooltip pretty-printing"
    32 
    33 public option jedit_structure_limit : int = 1000
    34   -- "maximum number of lines to scan for language structure"
    35 
    36 public option jedit_symbols_search_limit : int = 50
    37   -- "maximum number of symbols in search result"
    38 
    39 public option jedit_timing_threshold : real = 0.1
    40   -- "default threshold for timing display (seconds)"
    41 
    42 
    43 section "Completion"
    44 
    45 public option jedit_completion : bool = true
    46   -- "enable completion popup"
    47 
    48 public option jedit_completion_select_enter : bool = false
    49   -- "select completion item via ENTER"
    50 
    51 public option jedit_completion_select_tab : bool = true
    52   -- "select completion item via TAB"
    53 
    54 public option jedit_completion_context : bool = true
    55   -- "use semantic language context for completion"
    56 
    57 public option jedit_completion_delay : real = 0.5
    58   -- "delay for completion popup (seconds)"
    59 
    60 public option jedit_completion_immediate : bool = true
    61   -- "insert uniquely completed abbreviation immediately into buffer"
    62 
    63 public option jedit_completion_path_ignore : string = "*~:*.marks:*.orig:*.rej:.DS_Store"
    64   -- "glob patterns to ignore in file-system path completion (separated by colons)"
    65 
    66 
    67 section "Spell Checker"
    68 
    69 public option spell_checker : bool = true
    70   -- "enable spell-checker for prose words within document text, comments etc."
    71 
    72 public option spell_checker_dictionary : string = "en"
    73   -- "spell-checker dictionary name"
    74 
    75 public option spell_checker_elements : string = "words,comment,inner_comment,ML_comment,SML_comment"
    76   -- "relevant markup elements for spell-checker, separated by commas"
    77 
    78 
    79 section "Rendering of Document Content"
    80 
    81 option outdated_color : string = "EEE3E3FF"
    82 option unprocessed_color : string = "FFA0A0FF"
    83 option unprocessed1_color : string = "FFA0A032"
    84 option running_color : string = "610061FF"
    85 option running1_color : string = "61006164"
    86 option bullet_color : string = "000000FF"
    87 option tooltip_color : string = "FFFFE9FF"
    88 option writeln_color : string = "C0C0C0FF"
    89 option information_color : string = "C1DFEEFF"
    90 option warning_color : string = "FF8C00FF"
    91 option legacy_color : string = "FF8C00FF"
    92 option error_color : string = "B22222FF"
    93 option writeln_message_color : string = "F0F0F0FF"
    94 option information_message_color : string = "DCEAF3FF"
    95 option tracing_message_color : string = "F0F8FFFF"
    96 option warning_message_color : string = "EEE8AAFF"
    97 option legacy_message_color : string = "EEE8AAFF"
    98 option error_message_color : string = "FFC1C1FF"
    99 option spell_checker_color : string = "0000FFFF"
   100 option bad_color : string = "FF6A6A64"
   101 option intensify_color : string = "FFCC6664"
   102 option entity_def_color : string = "CCD9FFA0"
   103 option entity_ref_color : string = "E6FFCCA0"
   104 option breakpoint_disabled_color : string = "CCCC0080"
   105 option breakpoint_enabled_color : string = "FF9966FF"
   106 option quoted_color : string = "8B8B8B19"
   107 option antiquoted_color : string = "FFC83219"
   108 option antiquote_color : string = "6600CCFF"
   109 option highlight_color : string = "50505032"
   110 option hyperlink_color : string = "000000FF"
   111 option active_color : string = "DCDCDCFF"
   112 option active_hover_color : string = "9DC75DFF"
   113 option active_result_color : string = "999966FF"
   114 option keyword1_color : string = "006699FF"
   115 option keyword2_color : string = "009966FF"
   116 option keyword3_color : string = "0099FFFF"
   117 option quasi_keyword_color : string = "9966FFFF"
   118 option improper_color : string = "FF5050FF"
   119 option operator_color : string = "323232FF"
   120 option caret_debugger_color : string = "FF9966FF"
   121 option caret_invisible_color : string = "50000080"
   122 option completion_color : string = "0000FFFF"
   123 option search_color : string = "66FFFF64"
   124 
   125 option tfree_color : string = "A020F0FF"
   126 option tvar_color : string = "A020F0FF"
   127 option free_color : string = "0000FFFF"
   128 option skolem_color : string = "D2691EFF"
   129 option bound_color : string = "008000FF"
   130 option var_color : string = "00009BFF"
   131 option inner_numeral_color : string = "FF0000FF"
   132 option inner_quoted_color : string = "FF00CCFF"
   133 option inner_cartouche_color : string = "CC6600FF"
   134 option inner_comment_color : string = "CC0000FF"
   135 option dynamic_color : string = "7BA428FF"
   136 
   137 option markdown_item_color1 : string = "DAFEDAFF"
   138 option markdown_item_color2 : string = "FFF0CCFF"
   139 option markdown_item_color3 : string = "E7E7FFFF"
   140 option markdown_item_color4 : string = "FFE0F0FF"
   141 
   142 
   143 section "Icons"
   144 
   145 option tooltip_close_icon : string = "idea-icons/actions/closeHovered.png"
   146 option tooltip_detach_icon : string = "idea-icons/actions/nextfile.png"
   147 option gutter_information_icon : string = "idea-icons/general/balloonInformation.png"
   148 option gutter_warning_icon : string = "idea-icons/runConfigurations/testFailed.png"
   149 option gutter_legacy_icon : string = "idea-icons/general/balloonWarning.png"
   150 option gutter_error_icon : string = "idea-icons/runConfigurations/testError.png"
   151 option process_passive_icon : string = "idea-icons/process/step_passive.png"
   152 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"