()
| 287 | } |
| 288 | |
| 289 | public void applyPreferences() { |
| 290 | textarea.setCodeFoldingEnabled(PreferencesData.getBoolean("editor.code_folding")); |
| 291 | scrollPane.setFoldIndicatorEnabled(PreferencesData.getBoolean("editor.code_folding")); |
| 292 | scrollPane.setLineNumbersEnabled(PreferencesData.getBoolean("editor.linenumbers")); |
| 293 | |
| 294 | // apply the setting for 'use external editor', but only if it changed |
| 295 | if (external != PreferencesData.getBoolean("editor.external")) { |
| 296 | external = !external; |
| 297 | if (external) { |
| 298 | // disable line highlight and turn off the caret when disabling |
| 299 | textarea.setBackground(Theme.getColor("editor.external.bgcolor")); |
| 300 | textarea.setHighlightCurrentLine(false); |
| 301 | textarea.setEditable(false); |
| 302 | // Detach from the code, since we are no longer the authoritative source |
| 303 | // for file contents. |
| 304 | file.setStorage(null); |
| 305 | // Reload, in case the file contents already changed. |
| 306 | reload(); |
| 307 | } else { |
| 308 | textarea.setBackground(Theme.getColor("editor.bgcolor")); |
| 309 | textarea.setHighlightCurrentLine(Theme.getBoolean("editor.linehighlight")); |
| 310 | textarea.setEditable(true); |
| 311 | file.setStorage(this); |
| 312 | // Reload once just before disabling external mode, to ensure we have |
| 313 | // the latest contents. |
| 314 | reload(); |
| 315 | } |
| 316 | } |
| 317 | // apply changes to the font size for the editor |
| 318 | Font editorFont = scale(PreferencesData.getFont("editor.font")); |
| 319 | |
| 320 | // check whether a theme-defined editor font is available |
| 321 | Font themeFont = Theme.getFont("editor.font"); |
| 322 | if (themeFont != null) |
| 323 | { |
| 324 | // Apply theme font if the editor font has *not* been changed by the user, |
| 325 | // This allows themes to specify an editor font which will only be applied |
| 326 | // if the user hasn't already changed their editor font via preferences.txt |
| 327 | String defaultFontName = StringUtils.defaultIfEmpty(PreferencesData.getDefault("editor.font"), "").split(",")[0]; |
| 328 | if (defaultFontName.equals(editorFont.getName())) { |
| 329 | editorFont = new Font(themeFont.getName(), themeFont.getStyle(), editorFont.getSize()); |
| 330 | } |
| 331 | } |
| 332 | |
| 333 | textarea.setFont(editorFont); |
| 334 | scrollPane.getGutter().setLineNumberFont(editorFont); |
| 335 | } |
| 336 | |
| 337 | public void updateKeywords(PdeKeywords keywords) { |
| 338 | // update GUI for "Find In Reference" |
no test coverage detected