author | wenzelm |
Sat, 16 Mar 2013 21:26:44 +0100 | |
changeset 51441 | 37f699750430 |
parent 51071 | b7e7557e80b5 |
child 51452 | 14e6d761ba1c |
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 |
|
cb70157293c0
manage Isabelle/jEdit options as Isabelle/Scala options (with persistent preferences);
wenzelm
parents:
diff
changeset
|
3 |
option jedit_logic : string = "" |
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 |
|
49272
97f8cb455691
replaced jedit_relative_font_size by jedit_font_scale;
wenzelm
parents:
49270
diff
changeset
|
6 |
option jedit_font_scale : real = 1.0 |
97f8cb455691
replaced jedit_relative_font_size by jedit_font_scale;
wenzelm
parents:
49270
diff
changeset
|
7 |
-- "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
|
8 |
|
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
|
9 |
option jedit_tooltip_delay : real = 0.75 |
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
|
10 |
-- "delay for semantic tooltip popup" |
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
|
11 |
|
49701 | 12 |
option jedit_tooltip_font_scale : real = 0.85 |
13 |
-- "scale factor of tooltips wrt. main text area" |
|
49245
cb70157293c0
manage Isabelle/jEdit options as Isabelle/Scala options (with persistent preferences);
wenzelm
parents:
diff
changeset
|
14 |
|
cb70157293c0
manage Isabelle/jEdit options as Isabelle/Scala options (with persistent preferences);
wenzelm
parents:
diff
changeset
|
15 |
option jedit_tooltip_margin : int = 60 |
49250 | 16 |
-- "margin for tooltip pretty-printing" |
49245
cb70157293c0
manage Isabelle/jEdit options as Isabelle/Scala options (with persistent preferences);
wenzelm
parents:
diff
changeset
|
17 |
|
50554
0493efcc97e9
more general handling of graphics configurations, to increase chance of proper positioning of tooltips in multi-screen environment;
wenzelm
parents:
50499
diff
changeset
|
18 |
option jedit_tooltip_bounds : real = 0.5 |
0493efcc97e9
more general handling of graphics configurations, to increase chance of proper positioning of tooltips in multi-screen environment;
wenzelm
parents:
50499
diff
changeset
|
19 |
-- "relative bounds of tooltip window wrt. logical screen size" |
0493efcc97e9
more general handling of graphics configurations, to increase chance of proper positioning of tooltips in multi-screen environment;
wenzelm
parents:
50499
diff
changeset
|
20 |
|
49969
72216713733a
further attempts to cope with large files via option jedit_text_overview_limit;
wenzelm
parents:
49722
diff
changeset
|
21 |
option jedit_text_overview_limit : int = 100000 |
72216713733a
further attempts to cope with large files via option jedit_text_overview_limit;
wenzelm
parents:
49722
diff
changeset
|
22 |
-- "maximum amount of text to visualize in overview column" |
49697 | 23 |
|
50190 | 24 |
option jedit_symbols_search_limit : int = 50 |
25 |
-- "maximum number of symbols in search result" |
|
26 |
||
51071
b7e7557e80b5
some native Mac OS X support, notably quit_handler (important for dialog on unsaved changes);
wenzelm
parents:
50554
diff
changeset
|
27 |
option jedit_mac_adapter : bool = true |
b7e7557e80b5
some native Mac OS X support, notably quit_handler (important for dialog on unsaved changes);
wenzelm
parents:
50554
diff
changeset
|
28 |
-- "some native Mac OS X support (potential conflict with MacOSX plugin)" |
b7e7557e80b5
some native Mac OS X support, notably quit_handler (important for dialog on unsaved changes);
wenzelm
parents:
50554
diff
changeset
|
29 |
|
49294 | 30 |
|
49296 | 31 |
section "Rendering of Document Content" |
49294 | 32 |
|
49355 | 33 |
option outdated_color : string = "EEE3E3FF" |
34 |
option unprocessed_color : string = "FFA0A0FF" |
|
35 |
option unprocessed1_color : string = "FFA0A032" |
|
36 |
option running_color : string = "610061FF" |
|
37 |
option running1_color : string = "61006164" |
|
38 |
option light_color : string = "F0F0F0FF" |
|
49706 | 39 |
option tooltip_color : string = "FFFFE9FF" |
49355 | 40 |
option writeln_color : string = "C0C0C0FF" |
41 |
option warning_color : string = "FF8C00FF" |
|
42 |
option error_color : string = "B22222FF" |
|
43 |
option error1_color : string = "B2222232" |
|
49474 | 44 |
option writeln_message_color : string = "F0F0F0FF" |
49418 | 45 |
option tracing_message_color : string = "F0F8FFFF" |
46 |
option warning_message_color : string = "EEE8AAFF" |
|
47 |
option error_message_color : string = "FFC1C1FF" |
|
49355 | 48 |
option bad_color : string = "FF6A6A64" |
49358 | 49 |
option intensify_color : string = "FFCC6664" |
49355 | 50 |
option quoted_color : string = "8B8B8B19" |
49358 | 51 |
option highlight_color : string = "50505032" |
49355 | 52 |
option hyperlink_color : string = "000000FF" |
50450
358b6020f8b6
generalized notion of active area, where sendback is just one application;
wenzelm
parents:
50408
diff
changeset
|
53 |
option active_color : string = "DCDCDCFF" |
358b6020f8b6
generalized notion of active area, where sendback is just one application;
wenzelm
parents:
50408
diff
changeset
|
54 |
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
|
55 |
option active_result_color : string = "999966FF" |
49355 | 56 |
option keyword1_color : string = "006699FF" |
57 |
option keyword2_color : string = "009966FF" |
|
49294 | 58 |
|
49355 | 59 |
option tfree_color : string = "A020F0FF" |
60 |
option tvar_color : string = "A020F0FF" |
|
61 |
option free_color : string = "0000FFFF" |
|
62 |
option skolem_color : string = "D2691EFF" |
|
63 |
option bound_color : string = "008000FF" |
|
64 |
option var_color : string = "00009BFF" |
|
65 |
option inner_numeral_color : string = "FF0000FF" |
|
66 |
option inner_quoted_color : string = "D2691EFF" |
|
67 |
option inner_comment_color : string = "8B0000FF" |
|
68 |
option antiquotation_color : string = "0000FFFF" |
|
69 |
option dynamic_color : string = "7BA428FF" |
|
49294 | 70 |