yet another attempt for the editor sizing

This commit is contained in:
Ben Fry
2017-02-11 16:22:09 -05:00
parent 69f0700cc3
commit 4f7cd8cd5a
2 changed files with 11 additions and 8 deletions

View File

@@ -263,8 +263,13 @@ public abstract class Editor extends JFrame implements RunnerListener {
textarea.setRightClickPopup(new TextAreaPopup());
textarea.setHorizontalOffset(JEditTextArea.leftHandGutter);
//System.out.println(textarea.getPreferredSize());
final int editorHeight =
Preferences.getInteger("editor.window.height.default") - 240;
final int editorWidth =
Preferences.getInteger("editor.window.width.default") - 70;
// textarea.setPreferredSize(new Dimension(textarea.getPreferredSize().width,
// Toolkit.zoom(360)));
// Toolkit.zoom(textareaHeight)));
textarea.setPreferredSize(Toolkit.zoom(editorWidth, editorHeight));
{ // Hack: add Numpad Slash as an alternative shortcut for Comment/Uncomment
int modifiers = Toolkit.awtToolkit.getMenuShortcutKeyMask();

View File

@@ -844,6 +844,11 @@ public class Toolkit {
}
static public Dimension zoom(int w, int h) {
return new Dimension(zoom(w), zoom(h));
}
static private float parseZoom() {
String zoomSel = Preferences.get("editor.zoom");
if (zoomOptions.hasValue(zoomSel)) {
@@ -870,13 +875,6 @@ public class Toolkit {
}
/*
static Dimension zoom(int w, int h) {
return new Dimension(zoom(w), zoom(h));
}
*/
// . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .