author | wenzelm |
Sat, 15 Feb 2014 18:28:18 +0100 | |
changeset 55505 | 2a1ca7f6607b |
parent 55033 | 8e8243975860 |
child 55526 | 39708e59f4b0 |
permissions | -rw-r--r-- |
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 | 6 |
public option jedit_print_mode : string = "" |
7 |
-- "default print modes for output, separated by commas (change requires restart)" |
|
8 |
||
53715 | 9 |
public option jedit_auto_load : bool = false |
10 |
-- "load all required files automatically to resolve theory imports" |
|
11 |
||
53161 | 12 |
public option jedit_reset_font_size : int = 18 |
13 |
-- "reset font size for main text area" |
|
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 | 21 |
public option jedit_popup_bounds : real = 0.5 |
22 |
-- "relative bounds of popup window wrt. logical screen size" |
|
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 | 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 | 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 | 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 | 34 |
-- "maximum number of symbols in search result" |
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 | 37 |
-- "default threshold for timing display" |
38 |
||
53294 | 39 |
|
40 |
section "Completion" |
|
41 |
||
53273 | 42 |
public option jedit_completion : bool = true |
43 |
-- "enable completion popup" |
|
44 |
||
45 |
public option jedit_completion_delay : real = 0.0 |
|
46 |
-- "delay for completion popup (seconds)" |
|
47 |
||
54377
750561986828
added jedit_completion_dismiss_delay for hide_popup, which helps to avoid loosing key events on old popup (no change of default behavior);
wenzelm
parents:
53914
diff
changeset
|
48 |
public option jedit_completion_dismiss_delay : real = 0.0 |
750561986828
added jedit_completion_dismiss_delay for hide_popup, which helps to avoid loosing key events on old popup (no change of default behavior);
wenzelm
parents:
53914
diff
changeset
|
49 |
-- "delay for dismissing obsolete completion popup (seconds)" |
750561986828
added jedit_completion_dismiss_delay for hide_popup, which helps to avoid loosing key events on old popup (no change of default behavior);
wenzelm
parents:
53914
diff
changeset
|
50 |
|
53292
f567c1c7b180
option to insert unique completion immediately into buffer;
wenzelm
parents:
53273
diff
changeset
|
51 |
public option jedit_completion_immediate : bool = false |
f567c1c7b180
option to insert unique completion immediately into buffer;
wenzelm
parents:
53273
diff
changeset
|
52 |
-- "insert unique completion immediately into buffer (if delay = 0)" |
f567c1c7b180
option to insert unique completion immediately into buffer;
wenzelm
parents:
53273
diff
changeset
|
53 |
|
49294 | 54 |
|
49296 | 55 |
section "Rendering of Document Content" |
49294 | 56 |
|
49355 | 57 |
option outdated_color : string = "EEE3E3FF" |
58 |
option unprocessed_color : string = "FFA0A0FF" |
|
59 |
option unprocessed1_color : string = "FFA0A032" |
|
60 |
option running_color : string = "610061FF" |
|
61 |
option running1_color : string = "61006164" |
|
52576
7f5be9be51a7
less intrusive token_range rendering, which is relevant for inner parse errors;
wenzelm
parents:
52472
diff
changeset
|
62 |
option light_color : string = "F0F0F064" |
51574
2b58d7b139d6
ghost bullet via markup, which is painted as bar under text (normally space);
wenzelm
parents:
51533
diff
changeset
|
63 |
option bullet_color : string = "000000FF" |
49706 | 64 |
option tooltip_color : string = "FFFFE9FF" |
49355 | 65 |
option writeln_color : string = "C0C0C0FF" |
52650 | 66 |
option information_color : string = "C1DFEEFF" |
49355 | 67 |
option warning_color : string = "FF8C00FF" |
68 |
option error_color : string = "B22222FF" |
|
69 |
option error1_color : string = "B2222232" |
|
49474 | 70 |
option writeln_message_color : string = "F0F0F0FF" |
52650 | 71 |
option information_message_color : string = "C1DFEE32" |
49418 | 72 |
option tracing_message_color : string = "F0F8FFFF" |
73 |
option warning_message_color : string = "EEE8AAFF" |
|
74 |
option error_message_color : string = "FFC1C1FF" |
|
49355 | 75 |
option bad_color : string = "FF6A6A64" |
49358 | 76 |
option intensify_color : string = "FFCC6664" |
49355 | 77 |
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
|
78 |
option antiquoted_color : string = "FFC83219" |
49358 | 79 |
option highlight_color : string = "50505032" |
49355 | 80 |
option hyperlink_color : string = "000000FF" |
50450
358b6020f8b6
generalized notion of active area, where sendback is just one application;
wenzelm
parents:
50408
diff
changeset
|
81 |
option active_color : string = "DCDCDCFF" |
358b6020f8b6
generalized notion of active area, where sendback is just one application;
wenzelm
parents:
50408
diff
changeset
|
82 |
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
|
83 |
option active_result_color : string = "999966FF" |
49355 | 84 |
option keyword1_color : string = "006699FF" |
85 |
option keyword2_color : string = "009966FF" |
|
55505 | 86 |
option keyword3_color : string = "0099FFFF" |
49294 | 87 |
|
49355 | 88 |
option tfree_color : string = "A020F0FF" |
89 |
option tvar_color : string = "A020F0FF" |
|
90 |
option free_color : string = "0000FFFF" |
|
91 |
option skolem_color : string = "D2691EFF" |
|
92 |
option bound_color : string = "008000FF" |
|
93 |
option var_color : string = "00009BFF" |
|
94 |
option inner_numeral_color : string = "FF0000FF" |
|
95 |
option inner_quoted_color : string = "D2691EFF" |
|
55033 | 96 |
option inner_cartouche_color : string = "CC6600FF" |
49355 | 97 |
option inner_comment_color : string = "8B0000FF" |
98 |
option dynamic_color : string = "7BA428FF" |
|
49294 | 99 |
|
52472
3a43a8b1ecb0
load icons via options -- prefer IntelliJ IDEA for now;
wenzelm
parents:
52101
diff
changeset
|
100 |
|
3a43a8b1ecb0
load icons via options -- prefer IntelliJ IDEA for now;
wenzelm
parents:
52101
diff
changeset
|
101 |
section "Icons" |
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 |
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
|
104 |
option tooltip_detach_icon : string = "idea-icons/actions/nextfile.png" |
52644 | 105 |
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
|
106 |
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
|
107 |
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
|
108 |
option gutter_error_icon : string = "idea-icons/runConfigurations/testError.png" |
52874 | 109 |
option process_passive_icon : string = "idea-icons/process/step_passive.png" |
110 |
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
|
111 |