From 334e75254f7fc9a1fe051781ce9e9720e3c50c60 Mon Sep 17 00:00:00 2001 From: Federico Fissore Date: Mon, 11 May 2015 17:07:09 +0200 Subject: [PATCH] Restoring left empty space on the editor --- app/src/processing/app/Editor.java | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/app/src/processing/app/Editor.java b/app/src/processing/app/Editor.java index 74805fdd2..d05518b3d 100644 --- a/app/src/processing/app/Editor.java +++ b/app/src/processing/app/Editor.java @@ -47,7 +47,7 @@ import java.util.List; import java.util.zip.*; import javax.swing.*; -import javax.swing.border.EmptyBorder; +import javax.swing.border.MatteBorder; import javax.swing.event.*; import javax.swing.text.*; import javax.swing.undo.*; @@ -256,7 +256,7 @@ public class Editor extends JFrame implements RunnerListener { // RTextScrollPane scrollPane = new RTextScrollPane(textarea, true); - scrollPane.setBorder(new EmptyBorder(0, 0, 0, 0)); + scrollPane.setBorder(new MatteBorder(0, 6, 0, 0, Theme.getColor("editor.bgcolor"))); scrollPane.setViewportBorder(BorderFactory.createEmptyBorder()); scrollPane.setLineNumbersEnabled(Preferences.getBoolean("editor.linenumbers")); scrollPane.setIconRowHeaderEnabled(false); @@ -265,7 +265,7 @@ public class Editor extends JFrame implements RunnerListener { gutter.setBookmarkingEnabled(false); //gutter.setBookmarkIcon(CompletionsRenderer.getIcon(CompletionType.TEMPLATE)); gutter.setIconRowHeaderInheritsGutterBackground(true); - + upper.add(scrollPane); splitPane = new JSplitPane(JSplitPane.VERTICAL_SPLIT, upper, consolePanel);