# HG changeset patch
# User wenzelm
# Date 1357665892 -3600
# Node ID 8c1cda8ad83306a2bca6533052a8af07b4122bdb
# Parent  ac53370dfae1cbb080e3c5e479905518680dbf23
upper bound for font size;

diff -r ac53370dfae1 -r 8c1cda8ad833 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()