equal
deleted
inserted
replaced
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 |
71 |
72 public option jedit_completion_path_ignore : string = "*~:*.marks:*.orig:*.rej:.DS_Store" |
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)" |
73 -- "glob patterns to ignore in file-system path completion (separated by colons)" |
74 |
|
75 |
|
76 section "Spell Checker" |
|
77 |
|
78 public option spell_checker : bool = true |
|
79 -- "enable spell-checker for prose words within document text, comments etc." |
|
80 |
|
81 public option spell_checker_dictionary : string = "en" |
|
82 -- "spell-checker dictionary name" |
|
83 |
|
84 public option spell_checker_elements : string = "words,comment,inner_comment,ML_comment,SML_comment" |
|
85 -- "relevant markup elements for spell-checker, separated by commas" |
|
86 |
74 |
87 |
75 |
88 section "Rendering of Document Content" |
76 section "Rendering of Document Content" |
89 |
77 |
90 option outdated_color : string = "EEE3E3FF" |
78 option outdated_color : string = "EEE3E3FF" |