From 57823895aefe3c0fc01a596ec2834f95dac1d5cc Mon Sep 17 00:00:00 2001 From: Ben Fry Date: Sun, 31 Jul 2022 17:07:32 -0400 Subject: [PATCH] tweaking the gutter line numbers a little --- app/src/processing/app/ui/Editor.java | 2 +- todo.txt | 1 + 2 files changed, 2 insertions(+), 1 deletion(-) diff --git a/app/src/processing/app/ui/Editor.java b/app/src/processing/app/ui/Editor.java index e81b162de..3b96faa15 100644 --- a/app/src/processing/app/ui/Editor.java +++ b/app/src/processing/app/ui/Editor.java @@ -87,7 +87,7 @@ public abstract class Editor extends JFrame implements RunnerListener { static public final int LEFT_GUTTER = Toolkit.zoom(45); static public final int RIGHT_GUTTER = Toolkit.zoom(12); - static public final int GUTTER_MARGIN = Toolkit.zoom(3); + static public final int GUTTER_MARGIN = Toolkit.zoom(5); protected MarkerColumn errorColumn; diff --git a/todo.txt b/todo.txt index af5b25faa..970dcb0f2 100755 --- a/todo.txt +++ b/todo.txt @@ -120,6 +120,7 @@ X contrib mgr: filter/dropdown vertical centering is too high X should be resolved with both fonts now being installed X two tier dialog box (defaulting back to Lucida) X dialog box with stack trace (font is too small) +X try to tweak the line numbers in the gutter a bit design/selector X updated 4x4 for themes, foundation svg icon tweaks