Skip to content

Commit 23d708c

Browse files
committed
fixed fit to screen infinite loop when placing a single place
1 parent 9010302 commit 23d708c

File tree

2 files changed

+8
-2
lines changed

2 files changed

+8
-2
lines changed

src/main/java/pipe/gui/GuiFrame.java

+1
Original file line numberDiff line numberDiff line change
@@ -276,6 +276,7 @@ public void actionPerformed(ActionEvent e) {
276276
putValue(Action.NAME, FIT_TO_SCREEN_NAME);
277277
putValue(Action.SHORT_DESCRIPTION, FIT_TO_SCREEN_TOOLTIP);
278278
putValue(Action.SMALL_ICON, ResourceManager.getIcon(FIT_TO_SCREEN_ICON));
279+
o.setIsAlreadyFitToScreen(false);
279280
}
280281
});
281282
}

src/main/java/pipe/gui/petrinet/PetriNetTab.java

+7-2
Original file line numberDiff line numberDiff line change
@@ -1861,9 +1861,11 @@ public void fitToScreen() {
18611861
final int margin = 50;
18621862

18631863
// Loop until it converges
1864+
Double prevZoom = null;
18641865
while (true) {
18651866
Iterable<PetriNetObject> petriNetObjects = currentTemplate().guiModel().getPetriNetObjects();
18661867
if (!petriNetObjects.iterator().hasNext()) {
1868+
alreadyFitToScreen = true;
18671869
return;
18681870
}
18691871

@@ -1947,12 +1949,13 @@ public void fitToScreen() {
19471949
double xZoomFactor = (double) viewport.getWidth() / width;
19481950
double yZoomFactor = (double) viewport.getHeight() / height;
19491951
double zoomFactor = Math.min(xZoomFactor, yZoomFactor);
1950-
double zoomPercent = Math.min(xZoomFactor, yZoomFactor) * 100;
1952+
double zoomPercent = zoomFactor * 100;
19511953

19521954
double currentZoomPercent = drawingSurface().getZoomController().getPercent();
19531955

19541956
final double zoomConvergence = 1;
1955-
if (Math.abs(currentZoomPercent - zoomPercent) < zoomConvergence) {
1957+
final double current = Math.abs(currentZoomPercent - zoomPercent);
1958+
if (current < zoomConvergence || (prevZoom != null && current == prevZoom)) {
19561959
int x = (int) (smallestX * zoomFactor) - margin;
19571960
int y = (int) (smallestY * zoomFactor) - margin;
19581961

@@ -1964,6 +1967,8 @@ public void fitToScreen() {
19641967
return;
19651968
}
19661969

1970+
prevZoom = current;
1971+
19671972
app.ifPresent(e -> e.updateZoomSlider((int)zoomPercent));
19681973
}
19691974
}

0 commit comments

Comments
 (0)