src/Tools/jEdit/etc/options
author wenzelm
Tue Feb 25 20:15:47 2014 +0100 (2014-02-25)
changeset 55747 bef19c929ba5
parent 55726 945ad7eaf37f
child 55790 4670f18baba5
permissions -rw-r--r--
more completion rendering: active, semantic, syntactic;
tuned;
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@53161
    12
public option jedit_reset_font_size : int = 18
wenzelm@53161
    13
  -- "reset font size for main text area"
wenzelm@53161
    14
wenzelm@52065
    15
public option jedit_font_scale : real = 1.0
wenzelm@49272
    16
  -- "scale factor of add-on panels wrt. main text area"
wenzelm@49245
    17
wenzelm@53229
    18
public option jedit_popup_font_scale : real = 0.85
wenzelm@53229
    19
  -- "scale factor of popups wrt. main text area"
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@53639
    30
public option jedit_text_overview_limit : int = 65536
wenzelm@49969
    31
  -- "maximum amount of text to visualize in overview column"
wenzelm@49697
    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@51533
    37
  -- "default threshold for timing display"
wenzelm@51533
    38
wenzelm@53294
    39
wenzelm@53294
    40
section "Completion"
wenzelm@53294
    41
wenzelm@53273
    42
public option jedit_completion : bool = true
wenzelm@53273
    43
  -- "enable completion popup"
wenzelm@53273
    44
wenzelm@53273
    45
public option jedit_completion_delay : real = 0.0
wenzelm@53273
    46
  -- "delay for completion popup (seconds)"
wenzelm@53273
    47
wenzelm@54377
    48
public option jedit_completion_dismiss_delay : real = 0.0
wenzelm@54377
    49
  -- "delay for dismissing obsolete completion popup (seconds)"
wenzelm@54377
    50
wenzelm@53292
    51
public option jedit_completion_immediate : bool = false
wenzelm@53292
    52
  -- "insert unique completion immediately into buffer (if delay = 0)"
wenzelm@53292
    53
wenzelm@49294
    54
wenzelm@49296
    55
section "Rendering of Document Content"
wenzelm@49294
    56
wenzelm@49355
    57
option outdated_color : string = "EEE3E3FF"
wenzelm@49355
    58
option unprocessed_color : string = "FFA0A0FF"
wenzelm@49355
    59
option unprocessed1_color : string = "FFA0A032"
wenzelm@49355
    60
option running_color : string = "610061FF"
wenzelm@49355
    61
option running1_color : string = "61006164"
wenzelm@52576
    62
option light_color : string = "F0F0F064"
wenzelm@51574
    63
option bullet_color : string = "000000FF"
wenzelm@49706
    64
option tooltip_color : string = "FFFFE9FF"
wenzelm@49355
    65
option writeln_color : string = "C0C0C0FF"
wenzelm@52650
    66
option information_color : string = "C1DFEEFF"
wenzelm@49355
    67
option warning_color : string = "FF8C00FF"
wenzelm@49355
    68
option error_color : string = "B22222FF"
wenzelm@49355
    69
option error1_color : string = "B2222232"
wenzelm@49474
    70
option writeln_message_color : string = "F0F0F0FF"
wenzelm@52650
    71
option information_message_color : string = "C1DFEE32"
wenzelm@49418
    72
option tracing_message_color : string = "F0F8FFFF"
wenzelm@49418
    73
option warning_message_color : string = "EEE8AAFF"
wenzelm@49418
    74
option error_message_color : string = "FFC1C1FF"
wenzelm@49355
    75
option bad_color : string = "FF6A6A64"
wenzelm@49358
    76
option intensify_color : string = "FFCC6664"
wenzelm@49355
    77
option quoted_color : string = "8B8B8B19"
wenzelm@52101
    78
option antiquoted_color : string = "FFC83219"
wenzelm@55526
    79
option antiquote_color : string = "6600CCFF"
wenzelm@49358
    80
option highlight_color : string = "50505032"
wenzelm@49355
    81
option hyperlink_color : string = "000000FF"
wenzelm@50450
    82
option active_color : string = "DCDCDCFF"
wenzelm@50450
    83
option active_hover_color : string = "9DC75DFF"
wenzelm@50499
    84
option active_result_color : string = "999966FF"
wenzelm@49355
    85
option keyword1_color : string = "006699FF"
wenzelm@49355
    86
option keyword2_color : string = "009966FF"
wenzelm@55505
    87
option keyword3_color : string = "0099FFFF"
wenzelm@55726
    88
option caret_invisible_color : string = "50000080"
wenzelm@55747
    89
option completion_color : string = "0000FFFF"
wenzelm@49294
    90
wenzelm@49355
    91
option tfree_color : string = "A020F0FF"
wenzelm@49355
    92
option tvar_color : string = "A020F0FF"
wenzelm@49355
    93
option free_color : string = "0000FFFF"
wenzelm@49355
    94
option skolem_color : string = "D2691EFF"
wenzelm@49355
    95
option bound_color : string = "008000FF"
wenzelm@49355
    96
option var_color : string = "00009BFF"
wenzelm@49355
    97
option inner_numeral_color : string = "FF0000FF"
wenzelm@49355
    98
option inner_quoted_color : string = "D2691EFF"
wenzelm@55033
    99
option inner_cartouche_color : string = "CC6600FF"
wenzelm@49355
   100
option inner_comment_color : string = "8B0000FF"
wenzelm@49355
   101
option dynamic_color : string = "7BA428FF"
wenzelm@49294
   102
wenzelm@52472
   103
wenzelm@52472
   104
section "Icons"
wenzelm@52472
   105
wenzelm@52472
   106
option tooltip_close_icon : string = "idea-icons/actions/closeHovered.png"
wenzelm@52472
   107
option tooltip_detach_icon : string = "idea-icons/actions/nextfile.png"
wenzelm@52644
   108
option gutter_information_icon : string = "idea-icons/general/balloonInformation.png"
wenzelm@52472
   109
option gutter_warning_icon : string = "idea-icons/runConfigurations/testFailed.png"
wenzelm@52472
   110
option gutter_legacy_icon : string = "idea-icons/general/balloonWarning.png"
wenzelm@52472
   111
option gutter_error_icon : string = "idea-icons/runConfigurations/testError.png"
wenzelm@52874
   112
option process_passive_icon : string = "idea-icons/process/step_passive.png"
wenzelm@52874
   113
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"
wenzelm@52472
   114