src/Tools/jEdit/src/jedit_lib.scala

--- a/src/Tools/jEdit/src/jedit_lib.scala	Sun Aug 03 17:17:59 2014 +0200
+++ b/src/Tools/jEdit/src/jedit_lib.scala	Sun Aug 03 17:33:38 2014 +0200
@@ -295,7 +295,7 @@
       def string_width(s: String): Double =
         painter.getFont.getStringBounds(s, painter.getFontRenderContext).getWidth
 
-      val unit = string_width(Pretty.space)
+      val unit = string_width(Pretty.space) max 1.0
       val average = string_width("mix") / (3 * unit)
       def apply(s: String): Double = if (s == "\n") 1.0 else string_width(s) / unit
     }