|
40 | 40 | import org.eclipse.swt.graphics.ImageData; |
41 | 41 | import org.eclipse.swt.graphics.Point; |
42 | 42 | import org.eclipse.swt.graphics.Rectangle; |
| 43 | +import org.eclipse.swt.internal.DPIUtil; |
43 | 44 | import org.eclipse.swt.layout.FillLayout; |
44 | 45 | import org.eclipse.swt.widgets.Display; |
45 | 46 | import org.eclipse.swt.widgets.Shell; |
@@ -564,14 +565,16 @@ private static boolean hasCodeMiningPrintedBelowLine(ITextViewer viewer, int lin |
564 | 565 | starty= lineBounds.y; |
565 | 566 | } |
566 | 567 |
|
567 | | - Image image= new Image(widget.getDisplay(), (gc, width, height) -> {}, widget.getSize().x, widget.getSize().y); |
| 568 | + Image image= new Image(widget.getDisplay(), (gc, width, height) -> { |
| 569 | + }, (widget.getSize().x), (widget.getSize().y)); |
568 | 570 | try { |
569 | 571 | GC gc= new GC(widget); |
570 | 572 | gc.copyArea(image, 0, 0); |
571 | 573 | gc.dispose(); |
572 | | - ImageData imageData= image.getImageData(); |
573 | | - for (int x= startx + 1; x < image.getBounds().width && x < imageData.width; x++) { |
574 | | - for (int y= starty; y < imageData.height - 10 /*do not include the border*/; y++) { |
| 574 | + ImageData imageData= image.getImageData(DPIUtil.getDeviceZoom()); |
| 575 | + double zoomFactor= DPIUtil.getDeviceZoom() / 100.0; |
| 576 | + for (int x= (int) (zoomFactor * startx + 1); x < image.getBounds().width && x < imageData.width; x++) { |
| 577 | + for (int y= (int) (zoomFactor * starty); y < imageData.height - 10 /*do not include the border*/; y++) { |
575 | 578 | if (!imageData.palette.getRGB(imageData.getPixel(x, y)).equals(widget.getBackground().getRGB())) { |
576 | 579 | // code mining printed |
577 | 580 | return true; |
@@ -604,14 +607,19 @@ private static boolean hasCodeMiningPrintedAfterTextOnLine(ITextViewer viewer, i |
604 | 607 | } else { |
605 | 608 | secondLineBounds= widget.getTextBounds(lineOffset, lineOffset + lineLength); |
606 | 609 | } |
607 | | - Image image = new Image(widget.getDisplay(), (gc, width, height) -> {}, widget.getSize().x, widget.getSize().y); |
| 610 | + |
| 611 | + Image image= new Image(widget.getDisplay(), (gc, width, height) -> { |
| 612 | + }, (widget.getSize().x), (widget.getSize().y)); |
608 | 613 | GC gc = new GC(widget); |
609 | 614 | gc.copyArea(image, 0, 0); |
610 | 615 | gc.dispose(); |
611 | | - ImageData imageData = image.getImageData(); |
| 616 | + ImageData imageData= image.getImageData(DPIUtil.getDeviceZoom()); |
| 617 | + |
612 | 618 | secondLineBounds.x += secondLineBounds.width; // look only area after text |
613 | | - for (int x = secondLineBounds.x + 1; x < image.getBounds().width && x < imageData.width; x++) { |
614 | | - for (int y = secondLineBounds.y; y < secondLineBounds.y + secondLineBounds.height && y < imageData.height; y++) { |
| 619 | + |
| 620 | + double zoomFactor= DPIUtil.getDeviceZoom() / 100.0; |
| 621 | + for (int x= (int) (zoomFactor * (secondLineBounds.x + 1)); x < image.getBounds().width && x < imageData.width; x++) { |
| 622 | + for (int y= (int) (zoomFactor * (secondLineBounds.y)); y < zoomFactor * (secondLineBounds.y + secondLineBounds.height) && y < imageData.height; y++) { |
615 | 623 | if (!imageData.palette.getRGB(imageData.getPixel(x, y)).equals(widget.getBackground().getRGB())) { |
616 | 624 | // code mining printed |
617 | 625 | image.dispose(); |
|
0 commit comments