equal
deleted
inserted
replaced
87 getGutter.setFoldPainter(view.getTextArea.getFoldPainter) |
87 getGutter.setFoldPainter(view.getTextArea.getFoldPainter) |
88 getGutter.setGutterEnabled(jEdit.getBooleanProperty("view.gutter.enabled")) |
88 getGutter.setGutterEnabled(jEdit.getBooleanProperty("view.gutter.enabled")) |
89 |
89 |
90 if (getWidth > 0) { |
90 if (getWidth > 0) { |
91 val metric = JEdit_Lib.pretty_metric(getPainter) |
91 val metric = JEdit_Lib.pretty_metric(getPainter) |
92 val margin = (getPainter.getWidth.toDouble / metric.unit) max 20.0 |
92 val margin = ((getPainter.getWidth.toDouble / metric.unit) max 20.0).floor |
93 |
93 |
94 val snapshot = current_base_snapshot |
94 val snapshot = current_base_snapshot |
95 val results = current_base_results |
95 val results = current_base_results |
96 val formatted_body = Pretty.formatted(current_body, margin = margin, metric = metric) |
96 val formatted_body = Pretty.formatted(current_body, margin = margin, metric = metric) |
97 |
97 |