author | wenzelm |
Tue, 08 Jan 2013 18:24:52 +0100 | |
changeset 50775 | 8c1cda8ad833 |
parent 50774 | ac53370dfae1 |
child 50776 | 5a9964f7a691 |
--- a/src/Tools/jEdit/src/isabelle.scala Tue Jan 08 17:10:06 2013 +0100 +++ b/src/Tools/jEdit/src/isabelle.scala Tue Jan 08 18:24:52 2013 +0100 @@ -55,7 +55,7 @@ def change_font_size(view: View, change: Int => Int) { - val size = change(jEdit.getIntegerProperty("view.fontsize", 16)) max 5 + val size = change(jEdit.getIntegerProperty("view.fontsize", 16)) max 5 min 250 jEdit.setIntegerProperty("view.fontsize", size) jEdit.propertiesChanged() jEdit.saveSettings()