author | wenzelm |
Wed, 12 Dec 2012 23:36:07 +0100 | |
changeset 50499 | f496b2b7bafb |
parent 50498 | 6647ba2775c1 |
child 50554 | 0493efcc97e9 |
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 |
|
49701 | 9 |
option jedit_tooltip_font_scale : real = 0.85 |
10 |
-- "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
|
11 |
|
cb70157293c0
manage Isabelle/jEdit options as Isabelle/Scala options (with persistent preferences);
wenzelm
parents:
diff
changeset
|
12 |
option jedit_tooltip_margin : int = 60 |
49250 | 13 |
-- "margin for tooltip pretty-printing" |
49245
cb70157293c0
manage Isabelle/jEdit options as Isabelle/Scala options (with persistent preferences);
wenzelm
parents:
diff
changeset
|
14 |
|
49969
72216713733a
further attempts to cope with large files via option jedit_text_overview_limit;
wenzelm
parents:
49722
diff
changeset
|
15 |
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
|
16 |
-- "maximum amount of text to visualize in overview column" |
49697 | 17 |
|
50190 | 18 |
option jedit_symbols_search_limit : int = 50 |
19 |
-- "maximum number of symbols in search result" |
|
20 |
||
49294 | 21 |
|
49296 | 22 |
section "Rendering of Document Content" |
49294 | 23 |
|
49355 | 24 |
option outdated_color : string = "EEE3E3FF" |
25 |
option unprocessed_color : string = "FFA0A0FF" |
|
26 |
option unprocessed1_color : string = "FFA0A032" |
|
27 |
option running_color : string = "610061FF" |
|
28 |
option running1_color : string = "61006164" |
|
29 |
option light_color : string = "F0F0F0FF" |
|
49706 | 30 |
option tooltip_color : string = "FFFFE9FF" |
49355 | 31 |
option writeln_color : string = "C0C0C0FF" |
32 |
option warning_color : string = "FF8C00FF" |
|
33 |
option error_color : string = "B22222FF" |
|
34 |
option error1_color : string = "B2222232" |
|
49474 | 35 |
option writeln_message_color : string = "F0F0F0FF" |
49418 | 36 |
option tracing_message_color : string = "F0F8FFFF" |
37 |
option warning_message_color : string = "EEE8AAFF" |
|
38 |
option error_message_color : string = "FFC1C1FF" |
|
49355 | 39 |
option bad_color : string = "FF6A6A64" |
49358 | 40 |
option intensify_color : string = "FFCC6664" |
49355 | 41 |
option quoted_color : string = "8B8B8B19" |
49358 | 42 |
option highlight_color : string = "50505032" |
49355 | 43 |
option hyperlink_color : string = "000000FF" |
50450
358b6020f8b6
generalized notion of active area, where sendback is just one application;
wenzelm
parents:
50408
diff
changeset
|
44 |
option active_color : string = "DCDCDCFF" |
358b6020f8b6
generalized notion of active area, where sendback is just one application;
wenzelm
parents:
50408
diff
changeset
|
45 |
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
|
46 |
option active_result_color : string = "999966FF" |
49355 | 47 |
option keyword1_color : string = "006699FF" |
48 |
option keyword2_color : string = "009966FF" |
|
49294 | 49 |
|
49355 | 50 |
option tfree_color : string = "A020F0FF" |
51 |
option tvar_color : string = "A020F0FF" |
|
52 |
option free_color : string = "0000FFFF" |
|
53 |
option skolem_color : string = "D2691EFF" |
|
54 |
option bound_color : string = "008000FF" |
|
55 |
option var_color : string = "00009BFF" |
|
56 |
option inner_numeral_color : string = "FF0000FF" |
|
57 |
option inner_quoted_color : string = "D2691EFF" |
|
58 |
option inner_comment_color : string = "8B0000FF" |
|
59 |
option antiquotation_color : string = "0000FFFF" |
|
60 |
option dynamic_color : string = "7BA428FF" |
|
49294 | 61 |