rooty/Arduino
1
0
Fork 0
mirror of https://github.com/arduino/Arduino.git synced 2025-02-19 13:54:23 +01:00
Code Issues Releases Activity

New editor: mark occurrences enable when "editor.advanced" (hidden pref) is true. Fixes #3102

Browse Source
This commit is contained in:
Federico Fissore 2015-05-13 17:07:54 +02:00
parent 02e94f1879
commit 2d24d074e3
1 changed files with 1 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
app/src/processing/app/Editor.java
View File

@ -959,7 +959,7 @@ public class Editor extends JFrame implements RunnerListener {
protected SketchTextArea createTextArea() throws IOException {
SketchTextArea textArea = new SketchTextArea(base.getPdeKeywords());
textArea.requestFocusInWindow();
textArea.setMarkOccurrences(true);
textArea.setMarkOccurrences(PreferencesData.getBoolean("editor.advanced"));
textArea.setMarginLineEnabled(false);
textArea.setCodeFoldingEnabled(PreferencesData.getBoolean("editor.code_folding"));
textArea.setAntiAliasingEnabled(PreferencesData.getBoolean("editor.antialias"));