author | wenzelm |
Thu, 06 Dec 2012 21:54:43 +0100 | |
changeset 50408 | 1fac4ff86381 |
parent 50190 | 0d7f0d8fd63b |
child 50450 | 358b6020f8b6 |
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" |
49492 | 44 |
option sendback_color : string = "DCDCDCFF" |
45 |
option sendback_active_color : string = "9DC75DFF" |
|
49355 | 46 |
option keyword1_color : string = "006699FF" |
47 |
option keyword2_color : string = "009966FF" |
|
49294 | 48 |
|
49355 | 49 |
option tfree_color : string = "A020F0FF" |
50 |
option tvar_color : string = "A020F0FF" |
|
51 |
option free_color : string = "0000FFFF" |
|
52 |
option skolem_color : string = "D2691EFF" |
|
53 |
option bound_color : string = "008000FF" |
|
54 |
option var_color : string = "00009BFF" |
|
55 |
option inner_numeral_color : string = "FF0000FF" |
|
56 |
option inner_quoted_color : string = "D2691EFF" |
|
57 |
option inner_comment_color : string = "8B0000FF" |
|
58 |
option antiquotation_color : string = "0000FFFF" |
|
59 |
option dynamic_color : string = "7BA428FF" |
|
49294 | 60 |