Small tweaks.

master
skylarmt 9 years ago
parent 79e228af5b
commit 12f85b505d

@ -478,8 +478,9 @@ public class CodeEditor extends javax.swing.JInternalFrame {
openString(FileUtils.readFile(f.getAbsolutePath()), openString(FileUtils.readFile(f.getAbsolutePath()),
f.getAbsolutePath(), true); f.getAbsolutePath(), true);
} catch (IOException ex) { } catch (IOException ex) {
JOptionPane.showInternalMessageDialog(this, JOptionPane.showInternalMessageDialog(MainGUI.mainPane,
"Error: Cannot load file: " + ex.getMessage()); "Error: Cannot load file: " + ex.getMessage());
MainGUI.loadRecentFiles();
} }
} }

@ -86,9 +86,9 @@ public class Interpreter extends javax.swing.JInternalFrame {
} }
// Set font // Set font
int font_size = 15; int font_size = 12;
try { try {
font_size = Integer.valueOf(PrefStorage.getSetting("editfont")); font_size = Integer.valueOf(PrefStorage.getSetting("shellfontsize", "12"));
} catch (Exception ex) { } catch (Exception ex) {
} }
mainBox.setFont(new Font(Font.MONOSPACED, Font.PLAIN, font_size)); mainBox.setFont(new Font(Font.MONOSPACED, Font.PLAIN, font_size));
@ -391,6 +391,7 @@ public class Interpreter extends javax.swing.JInternalFrame {
if (fo.isModified()) { if (fo.isModified()) {
mainBox.setFont(new Font(Font.MONOSPACED, Font.PLAIN, fo.getResult())); mainBox.setFont(new Font(Font.MONOSPACED, Font.PLAIN, fo.getResult()));
inputBox.setFont(new Font(Font.MONOSPACED, Font.PLAIN, fo.getResult())); inputBox.setFont(new Font(Font.MONOSPACED, Font.PLAIN, fo.getResult()));
PrefStorage.saveSetting("shellfontsize", String.valueOf(fo.getResult()));
} }
}//GEN-LAST:event_fontBtnActionPerformed }//GEN-LAST:event_fontBtnActionPerformed

Loading…
Cancel
Save