src/Tools/jEdit/etc/options
author wenzelm
Sat Sep 01 20:20:50 2018 +0200 (10 months ago)
changeset 68871 f5c76072db55
parent 67322 734a4e44b159
child 69320 fc221fa79741
permissions -rw-r--r--
more explicit status for "canceled" command within theory node;
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@61139
     9
public option jedit_auto_resolve : bool = false
wenzelm@64835
    10
  -- "automatically resolve auxiliary files within the document model"
wenzelm@60916
    11
wenzelm@53161
    12
public option jedit_reset_font_size : int = 18
wenzelm@59286
    13
  -- "reset main text font size"
wenzelm@53161
    14
wenzelm@52065
    15
public option jedit_font_scale : real = 1.0
wenzelm@59286
    16
  -- "scale factor of add-on panels wrt. main text font"
wenzelm@49245
    17
wenzelm@53229
    18
public option jedit_popup_font_scale : real = 0.85
wenzelm@59286
    19
  -- "scale factor of popups wrt. main text font"
wenzelm@53229
    20
wenzelm@53230
    21
public option jedit_popup_bounds : real = 0.5
wenzelm@53230
    22
  -- "relative bounds of popup window wrt. logical screen size"
wenzelm@53230
    23
wenzelm@52065
    24
public option jedit_tooltip_delay : real = 0.75
wenzelm@53273
    25
  -- "open/close delay for document tooltips (seconds)"
wenzelm@51441
    26
wenzelm@52065
    27
public option jedit_tooltip_margin : int = 60
wenzelm@49250
    28
  -- "margin for tooltip pretty-printing"
wenzelm@49245
    29
wenzelm@58750
    30
public option jedit_structure_limit : int = 1000
wenzelm@58750
    31
  -- "maximum number of lines to scan for language structure"
wenzelm@58750
    32
wenzelm@52065
    33
public option jedit_symbols_search_limit : int = 50
wenzelm@50190
    34
  -- "maximum number of symbols in search result"
wenzelm@50190
    35
wenzelm@52065
    36
public option jedit_timing_threshold : real = 0.1
wenzelm@62792
    37
  -- "default threshold for timing display (seconds)"
wenzelm@51533
    38
wenzelm@53294
    39
wenzelm@63455
    40
section "Indentation"
wenzelm@63455
    41
wenzelm@66180
    42
public option jedit_indent_input : bool = true
wenzelm@66180
    43
  -- "indentation of Isabelle keywords after input (typed character or completion)"
wenzelm@66180
    44
wenzelm@63455
    45
public option jedit_indent_newline : bool = true
wenzelm@63455
    46
  -- "indentation of Isabelle keywords on ENTER (action isabelle.newline)"
wenzelm@63455
    47
wenzelm@63474
    48
public option jedit_indent_script : bool = true
wenzelm@63474
    49
  -- "indent unstructured proof script ('apply' etc.) via number of subgoals"
wenzelm@63474
    50
wenzelm@63474
    51
public option jedit_indent_script_limit : int = 20
wenzelm@63474
    52
  -- "maximum indentation of unstructured proof script ('apply' etc.)"
wenzelm@63474
    53
wenzelm@63455
    54
wenzelm@53294
    55
section "Completion"
wenzelm@53294
    56
wenzelm@53273
    57
public option jedit_completion : bool = true
wenzelm@53273
    58
  -- "enable completion popup"
wenzelm@53273
    59
wenzelm@57833
    60
public option jedit_completion_select_enter : bool = false
wenzelm@57833
    61
  -- "select completion item via ENTER"
wenzelm@57833
    62
wenzelm@57833
    63
public option jedit_completion_select_tab : bool = true
wenzelm@57833
    64
  -- "select completion item via TAB"
wenzelm@57833
    65
wenzelm@56842
    66
public option jedit_completion_context : bool = true
wenzelm@56842
    67
  -- "use semantic language context for completion"
wenzelm@56842
    68
wenzelm@56170
    69
public option jedit_completion_delay : real = 0.5
wenzelm@53273
    70
  -- "delay for completion popup (seconds)"
wenzelm@53273
    71
wenzelm@57425
    72
public option jedit_completion_immediate : bool = true
wenzelm@56326
    73
  -- "insert uniquely completed abbreviation immediately into buffer"
wenzelm@53292
    74
wenzelm@49294
    75
wenzelm@49296
    76
section "Rendering of Document Content"
wenzelm@49294
    77
wenzelm@49355
    78
option outdated_color : string = "EEE3E3FF"
wenzelm@49355
    79
option unprocessed_color : string = "FFA0A0FF"
wenzelm@49355
    80
option unprocessed1_color : string = "FFA0A032"
wenzelm@49355
    81
option running_color : string = "610061FF"
wenzelm@49355
    82
option running1_color : string = "61006164"
wenzelm@51574
    83
option bullet_color : string = "000000FF"
wenzelm@49706
    84
option tooltip_color : string = "FFFFE9FF"
wenzelm@49355
    85
option writeln_color : string = "C0C0C0FF"
wenzelm@52650
    86
