# HG changeset patch
# User wenzelm
# Date 1610288067 -3600
# Node ID cd0cd534f9273bd12e8db71fb92174a1b19d3aaf
# Parent  6345ad861a36d80eeeed6b3a81dbd10cc630e339
clarified pretty margin: attempt to avoid scrollbar;

diff -r 6345ad861a36 -r cd0cd534f927 src/Tools/jEdit/src/pretty_text_area.scala
--- a/src/Tools/jEdit/src/pretty_text_area.scala	Sun Jan 10 13:17:27 2021 +0100
+++ b/src/Tools/jEdit/src/pretty_text_area.scala	Sun Jan 10 15:14:27 2021 +0100
@@ -89,7 +89,7 @@
 
     if (getWidth > 0) {
       val metric = JEdit_Lib.pretty_metric(getPainter)
-      val margin = (getPainter.getWidth.toDouble / metric.unit) max 20.0
+      val margin = ((getPainter.getWidth.toDouble / metric.unit) max 20.0).floor
 
       val snapshot = current_base_snapshot
       val results = current_base_results