src/Tools/jEdit/etc/options
author wenzelm
Thu, 06 Dec 2012 21:54:43 +0100
changeset 50408 1fac4ff86381
parent 50190 0d7f0d8fd63b
child 50450 358b6020f8b6
permissions -rw-r--r--
discontinued option jedit_auto_start, which is somewhat pointless as there is no manual session start within Isabelle/jEdit;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
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
e2762f962042 refined rich tooltip options;
wenzelm
parents: 49697
diff changeset
     9
option jedit_tooltip_font_scale : real = 0.85
e2762f962042 refined rich tooltip options;
wenzelm
parents: 49697
diff changeset
    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
332ab3748350 option jedit_load_delay;
wenzelm
parents: 49245
diff changeset
    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
ad2bd4e5a029 option to bypass potentially slow text overview;
wenzelm
parents: 49492
diff changeset
    17
50190
0d7f0d8fd63b added option jedit_symbols_search_limit;
wenzelm
parents: 49969
diff changeset
    18
option jedit_symbols_search_limit : int = 50
0d7f0d8fd63b added option jedit_symbols_search_limit;
wenzelm
parents: 49969
diff changeset
    19
  -- "maximum number of symbols in search result"
0d7f0d8fd63b added option jedit_symbols_search_limit;
wenzelm
parents: 49969
diff changeset
    20
49294
a600c017f814 provide color values via options;
wenzelm
parents: 49288
diff changeset
    21
49296
313369027391 some GUI support for color options;
wenzelm
parents: 49295
diff changeset
    22
section "Rendering of Document Content"
49294
a600c017f814 provide color values via options;
wenzelm
parents: 49288
diff changeset
    23
49355
7d1af0a6e797 tuned options (again);
wenzelm
parents: 49296
diff changeset
    24
option outdated_color : string = "EEE3E3FF"
7d1af0a6e797 tuned options (again);
wenzelm
parents: 49296
diff changeset
    25
option unprocessed_color : string = "FFA0A0FF"
7d1af0a6e797 tuned options (again);
wenzelm
parents: 49296
diff changeset
    26
option unprocessed1_color : string = "FFA0A032"
7d1af0a6e797 tuned options (again);
wenzelm
parents: 49296
diff changeset
    27
option running_color : string = "610061FF"
7d1af0a6e797 tuned options (again);
wenzelm
parents: 49296
diff changeset
    28
option running1_color : string = "61006164"
7d1af0a6e797 tuned options (again);
wenzelm
parents: 49296
diff changeset
    29
option light_color : string = "F0F0F0FF"
49706
92ef8b638c6c tuned color and font size;
wenzelm
parents: 49701
diff changeset
    30
option tooltip_color : string = "FFFFE9FF"
49355
7d1af0a6e797 tuned options (again);
wenzelm
parents: 49296
diff changeset
    31
option writeln_color : string = "C0C0C0FF"
7d1af0a6e797 tuned options (again);
wenzelm
parents: 49296
diff changeset
    32
option warning_color : string = "FF8C00FF"
7d1af0a6e797 tuned options (again);
wenzelm
parents: 49296
diff changeset
    33
option error_color : string = "B22222FF"
7d1af0a6e797 tuned options (again);
wenzelm
parents: 49296
diff changeset
    34
option error1_color : string = "B2222232"
49474
e7ff10e1a155 clarified message background;
wenzelm
parents: 49473
diff changeset
    35
option writeln_message_color : string = "F0F0F0FF"
49418
c451856129cd more explicit message markup and rendering;
wenzelm
parents: 49358
diff changeset
    36
option tracing_message_color : string = "F0F8FFFF"
c451856129cd more explicit message markup and rendering;
wenzelm
parents: 49358
diff changeset
    37
option warning_message_color : string = "EEE8AAFF"
c451856129cd more explicit message markup and rendering;
wenzelm
parents: 49358
diff changeset
    38
option error_message_color : string = "FFC1C1FF"
49355
7d1af0a6e797 tuned options (again);
wenzelm
parents: 49296
diff changeset
    39
option bad_color : string = "FF6A6A64"
49358
0fa351b1bd14 clarified markup names;
wenzelm
parents: 49355
diff changeset
    40
option intensify_color : string = "FFCC6664"
49355
7d1af0a6e797 tuned options (again);
wenzelm
parents: 49296
diff changeset
    41
option quoted_color : string = "8B8B8B19"
49358
0fa351b1bd14 clarified markup names;
wenzelm
parents: 49355
diff changeset
    42
option highlight_color : string = "50505032"
49355
7d1af0a6e797 tuned options (again);
wenzelm
parents: 49296
diff changeset
    43
option hyperlink_color : string = "000000FF"
49492
2e3e7ea5ce8e some support for hovering and sendback area;
wenzelm
parents: 49474
diff changeset
    44
option sendback_color : string = "DCDCDCFF"
2e3e7ea5ce8e some support for hovering and sendback area;
wenzelm
parents: 49474
diff changeset
    45
option sendback_active_color : string = "9DC75DFF"
49355
7d1af0a6e797 tuned options (again);
wenzelm
parents: 49296
diff changeset
    46
option keyword1_color : string = "006699FF"
7d1af0a6e797 tuned options (again);
wenzelm
parents: 49296
diff changeset
    47
option keyword2_color : string = "009966FF"
49294
a600c017f814 provide color values via options;
wenzelm
parents: 49288
diff changeset
    48
49355
7d1af0a6e797 tuned options (again);
wenzelm
parents: 49296
diff changeset
    49
option tfree_color : string = "A020F0FF"
7d1af0a6e797 tuned options (again);
wenzelm
parents: 49296
diff changeset
    50
option tvar_color : string = "A020F0FF"
7d1af0a6e797 tuned options (again);
wenzelm
parents: 49296
diff changeset
    51
option free_color : string = "0000FFFF"
7d1af0a6e797 tuned options (again);
wenzelm
parents: 49296
diff changeset
    52
option skolem_color : string = "D2691EFF"
7d1af0a6e797 tuned options (again);
wenzelm
parents: 49296
diff changeset
    53
option bound_color : string = "008000FF"
7d1af0a6e797 tuned options (again);
wenzelm
parents: 49296
diff changeset
    54
option var_color : string = "00009BFF"
7d1af0a6e797 tuned options (again);
wenzelm
parents: 49296
diff changeset
    55
option inner_numeral_color : string = "FF0000FF"
7d1af0a6e797 tuned options (again);
wenzelm
parents: 49296
diff changeset
    56
option inner_quoted_color : string = "D2691EFF"
7d1af0a6e797 tuned options (again);
wenzelm
parents: 49296
diff changeset
    57
option inner_comment_color : string = "8B0000FF"
7d1af0a6e797 tuned options (again);
wenzelm
parents: 49296
diff changeset
    58
option antiquotation_color : string = "0000FFFF"
7d1af0a6e797 tuned options (again);
wenzelm
parents: 49296
diff changeset
    59
option dynamic_color : string = "7BA428FF"
49294
a600c017f814 provide color values via options;
wenzelm
parents: 49288
diff changeset
    60