From 364e52d288ad5244ede07715bcb5ab1da1955f2f Mon Sep 17 00:00:00 2001 From: Ben Fry Date: Wed, 19 Aug 2015 18:05:26 -0400 Subject: [PATCH] working on ui, update Java version --- app/src/processing/app/ui/EditorFooter.java | 4 ++-- build/build.xml | 4 ++-- java/src/processing/mode/java/pdex/JavaTextArea.java | 1 + 3 files changed, 5 insertions(+), 4 deletions(-) diff --git a/app/src/processing/app/ui/EditorFooter.java b/app/src/processing/app/ui/EditorFooter.java index 81308bb50..c97815a99 100644 --- a/app/src/processing/app/ui/EditorFooter.java +++ b/app/src/processing/app/ui/EditorFooter.java @@ -55,12 +55,12 @@ public class EditorFooter extends Box { // amount of extra space between individual tabs static final int TAB_BETWEEN = 2; // amount of margin on the left/right for the text on the tab - static final int MARGIN = 10; + static final int MARGIN = 14; static final int ICON_WIDTH = 16; static final int ICON_HEIGHT = 16; static final int ICON_TOP = 7; - static final int ICON_MARGIN = 8; + static final int ICON_MARGIN = 7; Color[] textColor = new Color[2]; Color[] tabColor = new Color[2]; diff --git a/build/build.xml b/build/build.xml index 86615e10d..f992dfc38 100644 --- a/build/build.xml +++ b/build/build.xml @@ -64,8 +64,8 @@ --> - - + + diff --git a/java/src/processing/mode/java/pdex/JavaTextArea.java b/java/src/processing/mode/java/pdex/JavaTextArea.java index 0461e34d1..f74df6dda 100644 --- a/java/src/processing/mode/java/pdex/JavaTextArea.java +++ b/java/src/processing/mode/java/pdex/JavaTextArea.java @@ -136,6 +136,7 @@ public class JavaTextArea extends JEditTextArea { gutterLineColor = mode.getColor("gutter.linecolor"); //, gutterLineColor); gutterPadding = mode.getInteger("gutter.padding"); breakpointMarker = mode.getString("breakpoint.marker"); //, breakpointMarker); +// breakpointMarker = "\u2666"; currentLineMarker = mode.getString("currentline.marker"); //, currentLineMarker); // TweakMode code