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.
clarified pretty margin: attempt to avoid scrollbar;
authorwenzelm
Sun, 10 Jan 2021 15:14:27 +0100
changeset 73122 cd0cd534f927
parent 73121 6345ad861a36
child 73123 b4066bad7f76
clarified pretty margin: attempt to avoid scrollbar;
src/Tools/jEdit/src/pretty_text_area.scala file | annotate | diff | comparison | revisions 
--- 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
isabelle