option information_color : string = "C1DFEEFF"
wenzelm@49355
    87
option warning_color : string = "FF8C00FF"
wenzelm@59203
    88
option legacy_color : string = "FF8C00FF"
wenzelm@49355
    89
option error_color : string = "B22222FF"
wenzelm@49474
    90
option writeln_message_color : string = "F0F0F0FF"
wenzelm@59129
    91
option information_message_color : string = "DCEAF3FF"
wenzelm@49418
    92
option tracing_message_color : string = "F0F8FFFF"
wenzelm@49418
    93
option warning_message_color : string = "EEE8AAFF"
wenzelm@59203
    94
option legacy_message_color : string = "EEE8AAFF"
wenzelm@49418
    95
option error_message_color : string = "FFC1C1FF"
wenzelm@56553
    96
option spell_checker_color : string = "0000FFFF"
wenzelm@49355
    97
option bad_color : string = "FF6A6A64"
wenzelm@68871
    98
option canceled_color : string = "FF6A6A64"
wenzelm@49358
    99
option intensify_color : string = "FFCC6664"
wenzelm@62988
   100
option entity_color : string = "CCD9FF80"
wenzelm@62991
   101
option entity_ref_color : string = "800080FF"
wenzelm@60914
   102
option breakpoint_disabled_color : string = "CCCC0080"
wenzelm@60914
   103
option breakpoint_enabled_color : string = "FF9966FF"
wenzelm@49355
   104
option quoted_color : string = "8B8B8B19"
wenzelm@52101
   105
option antiquoted_color : string = "FFC83219"
wenzelm@55526
   106
option antiquote_color : string = "6600CCFF"
wenzelm@49358
   107
option highlight_color : string = "50505032"
wenzelm@49355
   108
option hyperlink_color : string = "000000FF"
wenzelm@50450
   109
option active_color : string = "DCDCDCFF"
wenzelm@50450
   110
option active_hover_color : string = "9DC75DFF"
wenzelm@50499
   111
option active_result_color : string = "999966FF"
wenzelm@49355
   112
option keyword1_color : string = "006699FF"
wenzelm@49355
   113
option keyword2_color : string = "009966FF"
wenzelm@55505
   114
option keyword3_color : string = "0099FFFF"
wenzelm@55924
   115
option quasi_keyword_color : string = "9966FFFF"
wenzelm@56202
   116
option improper_color : string = "FF5050FF"
wenzelm@56064
   117
option operator_color : string = "323232FF"
wenzelm@61011
   118
option caret_debugger_color : string = "FF9966FF"
wenzelm@55726
   119
option caret_invisible_color : string = "50000080"
wenzelm@55747
   120
option completion_color : string = "0000FFFF"
wenzelm@56883
   121
option search_color : string = "66FFFF64"
wenzelm@49294
   122
wenzelm@49355
   123
option tfree_color : string = "A020F0FF"
wenzelm@49355
   124
option tvar_color : string = "A020F0FF"
wenzelm@49355
   125
option free_color : string = "0000FFFF"
wenzelm@49355
   126
option skolem_color : string = "D2691EFF"
wenzelm@49355
   127
option bound_color : string = "008000FF"
wenzelm@49355
   128
option var_color : string = "00009BFF"
wenzelm@49355
   129
option inner_numeral_color : string = "FF0000FF"
wenzelm@59120
   130
option inner_quoted_color : string = "FF00CCFF"
wenzelm@55033
   131
option inner_cartouche_color : string = "CC6600FF"
wenzelm@59120
   132
option inner_comment_color : string = "CC0000FF"
wenzelm@49355
   133
option dynamic_color : string = "7BA428FF"
wenzelm@63347
   134
option class_parameter_color : string = "D2691EFF"
wenzelm@49294
   135
wenzelm@67322
   136
option markdown_bullet1_color : string = "DAFEDAFF"
wenzelm@67322
   137
option markdown_bullet2_color : string = "FFF0CCFF"
wenzelm@67322
   138
option markdown_bullet3_color : string = "E7E7FFFF"
wenzelm@67322
   139
option markdown_bullet4_color : string = "FFE0F0FF"
wenzelm@61449
   140
wenzelm@52472
   141
wenzelm@52472
   142
section "Icons"
wenzelm@52472
   143
wenzelm@52472
   144
option tooltip_close_icon : string = "idea-icons/actions/closeHovered.png"
wenzelm@52472
   145
option tooltip_detach_icon : string = "idea-icons/actions/nextfile.png"
wenzelm@52644
   146
option gutter_information_icon : string = "idea-icons/general/balloonInformation.png"
wenzelm@52472
   147
option gutter_warning_icon : string = "idea-icons/runConfigurations/testFailed.png"
wenzelm@52472
   148
option gutter_legacy_icon : string = "idea-icons/general/balloonWarning.png"
wenzelm@52472
   149
option gutter_error_icon : string = "idea-icons/runConfigurations/testError.png"
wenzelm@52874
   150
option process_passive_icon : string = "idea-icons/process/step_passive.png"
wenzelm@52874
   151
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"