equal
deleted
inserted
replaced
27 public option jedit_tooltip_delay : real = 0.75 |
27 public option jedit_tooltip_delay : real = 0.75 |
28 -- "open/close delay for document tooltips (seconds)" |
28 -- "open/close delay for document tooltips (seconds)" |
29 |
29 |
30 public option jedit_tooltip_margin : int = 60 |
30 public option jedit_tooltip_margin : int = 60 |
31 -- "margin for tooltip pretty-printing" |
31 -- "margin for tooltip pretty-printing" |
32 |
|
33 public option jedit_text_overview_limit : int = 65536 |
|
34 -- "maximum amount of text to visualize in overview column" |
|
35 |
32 |
36 public option jedit_structure_limit : int = 1000 |
33 public option jedit_structure_limit : int = 1000 |
37 -- "maximum number of lines to scan for language structure" |
34 -- "maximum number of lines to scan for language structure" |
38 |
35 |
39 public option jedit_symbols_search_limit : int = 50 |
36 public option jedit_symbols_search_limit : int = 50 |