upper bound for font size;
authorwenzelm
Tue Jan 08 18:24:52 2013 +0100 (2013-01-08)
changeset 507758c1cda8ad833
parent 50774 ac53370dfae1
child 50776 5a9964f7a691
upper bound for font size;
src/Tools/jEdit/src/isabelle.scala
     1.1 --- a/src/Tools/jEdit/src/isabelle.scala	Tue Jan 08 17:10:06 2013 +0100
     1.2 +++ b/src/Tools/jEdit/src/isabelle.scala	Tue Jan 08 18:24:52 2013 +0100
     1.3 @@ -55,7 +55,7 @@
     1.4  
     1.5    def change_font_size(view: View, change: Int => Int)
     1.6    {
     1.7 -    val size = change(jEdit.getIntegerProperty("view.fontsize", 16)) max 5
     1.8 +    val size = change(jEdit.getIntegerProperty("view.fontsize", 16)) max 5 min 250
     1.9      jEdit.setIntegerProperty("view.fontsize", size)
    1.10      jEdit.propertiesChanged()
    1.11      jEdit.saveSettings()