| author | blanchet | 
| Thu, 26 Sep 2013 02:09:52 +0200 | |
| changeset 53903 | 27fd72593624 | 
| parent 53884 | 48d13465c7c7 | 
| child 53914 | 48072f049838 | 
| 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: 
51574diff
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 | |
| 53715 | 6 | public option jedit_auto_load : bool = false | 
| 7 | -- "load all required files automatically to resolve theory imports" | |
| 8 | ||
| 53161 | 9 | public option jedit_reset_font_size : int = 18 | 
| 10 | -- "reset font size for main text area" | |
| 11 | ||
| 52065 
78f2475aa126
explicit notion of public options, which are shown in the editor options dialog;
 wenzelm parents: 
51574diff
changeset | 12 | public option jedit_font_scale : real = 1.0 | 
| 49272 
97f8cb455691
replaced jedit_relative_font_size by jedit_font_scale;
 wenzelm parents: 
49270diff
changeset | 13 | -- "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 | 14 | |
| 53229 
6ce8328d7912
explicit "hidden" operation with focus management;
 wenzelm parents: 
53161diff
changeset | 15 | public option jedit_popup_font_scale : real = 0.85 | 
| 
6ce8328d7912
explicit "hidden" operation with focus management;
 wenzelm parents: 
53161diff
changeset | 16 | -- "scale factor of popups wrt. main text area" | 
| 
6ce8328d7912
explicit "hidden" operation with focus management;
 wenzelm parents: 
53161diff
changeset | 17 | |
| 53230 | 18 | public option jedit_popup_bounds : real = 0.5 | 
| 19 | -- "relative bounds of popup window wrt. logical screen size" | |
| 20 | ||
| 52065 
78f2475aa126
explicit notion of public options, which are shown in the editor options dialog;
 wenzelm parents: 
51574diff
changeset | 21 | public option jedit_tooltip_delay : real = 0.75 | 
| 53273 | 22 | -- "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: 
51071diff
changeset | 23 | |
| 52065 
78f2475aa126
explicit notion of public options, which are shown in the editor options dialog;
 wenzelm parents: 
51574diff
changeset | 24 | public option jedit_tooltip_margin : int = 60 | 
| 49250 | 25 | -- "margin for tooltip pretty-printing" | 
| 49245 
cb70157293c0
manage Isabelle/jEdit options as Isabelle/Scala options (with persistent preferences);
 wenzelm parents: diff
changeset | 26 | |
| 53639 
09a4954e7c07
tuned magic number, for improved reactivity on old 2-core machine;
 wenzelm parents: 
53487diff
changeset | 27 | 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: 
49722diff
changeset | 28 | -- "maximum amount of text to visualize in overview column" | 
| 49697 | 29 | |
| 52065 
78f2475aa126
explicit notion of public options, which are shown in the editor options dialog;
 wenzelm parents: 
51574diff
changeset | 30 | public option jedit_symbols_search_limit : int = 50 | 
| 50190 | 31 | -- "maximum number of symbols in search result" | 
| 32 | ||
| 53884 
48d13465c7c7
bypass Isabelle OSX_Adapter for now -- MacOSX plugin 1.3 manages that better;
 wenzelm parents: 
53715diff
changeset | 33 | option jedit_macos_application : bool = false | 
| 53487 | 34 | -- "some native Mac OS X application support (potential conflict with MacOSX plugin)" | 
| 35 | ||
| 53884 
48d13465c7c7
bypass Isabelle OSX_Adapter for now -- MacOSX plugin 1.3 manages that better;
 wenzelm parents: 
53715diff
changeset | 36 | option jedit_macos_preferences : bool = false | 
| 53487 | 37 | -- "native Mac OS X preferences menu" | 
| 51071 
b7e7557e80b5
some native Mac OS X support, notably quit_handler (important for dialog on unsaved changes);
 wenzelm parents: 
50554diff
changeset | 38 | |
| 52065 
78f2475aa126
explicit notion of public options, which are shown in the editor options dialog;
 wenzelm parents: 
