upper bound for font size;
authorwenzelm
Tue, 08 Jan 2013 18:24:52 +0100
changeset 50775 8c1cda8ad833
parent 50774 ac53370dfae1
child 50776 5a9964f7a691
upper bound for font size;
src/Tools/jEdit/src/isabelle.scala
--- 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()