equal
deleted
inserted
replaced
66 public option jedit_completion_delay : real = 0.5 |
66 public option jedit_completion_delay : real = 0.5 |
67 -- "delay for completion popup (seconds)" |
67 -- "delay for completion popup (seconds)" |
68 |
68 |
69 public option jedit_completion_immediate : bool = true |
69 public option jedit_completion_immediate : bool = true |
70 -- "insert uniquely completed abbreviation immediately into buffer" |
70 -- "insert uniquely completed abbreviation immediately into buffer" |
71 |
|
72 public option jedit_completion_path_ignore : string = "*~:*.marks:*.orig:*.rej:.DS_Store" |
|
73 -- "glob patterns to ignore in file-system path completion (separated by colons)" |
|
74 |
71 |
75 |
72 |
76 section "Rendering of Document Content" |
73 section "Rendering of Document Content" |
77 |
74 |
78 option outdated_color : string = "EEE3E3FF" |
75 option outdated_color : string = "EEE3E3FF" |