src/Tools/jEdit/etc/options
author wenzelm
Sun, 30 Mar 2014 21:03:40 +0200
changeset 56326 c3d7b3bb2708
parent 56202 0a11d17eeeff
child 56550 b26bdc1f96e5
permissions -rw-r--r--
immediate completion even with delay, which is the default according to 638b29331549;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
49245
cb70157293c0 manage Isabelle/jEdit options as Isabelle/Scala options (with persistent preferences);
wenzelm
parents:
diff changeset
     1
(* :mode=isabelle-options: *)
cb70157293c0 manage Isabelle/jEdit options as Isabelle/Scala options (with persistent preferences);
wenzelm
parents:
diff changeset
     2
52065
78f2475aa126 explicit notion of public options, which are shown in the editor options dialog;
wenzelm
parents: 51574
diff changeset
     3
public option jedit_logic : string = ""
49245
cb70157293c0 manage Isabelle/jEdit options as Isabelle/Scala options (with persistent preferences);
wenzelm
parents:
diff changeset
     4
  -- "default logic session"
cb70157293c0 manage Isabelle/jEdit options as Isabelle/Scala options (with persistent preferences);
wenzelm
parents:
diff changeset
     5
54881
dff57132cf18 added system option "jedit_print_mode";
wenzelm
parents: 54377
diff changeset
     6
public option jedit_print_mode : string = ""
dff57132cf18 added system option "jedit_print_mode";
wenzelm
parents: 54377
diff changeset
     7
  -- "default print modes for output, separated by commas (change requires restart)"
dff57132cf18 added system option "jedit_print_mode";
wenzelm
parents: 54377
diff changeset
     8
53715
68c664737d04 added option "jedit_auto_load";
wenzelm
parents: 53639
diff changeset
     9
public option jedit_auto_load : bool = false
68c664737d04 added option "jedit_auto_load";
wenzelm
parents: 53639
diff changeset
    10
  -- "load all required files automatically to resolve theory imports"
68c664737d04 added option "jedit_auto_load";
wenzelm
parents: 53639
diff changeset
    11
53161
051cbf663b5f added action isabelle.reset-font-size;
wenzelm
parents: 52874
diff changeset
    12
public option jedit_reset_font_size : int = 18
051cbf663b5f added action isabelle.reset-font-size;
wenzelm
parents: 52874
diff changeset
    13
  -- "reset font size for main text area"
051cbf663b5f added action isabelle.reset-font-size;
wenzelm
parents: 52874
diff changeset
    14
52065
78f2475aa126 explicit notion of public options, which are shown in the editor options dialog;
wenzelm
parents: 51574
diff changeset
    15
public option jedit_font_scale : real = 1.0
49272
97f8cb455691 replaced jedit_relative_font_size by jedit_font_scale;
wenzelm
parents: 49270
diff changeset
    16
  -- "scale factor of add-on panels wrt. main text area"
49245
cb70157293c0 manage Isabelle/jEdit options as Isabelle/Scala options (with persistent preferences);
wenzelm
parents:
diff changeset
    17
53229
6ce8328d7912 explicit "hidden" operation with focus management;
wenzelm
parents: 53161
diff changeset
    18
public option jedit_popup_font_scale : real = 0.85
6ce8328d7912 explicit "hidden" operation with focus management;
wenzelm
parents: 53161
diff changeset
    19
  -- "scale factor of popups wrt. main text area"
6ce8328d7912 explicit "hidden" operation with focus management;
wenzelm
parents: 53161
diff changeset
    20
53230
6589ff56cc3c determine completion geometry like tooltip;
wenzelm
parents: 53229
diff changeset
    21
public option jedit_popup_bounds : real = 0.5
6589ff56cc3c determine completion geometry like tooltip;
wenzelm
parents: 53229
diff changeset
    22
  -- "relative bounds of popup window wrt. logical screen size"
6589ff56cc3c determine completion geometry like tooltip;
wenzelm
parents: 53229
diff changeset
    23
52065
78f2475aa126 explicit notion of public options, which are shown in the editor options dialog;
wenzelm
parents: 51574
diff changeset
    24
public option jedit_tooltip_delay : real = 0.75
53273
473ea1ed7503 some completion options;
wenzelm
parents: 53230
diff changeset
    25
  -- "open/close delay for document tooltips (seconds)"
51441
37f699750430 more elementary tooltips via mouse events (imitating parts of javax.swing.ToolTipManager) -- avoid abuse of getToolTipText to produce window as side-effect;
wenzelm
parents: 51071
diff changeset
    26
