Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
tighten margin for TextArea instead of Lobo;
authorwenzelm
Fri, 21 Sep 2012 21:24:33 +0200
changeset 49520 506f2a634473
parent 49519 4d2c93e1d9c8
child 49521 06cb12198b92
tighten margin for TextArea instead of Lobo;
src/Tools/jEdit/src/pretty_text_area.scala file | annotate | diff | comparison | revisions 
--- 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))
isabelle