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