52065
78f2475aa126 explicit notion of public options, which are shown in the editor options dialog;
wenzelm
parents: 51574
diff changeset
    27
public option jedit_tooltip_margin : int = 60
49250
332ab3748350 option jedit_load_delay;
wenzelm
parents: 49245
diff changeset
    28
  -- "margin for tooltip pretty-printing"
49245
cb70157293c0 manage Isabelle/jEdit options as Isabelle/Scala options (with persistent preferences);
wenzelm
parents:
diff changeset
    29
53639
09a4954e7c07 tuned magic number, for improved reactivity on old 2-core machine;
wenzelm
parents: 53487
diff changeset
    30
public option jedit_text_overview_limit : int = 65536
49969
72216713733a further attempts to cope with large files via option jedit_text_overview_limit;
wenzelm
parents: 49722
diff changeset
    31
  -- "maximum amount of text to visualize in overview column"
49697
ad2bd4e5a029 option to bypass potentially slow text overview;
wenzelm
parents: 49492
diff changeset
    32
52065
78f2475aa126 explicit notion of public options, which are shown in the editor options dialog;
wenzelm
parents: 51574
diff changeset
    33
public option jedit_symbols_search_limit : int = 50
50190
0d7f0d8fd63b added option jedit_symbols_search_limit;
wenzelm
parents: 49969
diff changeset
    34
  -- "maximum number of symbols in search result"
0d7f0d8fd63b added option jedit_symbols_search_limit;
wenzelm
parents: 49969
diff changeset
    35
52065
78f2475aa126 explicit notion of public options, which are shown in the editor options dialog;
wenzelm
parents: 51574
diff changeset
    36
public option jedit_timing_threshold : real = 0.1
51533
3f6280aedbcc dockable window for timing information;
wenzelm
parents: 51452
diff changeset
    37
  -- "default threshold for timing display"
3f6280aedbcc dockable window for timing information;
wenzelm
parents: 51452
diff changeset
    38
53294
wenzelm
parents: 53292
diff changeset
    39
wenzelm
parents: 53292
diff changeset
    40
section "Completion"
wenzelm
parents: 53292
diff changeset
    41
53273
473ea1ed7503 some completion options;
wenzelm
parents: 53230
diff changeset
    42
public option jedit_completion : bool = true
473ea1ed7503 some completion options;
wenzelm
parents: 53230
diff changeset
    43
  -- "enable completion popup"
473ea1ed7503 some completion options;
wenzelm
parents: 53230
diff changeset
    44
56170
638b29331549 allow implicit semantic completion, notably after delay that exceeds usual round-trip time;
wenzelm
parents: 56064
diff changeset
    45
public option jedit_completion_delay : real = 0.5
53273
473ea1ed7503 some completion options;
wenzelm
parents: 53230
diff changeset
    46
  -- "delay for completion popup (seconds)"
473ea1ed7503 some completion options;
wenzelm
parents: 53230
diff changeset
    47
53292
f567c1c7b180 option to insert unique completion immediately into buffer;
wenzelm
parents: 53273
diff changeset
    48
public option jedit_completion_immediate : bool = false
56326
c3d7b3bb2708 immediate completion even with delay, which is the default according to 638b29331549;
wenzelm
parents: 56202
diff changeset
    49
  -- "insert uniquely completed abbreviation immediately into buffer"
53292
f567c1c7b180 option to insert unique completion immediately into buffer;
wenzelm
parents: 53273
diff changeset
    50
49294
a600c017f814 provide color values via options;
wenzelm
parents: 49288
diff changeset
    51
49296
313369027391 some GUI support for color options;
wenzelm
parents: 49295
diff changeset
    52
section "Rendering of Document Content"
49294
a600c017f814 provide color values via options;
wenzelm
parents: 49288
diff changeset
    53
49355
7d1af0a6e797 tuned options (again);
wenzelm
parents: 49296
diff changeset
    54
option outdated_color : string = "EEE3E3FF"
7d1af0a6e797 tuned options (again);
wenzelm
parents: 49296
diff changeset
    55
option unprocessed_color : string = "FFA0A0FF"
7d1af0a6e797 tuned options (again);
wenzelm
parents: 49296
diff changeset
    56
option unprocessed1_color : string = "FFA0A032"
7d1af0a6e797 tuned options (again);
wenzelm
parents: 49296
diff changeset
    57
option running_color : string = "610061FF"
7d1af0a6e797 tuned options (again);
wenzelm
parents: 49296
diff changeset
    58
