diff --git a/app/src/processing/app/EditorHeader.java b/app/src/processing/app/EditorHeader.java index db3469f4b..afe31b836 100644 --- a/app/src/processing/app/EditorHeader.java +++ b/app/src/processing/app/EditorHeader.java @@ -398,10 +398,12 @@ public class EditorHeader extends JComponent { int textLeft = tab.left + ((tab.right - tab.left) - tab.textWidth) / 2; g.setColor(textColor[state]); // int baseline = (int) Math.ceil((sizeH + fontAscent) / 2.0); - int baseline = bottom - (TAB_HEIGHT - fontAscent)/2; + //int baseline = bottom - (TAB_HEIGHT - fontAscent)/2; + int tabHeight = TAB_HEIGHT; //bottom - top; + int baseline = top + (tabHeight + fontAscent) / 2; //g.drawString(sketch.code[i].name, textLeft, baseline); g.drawString(tab.text, textLeft, baseline); -// g.drawLine(tab.left, baseline-fontAscent, tab.right, baseline-fontAscent); + g.drawLine(tab.left, baseline-fontAscent, tab.right, baseline-fontAscent); } } diff --git a/app/src/processing/app/Preferences.java b/app/src/processing/app/Preferences.java index 4e9f95c48..086c16c7a 100644 --- a/app/src/processing/app/Preferences.java +++ b/app/src/processing/app/Preferences.java @@ -969,13 +969,9 @@ public class Preferences { } else { if (pieces[0].equals("processing.sans")) { - if (style == Font.BOLD) { - return Toolkit.getBoldFont(size); - } else { - return Toolkit.getPlainFont(size); - } + return Toolkit.getSansFont(size, style); } else if (pieces[0].equals("processing.mono")) { - return Toolkit.getMonoFont(size); + return Toolkit.getMonoFont(size, style); } } diff --git a/app/src/processing/app/Settings.java b/app/src/processing/app/Settings.java index 1a99e72e2..eea88204b 100644 --- a/app/src/processing/app/Settings.java +++ b/app/src/processing/app/Settings.java @@ -215,13 +215,9 @@ public class Settings { } else { if (pieces[0].equals("processing.sans")) { - if (style == Font.BOLD) { - return Toolkit.getBoldFont(size); - } else { - return Toolkit.getPlainFont(size); - } + return Toolkit.getSansFont(size, style); } else if (pieces[0].equals("processing.mono")) { - return Toolkit.getMonoFont(size); + return Toolkit.getMonoFont(size, style); } } diff --git a/app/src/processing/app/Toolkit.java b/app/src/processing/app/Toolkit.java index de35a4c38..79774446b 100644 --- a/app/src/processing/app/Toolkit.java +++ b/app/src/processing/app/Toolkit.java @@ -238,47 +238,116 @@ public class Toolkit { // . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . +// static Font monoFont; +// static Font plainFont; +// static Font boldFont; +// +// +// static public Font getMonoFont(int size) { +// if (monoFont == null) { +// try { +// monoFont = createFont("DroidSansMono.ttf", size); +// } catch (Exception e) { +// monoFont = new Font("Monospaced", Font.PLAIN, size); +// } +// } +// return monoFont; +// } +// +// +// static public Font getPlainFont(int size) { +// if (plainFont == null) { +// try { +// plainFont = createFont("DroidSans.ttf", size); +// } catch (Exception e) { +// plainFont = new Font("SansSerif", Font.PLAIN, size); +// } +// } +// return plainFont; +// } +// +// +// static public Font getBoldFont(int size) { +// if (boldFont == null) { +// try { +// boldFont = createFont("DroidSans-Bold.ttf", size); +// } catch (Exception e) { +// boldFont = new Font("SansSerif", Font.BOLD, size); +// } +// } +// return boldFont; +// } + + static Font monoFont; - static Font plainFont; - static Font boldFont; + static Font monoBoldFont; + static Font sansFont; + static Font sansBoldFont; - static public Font getMonoFont(int size) { + static public Font getMonoFont(int size, int style) { if (monoFont == null) { try { - monoFont = createFont("DroidSansMono.ttf", size); + monoFont = createFont("SourceCodePro-Regular.otf", size); + monoBoldFont = createFont("SourceCodePro-Semibold.otf", size); } catch (Exception e) { monoFont = new Font("Monospaced", Font.PLAIN, size); + monoBoldFont = new Font("Monospaced", Font.BOLD, size); } } - return monoFont; + if (style == Font.BOLD) { + if (size == monoBoldFont.getSize()) { + return monoBoldFont; + } else { +// System.out.println("deriving new font"); + return monoBoldFont.deriveFont((float) size); + } + } else { + if (size == monoFont.getSize()) { + return monoFont; + } else { +// System.out.println("deriving new font"); + return monoFont.deriveFont((float) size); + } + } +// return style == Font.BOLD ? +// monoBoldFont.deriveFont((float) size) : +// monoFont.deriveFont((float) size); } - static public Font getPlainFont(int size) { - if (plainFont == null) { + static public Font getSansFont(int size, int style) { + if (sansFont == null) { try { - plainFont = createFont("DroidSans.ttf", size); + sansFont = createFont("SourceSansPro-Regular.otf", size); + sansBoldFont = createFont("SourceSansPro-Semibold.otf", size); } catch (Exception e) { - plainFont = new Font("SansSerif", Font.PLAIN, size); + sansFont = new Font("Monospaced", Font.PLAIN, size); + sansBoldFont = new Font("Monospaced", Font.BOLD, size); + } + } +// System.out.println("deriving new font"); +// return style == Font.BOLD ? +// sansBoldFont.deriveFont((float) size) : +// sansFont.deriveFont((float) size); + if (style == Font.BOLD) { + if (size == sansBoldFont.getSize()) { + return sansBoldFont; + } else { +// System.out.println("deriving new font"); + return sansBoldFont.deriveFont((float) size); + } + } else { + if (size == sansFont.getSize()) { + return sansFont; + } else { +// System.out.println("deriving new font"); + return sansFont.deriveFont((float) size); } } - return plainFont; } - static public Font getBoldFont(int size) { - if (boldFont == null) { - try { - boldFont = createFont("DroidSans-Bold.ttf", size); - } catch (Exception e) { - boldFont = new Font("SansSerif", Font.BOLD, size); - } - } - return boldFont; - } - - static private Font createFont(String filename, int size) throws IOException, FontFormatException { InputStream is = Base.getLibStream("fonts/" + filename); BufferedInputStream input = new BufferedInputStream(is); diff --git a/app/src/processing/app/syntax/SyntaxStyle.java b/app/src/processing/app/syntax/SyntaxStyle.java index 91e8873de..f29301c55 100644 --- a/app/src/processing/app/syntax/SyntaxStyle.java +++ b/app/src/processing/app/syntax/SyntaxStyle.java @@ -78,32 +78,60 @@ public class SyntaxStyle if(font.equals(lastFont)) return lastStyledFont; lastFont = font; - lastStyledFont = new Font(font.getFamily(), - (bold ? Font.BOLD : 0) - | (italic ? Font.ITALIC : 0), - font.getSize()); +// lastStyledFont = new Font(font.getFamily(), +// (bold ? Font.BOLD : 0) +// | (italic ? Font.ITALIC : 0), +// font.getSize()); + lastStyledFont = + findFont(font.getFamily(), bold ? Font.BOLD : Font.PLAIN, font.getSize()); return lastStyledFont; } /** * Returns the font metrics for the styled font. */ - public FontMetrics getFontMetrics(Font font, JComponent comp) - { - if(font == null) - throw new NullPointerException("font param must not" - + " be null"); - if(font.equals(lastFont) && fontMetrics != null) + public FontMetrics getFontMetrics(Font font, JComponent comp) { + if (font == null) { + throw new NullPointerException("font param must not be null"); + } + if (font.equals(lastFont) && fontMetrics != null) { return fontMetrics; + } lastFont = font; - lastStyledFont = new Font(font.getFamily(), - (bold ? Font.BOLD : 0) - | (italic ? Font.ITALIC : 0), - font.getSize()); +// lastStyledFont = new Font(font.getFamily(), +// (bold ? Font.BOLD : 0) +// | (italic ? Font.ITALIC : 0), +// font.getSize()); + lastStyledFont = + findFont(font.getFamily(), bold ? Font.BOLD : Font.PLAIN, font.getSize()); + //fontMetrics = Toolkit.getDefaultToolkit().getFontMetrics(lastStyledFont); fontMetrics = comp.getFontMetrics(lastStyledFont); return fontMetrics; } + + private String monoFontFamily; + + private Font findFont(String familyName, int style, int size) { + if (monoFontFamily == null) { + // Just get the font family name for comparison + monoFontFamily = + processing.app.Toolkit.getMonoFont(size, style).getFamily(); + //processing.app.Toolkit.getMonoFont(size, style).getFamily(); +// Font mono = processing.app.Toolkit.getMonoFont(size, style); +// System.out.println("mono family " + mono.getFamily()); +// System.out.println("mono fontname " + mono.getFontName()); +// System.out.println("mono name " + mono.getName()); +// System.out.println("mono psname " + mono.getPSName()); + } + if (familyName.equals(monoFontFamily)) { +// System.out.println("getting style bold? " + (style == Font.BOLD)); + return processing.app.Toolkit.getMonoFont(size, style); + } else { +// System.out.println("name is " + name + " mono name is " + monoFontName + " " + style); + return new Font(familyName, style, size); + } + } /** * Sets the foreground color and font of the specified graphics diff --git a/app/src/processing/app/syntax/TextAreaPainter.java b/app/src/processing/app/syntax/TextAreaPainter.java index 775ac5c5c..4f23686ce 100644 --- a/app/src/processing/app/syntax/TextAreaPainter.java +++ b/app/src/processing/app/syntax/TextAreaPainter.java @@ -26,8 +26,7 @@ import java.awt.print.*; * @author Slava Pestov */ public class TextAreaPainter extends JComponent -implements TabExpander, Printable -{ +implements TabExpander, Printable { /** True if inside printing, will handle disabling the highlight */ boolean printing; /** Current setting for editor.antialias preference */ diff --git a/build/shared/lib/theme.txt b/build/shared/lib/theme.txt index 81407f1bc..130327728 100755 --- a/build/shared/lib/theme.txt +++ b/build/shared/lib/theme.txt @@ -18,7 +18,7 @@ header.text.selected.color = #000000 header.text.unselected.color = #ffffff #header.text.font = SansSerif,plain,12 #header.text.font.macosx = Helvetica,plain,12 -header.text.font = processing.sans,plain,12 +header.text.font = processing.sans,plain,16 header.tab.selected.color = #a2afba header.tab.unselected.color = #2a4159