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