option running1_color : string = "61006164"
51574
2b58d7b139d6 ghost bullet via markup, which is painted as bar under text (normally space);
wenzelm
parents: 51533
diff changeset
    59
option bullet_color : string = "000000FF"
49706
92ef8b638c6c tuned color and font size;
wenzelm
parents: 49701
diff changeset
    60
option tooltip_color : string = "FFFFE9FF"
49355
7d1af0a6e797 tuned options (again);
wenzelm
parents: 49296
diff changeset
    61
option writeln_color : string = "C0C0C0FF"
52650
4cf6fbf1d9a1 more rendering for information messages;
wenzelm
parents: 52644
diff changeset
    62
option information_color : string = "C1DFEEFF"
49355
7d1af0a6e797 tuned options (again);
wenzelm
parents: 49296
diff changeset
    63
option warning_color : string = "FF8C00FF"
7d1af0a6e797 tuned options (again);
wenzelm
parents: 49296
diff changeset
    64
option error_color : string = "B22222FF"
7d1af0a6e797 tuned options (again);
wenzelm
parents: 49296
diff changeset
    65
option error1_color : string = "B2222232"
49474
e7ff10e1a155 clarified message background;
wenzelm
parents: 49473
diff changeset
    66
option writeln_message_color : string = "F0F0F0FF"
52650
4cf6fbf1d9a1 more rendering for information messages;
wenzelm
parents: 52644
diff changeset
    67
option information_message_color : string = "C1DFEE32"
49418
c451856129cd more explicit message markup and rendering;
wenzelm
parents: 49358
diff changeset
    68
option tracing_message_color : string = "F0F8FFFF"
c451856129cd more explicit message markup and rendering;
wenzelm
parents: 49358
diff changeset
    69
option warning_message_color : string = "EEE8AAFF"
c451856129cd more explicit message markup and rendering;
wenzelm
parents: 49358
diff changeset
    70
option error_message_color : string = "FFC1C1FF"
49355
7d1af0a6e797 tuned options (again);
wenzelm
parents: 49296
diff changeset
    71
option bad_color : string = "FF6A6A64"
49358
0fa351b1bd14 clarified markup names;
wenzelm
parents: 49355
diff changeset
    72
option intensify_color : string = "FFCC6664"
49355
7d1af0a6e797 tuned options (again);
wenzelm
parents: 49296
diff changeset
    73
option quoted_color : string = "8B8B8B19"
52101
7679178b0aa5 less intrusive rendering of antiquoted text -- avoid visual clash with "blue variables" in particular;
wenzelm
parents: 52065
diff changeset
    74
option antiquoted_color : string = "FFC83219"
55526
39708e59f4b0 more markup;
wenzelm
parents: 55505
diff changeset
    75
option antiquote_color : string = "6600CCFF"
49358
0fa351b1bd14 clarified markup names;
wenzelm
parents: 49355
diff changeset
    76
option highlight_color : string = "50505032"
49355
7d1af0a6e797 tuned options (again);
wenzelm
parents: 49296
diff changeset
    77
option hyperlink_color : string = "000000FF"
50450
358b6020f8b6 generalized notion of active area, where sendback is just one application;
wenzelm
parents: 50408
diff changeset
    78
option active_color : string = "DCDCDCFF"
358b6020f8b6 generalized notion of active area, where sendback is just one application;
wenzelm
parents: 50408
diff changeset
    79
option active_hover_color : string = "9DC75DFF"
50499
f496b2b7bafb rendering of selected dialog_result as active_result_color, depending on dynamic command status in output panel, but not static popups etc.;
wenzelm
parents: 50498
diff changeset
    80
option active_result_color : string = "999966FF"
49355
7d1af0a6e797 tuned options (again);
wenzelm
parents: 49296
diff changeset
    81
option keyword1_color : string = "006699FF"
7d1af0a6e797 tuned options (again);
wenzelm
parents: 49296
diff changeset
    82
option keyword2_color : string = "009966FF"
55505
2a1ca7f6607b more uniform ML keyword markup;
wenzelm
parents: 55033
diff changeset
    83
option keyword3_color : string = "0099FFFF"
55924
fd5e3f93bae4 tuned color (cf. jEdit FUNCTION);
wenzelm
parents: 55919
diff changeset
    84
option quasi_keyword_color : string = "9966FFFF"
56202
0a11d17eeeff more markup for improper elements;
wenzelm
parents: 56197
diff changeset
    85
