mirror of
https://github.com/arduino/Arduino.git
synced 2024-11-29 10:24:12 +01:00
parent
fcd88e6a43
commit
5427f94b9d
@ -1854,11 +1854,18 @@ public class Base {
|
|||||||
* Adjust font size
|
* Adjust font size
|
||||||
*/
|
*/
|
||||||
public void handleFontSizeChange(int change) {
|
public void handleFontSizeChange(int change) {
|
||||||
String pieces[] = PApplet.split(PreferencesData.get("editor.font"), ',');
|
String pieces[] = PreferencesData.get("editor.font").split(",");
|
||||||
int newSize = Integer.parseInt(pieces[2]) + change;
|
try {
|
||||||
pieces[2] = String.valueOf(newSize);
|
int newSize = Integer.parseInt(pieces[2]) + change;
|
||||||
PreferencesData.set("editor.font", PApplet.join(pieces, ','));
|
if (newSize < 4)
|
||||||
this.getEditors().forEach(processing.app.Editor::applyPreferences);
|
newSize = 4;
|
||||||
|
pieces[2] = String.valueOf(newSize);
|
||||||
|
} catch (NumberFormatException e) {
|
||||||
|
// ignore
|
||||||
|
return;
|
||||||
|
}
|
||||||
|
PreferencesData.set("editor.font", StringUtils.join(pieces, ','));
|
||||||
|
getEditors().forEach(Editor::applyPreferences);
|
||||||
}
|
}
|
||||||
|
|
||||||
// XXX: Remove this method and make librariesIndexer non-static
|
// XXX: Remove this method and make librariesIndexer non-static
|
||||||
|
Loading…
Reference in New Issue
Block a user