fixes Location#compareTo(Location) (#3519)

WolframPfeifer · web-flow · commit f8622f610273 · 2024-11-13T18:02:53.000Z
diff --git a/key.core/src/main/java/de/uka/ilkd/key/parser/Location.java b/key.core/src/main/java/de/uka/ilkd/key/parser/Location.java
@@ -94,8 +94,7 @@ public int hashCode() {
 
     @Override
     public int compareTo(@NonNull Location o) {
-        return Comparator
-                .<Location, URI>comparing(l -> l.fileUri)
-                .thenComparing(Location::getPosition).compare(this, o);
+        return Comparator.<Location, URI>comparing(l -> l.fileUri, Comparator.nullsLast(Comparator.naturalOrder()))
+                .thenComparing(Location::getPosition, Comparator.nullsLast(Comparator.naturalOrder())).compare(this, o);
     }
 }

Original file line number	Diff line number	Diff line change
`@@ -94,8 +94,7 @@ public int hashCode() {`
`94`	`94`
`95`	`95`	`@Override`
`96`	`96`	`public int compareTo(@NonNull Location o) {`
`97`		`- return Comparator`
`98`		`- .<Location, URI>comparing(l -> l.fileUri)`
`99`		`- .thenComparing(Location::getPosition).compare(this, o);`
	`97`	`+ return Comparator.<Location, URI>comparing(l -> l.fileUri, Comparator.nullsLast(Comparator.naturalOrder()))`
	`98`	`+ .thenComparing(Location::getPosition, Comparator.nullsLast(Comparator.naturalOrder())).compare(this, o);`
`100`	`99`	`}`
`101`	`100`	`}`