option improper_color : string = "FF5050FF"
56064
7658489047e3 clarified Markup.operator vs. Markup.delimiter;
wenzelm
parents: 55924
diff changeset
    86
option operator_color : string = "323232FF"
55726
945ad7eaf37f tuned colors;
wenzelm
parents: 55713
diff changeset
    87
option caret_invisible_color : string = "50000080"
55747
bef19c929ba5 more completion rendering: active, semantic, syntactic;
wenzelm
parents: 55726
diff changeset
    88
option completion_color : string = "0000FFFF"
49294
a600c017f814 provide color values via options;
wenzelm
parents: 49288
diff changeset
    89
49355
7d1af0a6e797 tuned options (again);
wenzelm
parents: 49296
diff changeset
    90
option tfree_color : string = "A020F0FF"
7d1af0a6e797 tuned options (again);
wenzelm
parents: 49296
diff changeset
    91
option tvar_color : string = "A020F0FF"
7d1af0a6e797 tuned options (again);
wenzelm
parents: 49296
diff changeset
    92
option free_color : string = "0000FFFF"
7d1af0a6e797 tuned options (again);
wenzelm
parents: 49296
diff changeset
    93
option skolem_color : string = "D2691EFF"
7d1af0a6e797 tuned options (again);
wenzelm
parents: 49296
diff changeset
    94
option bound_color : string = "008000FF"
7d1af0a6e797 tuned options (again);
wenzelm
parents: 49296
diff changeset
    95
option var_color : string = "00009BFF"
7d1af0a6e797 tuned options (again);
wenzelm
parents: 49296
diff changeset
    96
option inner_numeral_color : string = "FF0000FF"
7d1af0a6e797 tuned options (again);
wenzelm
parents: 49296
diff changeset
    97
option inner_quoted_color : string = "D2691EFF"
55033
8e8243975860 support for nested text cartouches;
wenzelm
parents: 54881
diff changeset
    98
option inner_cartouche_color : string = "CC6600FF"
49355
7d1af0a6e797 tuned options (again);
wenzelm
parents: 49296
diff changeset
    99
option inner_comment_color : string = "8B0000FF"
7d1af0a6e797 tuned options (again);
wenzelm
parents: 49296
diff changeset
   100
option dynamic_color : string = "7BA428FF"
49294
a600c017f814 provide color values via options;
wenzelm
parents: 49288
diff changeset
   101
52472
3a43a8b1ecb0 load icons via options -- prefer IntelliJ IDEA for now;
wenzelm
parents: 52101
diff changeset
   102
3a43a8b1ecb0 load icons via options -- prefer IntelliJ IDEA for now;
wenzelm
parents: 52101
diff changeset
   103
section "Icons"
3a43a8b1ecb0 load icons via options -- prefer IntelliJ IDEA for now;
wenzelm
parents: 52101
diff changeset
   104
3a43a8b1ecb0 load icons via options -- prefer IntelliJ IDEA for now;
wenzelm
parents: 52101
diff changeset
   105
option tooltip_close_icon : string = "idea-icons/actions/closeHovered.png"
3a43a8b1ecb0 load icons via options -- prefer IntelliJ IDEA for now;
wenzelm
parents: 52101
diff changeset
   106
option tooltip_detach_icon : string = "idea-icons/actions/nextfile.png"
52644
cea207576f81 gutter icon for information messages;
wenzelm
parents: 52643
diff changeset
   107
option gutter_information_icon : string = "idea-icons/general/balloonInformation.png"
52472
3a43a8b1ecb0 load icons via options -- prefer IntelliJ IDEA for now;
wenzelm
parents: 52101
diff changeset
   108
option gutter_warning_icon : string = "idea-icons/runConfigurations/testFailed.png"
3a43a8b1ecb0 load icons via options -- prefer IntelliJ IDEA for now;
wenzelm
parents: 52101
diff changeset
   109
option gutter_legacy_icon : string = "idea-icons/general/balloonWarning.png"
3a43a8b1ecb0 load icons via options -- prefer IntelliJ IDEA for now;
wenzelm
parents: 52101
diff changeset
   110
option gutter_error_icon : string = "idea-icons/runConfigurations/testError.png"
52874
91032244e4ca query process animation;
wenzelm
parents: 52650
diff changeset
   111
option process_passive_icon : string = "idea-icons/process/step_passive.png"
91032244e4ca query process animation;
wenzelm
parents: 52650
diff changeset
   112
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"
52472
3a43a8b1ecb0 load icons via options -- prefer IntelliJ IDEA for now;
wenzelm
parents: 52101
diff changeset
   113