51574diff
changeset | 39 | public option jedit_timing_threshold : real = 0.1 | 
| 51533 | 40 | -- "default threshold for timing display" | 
| 41 | ||
| 53294 | 42 | |
| 43 | section "Completion" | |
| 44 | ||
| 53273 | 45 | public option jedit_completion : bool = true | 
| 46 | -- "enable completion popup" | |
| 47 | ||
| 48 | public option jedit_completion_delay : real = 0.0 | |
| 49 | -- "delay for completion popup (seconds)" | |
| 50 | ||
| 53292 
f567c1c7b180
option to insert unique completion immediately into buffer;
 wenzelm parents: 
53273diff
changeset | 51 | public option jedit_completion_immediate : bool = false | 
| 
f567c1c7b180
option to insert unique completion immediately into buffer;
 wenzelm parents: 
53273diff
changeset | 52 | -- "insert unique completion immediately into buffer (if delay = 0)" | 
| 
f567c1c7b180
option to insert unique completion immediately into buffer;
 wenzelm parents: 
53273diff
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: 
52472diff
changeset | 62 | option light_color : string = "F0F0F064" | 
| 51574 
2b58d7b139d6
ghost bullet via markup, which is painted as bar under text (normally space);
 wenzelm parents: 
51533diff
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: 
52065diff
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: 
50408diff
changeset | 81 | option active_color : string = "DCDCDCFF" | 
| 
358b6020f8b6
generalized notion of active area, where sendback is just one application;
 wenzelm parents: 
50408diff
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: 
50498diff
changeset | 83 | option active_result_color : string = "999966FF" | 
| 49355 | 84 | option keyword1_color : string = "006699FF" | 
| 85 | option keyword2_color : string = "009966FF" | |
| 49294 | 86 | |
| 49355 | 87 | option tfree_color : string = "A020F0FF" | 
| 88 | option tvar_color : string = "A020F0FF" | |
| 89 | option free_color : string = "0000FFFF" | |
| 90 | option skolem_color : string = "D2691EFF" | |
| 91 | option bound_color : string = "008000FF" | |
| 92 | option var_color : string = "00009BFF" | |
| 93 | option inner_numeral_color : string = "FF0000FF" | |
| 94 | option inner_quoted_color : string = "D2691EFF" | |
| 95 | option inner_comment_color : string = "8B0000FF" | |
| 96 | option dynamic_color : string = "7BA428FF" | |
| 49294 | 97 | |
| 52472 
3a43a8b1ecb0
load icons via options -- prefer IntelliJ IDEA for now;
 wenzelm parents: 
52101diff
changeset | 98 | |
| 
3a43a8b1ecb0
load icons via options -- prefer IntelliJ IDEA for now;
 wenzelm parents: 
52101diff
changeset | 99 | section "Icons" | 
| 
3a43a8b1ecb0
load icons via options -- prefer IntelliJ IDEA for now;
 wenzelm parents: 
52101diff
changeset | 100 | |
| 
3a43a8b1ecb0
load icons via options -- prefer IntelliJ IDEA for now;
 wenzelm parents: 
52101diff
changeset | 101 | option tooltip_close_icon : string = "idea-icons/actions/closeHovered.png" | 
| 
3a43a8b1ecb0
load icons via options -- prefer IntelliJ IDEA for now;
 wenzelm parents: 
52101diff
changeset | 102 | option tooltip_detach_icon : string = "idea-icons/actions/nextfile.png" | 
| 52644 | 103 | option gutter_information_icon : string = "idea-icons/general/balloonInformation.png" | 
| 52472 
3a43a8b1ecb0
load icons via options -- prefer IntelliJ IDEA for now;
 wenzelm parents: 
52101diff
changeset | 104 | option gutter_warning_icon : string = "idea-icons/runConfigurations/testFailed.png" | 
| 
3a43a8b1ecb0
load icons via options -- prefer IntelliJ IDEA for now;
 wenzelm parents: 
52101diff
changeset | 105 | option gutter_legacy_icon : string = "idea-icons/general/balloonWarning.png" | 
| 
3a43a8b1ecb0
load icons via options -- prefer IntelliJ IDEA for now;
 wenzelm parents: 
52101diff
changeset | 106 | option gutter_error_icon : string = "idea-icons/runConfigurations/testError.png" | 
| 52874 | 107 | option process_passive_icon : string = "idea-icons/process/step_passive.png" | 
| 108 | 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: 
52101diff
changeset | 109 |