mirror of
https://github.com/processing/processing4.git
synced 2026-06-16 04:26:26 +02:00
fix console location and divider placement
This commit is contained in:
@@ -262,14 +262,16 @@ public abstract class Editor extends JFrame implements RunnerListener {
|
||||
textarea = createTextArea();
|
||||
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 editorHeight = 200;
|
||||
//Preferences.getInteger("editor.window.height.default") - 340; //240;
|
||||
final int editorWidth =
|
||||
Preferences.getInteger("editor.window.width.default") - 70;
|
||||
// textarea.setPreferredSize(new Dimension(textarea.getPreferredSize().width,
|
||||
// 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();
|
||||
@@ -349,7 +351,7 @@ public abstract class Editor extends JFrame implements RunnerListener {
|
||||
|
||||
contentPain.setTransferHandler(new FileDropHandler());
|
||||
|
||||
// Finish preparing Editor (formerly found in Base)
|
||||
// Finish preparing Editor
|
||||
pack();
|
||||
|
||||
// Set the window bounds and the divider location before setting it visible
|
||||
|
||||
@@ -223,7 +223,8 @@ public class EditorConsole extends JScrollPane {
|
||||
*/
|
||||
protected void updateAppearance() {
|
||||
String fontFamily = Preferences.get("editor.font.family");
|
||||
int fontSize = Preferences.getInteger("console.font.size");
|
||||
int fontSize =
|
||||
Toolkit.zoom(Preferences.getInteger("console.font.size"));
|
||||
StyleConstants.setFontFamily(stdStyle, fontFamily);
|
||||
StyleConstants.setFontSize(stdStyle, fontSize);
|
||||
StyleConstants.setFontFamily(errStyle, fontFamily);
|
||||
|
||||
@@ -221,6 +221,8 @@ public class EditorState {
|
||||
editor.setBounds(editorBounds);
|
||||
if (dividerLocation != 0) {
|
||||
editor.setDividerLocation(dividerLocation);
|
||||
} else {
|
||||
editor.setDividerLocation(2 * editor.getSize().height / 3);
|
||||
}
|
||||
if (isMaximized) {
|
||||
editor.setExtendedState(Frame.MAXIMIZED_BOTH);
|
||||
|
||||
Reference in New Issue
Block a user