# HG changeset patch
# User wenzelm
# Date 1348255473 -7200
# Node ID 506f2a634473fc5b9d5059471ed3076cb19fd92c
# Parent  4d2c93e1d9c80be565bf41818e9f6ec33871f830
tighten margin for TextArea instead of Lobo;

diff -r 4d2c93e1d9c8 -r 506f2a634473 src/Tools/jEdit/src/pretty_text_area.scala
--- a/src/Tools/jEdit/src/pretty_text_area.scala	Fri Sep 21 20:54:48 2012 +0200
+++ b/src/Tools/jEdit/src/pretty_text_area.scala	Fri Sep 21 21:24:33 2012 +0200
@@ -79,7 +79,7 @@
     getPainter.setStyles(SyntaxUtilities.loadStyles(current_font_family, current_font_size))
 
     val font_metrics = getPainter.getFontMetrics(font)
-    val margin = (getWidth / (font_metrics.charWidth(Pretty.spc) max 1) - 4) max 20
+    val margin = (getWidth / (font_metrics.charWidth(Pretty.spc) max 1) - 2) max 20
 
     val base_snapshot = current_base_snapshot
     val formatted_body = Pretty.formatted(current_body, margin, Pretty.font_metric(font_metrics))