fix rebasing

Author: wadoon

key.core/src/main/java/de/uka/ilkd/key/nparser/builder/TacletPBuilder.java

@@ -27,10 +27,7 @@
 import de.uka.ilkd.key.rule.tacletbuilder.*;
 import de.uka.ilkd.key.util.parsing.BuildingException;
 
-import org.key_project.logic.Choice;
-import org.key_project.logic.ChoiceExpr;
-import org.key_project.logic.Name;
-import org.key_project.logic.Namespace;
+import org.key_project.logic.*;
 import org.key_project.logic.op.Function;
 import org.key_project.logic.op.QuantifiableVariable;
 import org.key_project.logic.op.sv.SchemaVariable;
@@ -139,7 +136,7 @@ public TacletBuilder<?> visitTriggers(KeYParser.TriggersContext ctx) {
         TacletBuilder<?> b = peekTBuilder();
         JTerm t = accept(ctx.t);
         List<JTerm> avoidConditions = mapOf(ctx.avoidCond);
-        b.setTrigger(new Trigger(triggerVar, t, ImmutableList.fromList(avoidConditions)));
+        b.setTrigger(new Trigger(triggerVar, t, ImmutableList.<Term>fromList(avoidConditions)));
         return null;
     }
 
@@ -187,7 +184,6 @@ public Taclet visitTaclet(KeYParser.TacletContext ctx) {
             ifSeq = accept(ctx.ifSeq);
         }
 
-        @Nullable
         Object find = accept(ctx.find);
         Sequent seq = find instanceof Sequent ? (Sequent) find : null;
 
@@ -798,7 +794,7 @@ public Object visitGoalspec(KeYParser.GoalspecContext ctx) {
         String name = accept(ctx.string_value());
 
         Sequent addSeq = JavaDLSequentKit.getInstance().getEmptySequent();
-        ImmutableSLList<Taclet> addRList = ImmutableList.nil();
+        ImmutableList<Taclet> addRList = ImmutableList.nil();
         DefaultImmutableSet<SchemaVariable> addpv = DefaultImmutableSet.nil();
 
         @Nullable

key.core/src/main/java/de/uka/ilkd/key/rule/QueryExpand.java

@@ -38,7 +38,6 @@
 import org.key_project.prover.sequent.SequentFormula;
 import org.key_project.util.collection.ImmutableArray;
 import org.key_project.util.collection.ImmutableList;
-import org.key_project.util.collection.ImmutableSLList;
 import org.key_project.util.collection.Pair;
 
 import org.jspecify.annotations.NonNull;
@@ -281,7 +280,7 @@ public JTerm evaluateQueries(Services services, JTerm term, boolean positiveCont
         final int depth = term.depth();
         List<QueryEvalPos> qeps = new ArrayList<>();
         int[] path = new int[depth];
-        final ImmutableSLList<QuantifiableVariable> instVars;
+        final ImmutableList<QuantifiableVariable> instVars;
         if (allowExpandBelowInstQuantifier) {
             instVars = ImmutableList.nil();
         } else {

key.core/src/main/java/de/uka/ilkd/key/speclang/jml/pretranslation/TextualJMLClassAxiom.java

@@ -26,7 +26,7 @@ public final class TextualJMLClassAxiom extends TextualJMLConstruct {
     public TextualJMLClassAxiom(ImmutableList<JMLModifier> modifiers,
             LabeledParserRuleContext inv) {
         super(ImmutableList.nil()); // no modifiers allowed in axiom clause (see
-                                      // Sect. 8 of reference manual)
+                                    // Sect. 8 of reference manual)
         assert inv != null;
         this.inv = inv;
         setPosition(inv);

key.core/src/main/java/de/uka/ilkd/key/speclang/njml/Translator.java

@@ -43,7 +43,6 @@
 import org.key_project.logic.op.Function;
 import org.key_project.logic.sort.Sort;
 import org.key_project.util.collection.ImmutableList;
-import org.key_project.util.collection.ImmutableSLList;
 import org.key_project.util.collection.Pair;
 
 import org.antlr.v4.runtime.ParserRuleContext;
@@ -1121,7 +1120,7 @@ private SLExpression processJmlBuiltInFunction(String name,
     private SLParameters visitParameters(JmlParser.Param_listContext ctx) {
         ImmutableList<SLExpression> params =
             ctx.param_decl().stream().map(it -> lookupIdentifier(it.p.getText(), null, null, it))
-                    .collect(ImmutableSLList.toImmutableList());
+                    .collect(ImmutableList.collector());
         return getSlParametersWithHeap(params);
     }
 

key.ui/src/main/java/de/uka/ilkd/key/gui/mergerule/MergePartnerSelectionDialog.java

@@ -30,7 +30,6 @@
 
 import org.key_project.prover.sequent.*;
 import org.key_project.util.collection.ImmutableList;
-import org.key_project.util.collection.ImmutableSLList;
 import org.key_project.util.collection.Pair;
 
 /**
@@ -327,7 +326,7 @@ public MergePartnerSelectionDialog(Goal mergeGoal,
      * @return All chosen merge partners.
      */
     public ImmutableList<MergePartner> getChosenCandidates() {
-        ImmutableSLList<MergePartner> result = ImmutableList.nil();
+        ImmutableList<MergePartner> result = ImmutableList.nil();
 
         if (chosenGoals != null) {
             return result.append(chosenGoals);

key.ui/src/main/java/de/uka/ilkd/key/gui/nodeviews/CurrentGoalViewMenu.java

@@ -42,7 +42,6 @@
 import org.key_project.prover.rules.tacletbuilder.TacletGoalTemplate;
 import org.key_project.prover.sequent.PosInOccurrence;
 import org.key_project.util.collection.ImmutableList;
-import org.key_project.util.collection.ImmutableSLList;
 import org.key_project.util.java.StringUtil;
 
 import org.jspecify.annotations.NonNull;
@@ -120,7 +119,7 @@ private static ImmutableList<TacletApp> removeIntroduceAxiomTaclet(
             ImmutableList<TacletApp> list) {
         return list.stream()
                 .filter(app -> !app.rule().name().toString().equals(INTRODUCE_AXIOM_TACLET_NAME))
-                .collect(ImmutableSLList.toImmutableList());
+                .collect(ImmutableList.collector());
     }
 
     /**

key.ui/src/main/java/de/uka/ilkd/key/gui/nodeviews/SequentView.java

@@ -36,7 +36,6 @@
 import org.key_project.prover.sequent.Sequent;
 import org.key_project.prover.sequent.SequentFormula;
 import org.key_project.util.collection.ImmutableList;
-import org.key_project.util.collection.ImmutableSLList;
 
 import org.jspecify.annotations.Nullable;
 import org.slf4j.Logger;
@@ -761,7 +760,7 @@ protected void updateHeatmapSFHighlights(int max_age, boolean newest) {
                 for (int j = 0; j < max_age && j < sortedArray.length; ++j) {
                     if (sortedArray[j].equals(entry)) {
                         Color color = computeColorForAge(max_age, j);
-                        ImmutableSLList<Integer> list = (ImmutableSLList<Integer>) ImmutableList
+                        ImmutableList<Integer> list = (ImmutableList<Integer>) ImmutableList
                                 .<Integer>nil().prepend(0).append(i);
                         Range r = ipt.rangeForPath(list);
                         // Off-by-one: siehe updateUpdateHighlights bzw in InnerNodeView.
@@ -780,7 +779,7 @@ protected void updateHeatmapSFHighlights(int max_age, boolean newest) {
                     form, max_age + 2);
                 if (age < max_age) {
                     Color color = computeColorForAge(max_age, age);
-                    ImmutableSLList<Integer> list = (ImmutableSLList<Integer>) ImmutableList
+                    ImmutableList<Integer> list = (ImmutableList<Integer>) ImmutableList
                             .<Integer>nil().prepend(0).append(i);
                     Range r = ipt.rangeForPath(list);
                     // Off-by-one: siehe updateUpdateHighlights bzw in InnerNodeView. rangeForPath

key.util/src/main/java/org/key_project/util/collection/ImmutableList.java

@@ -3,8 +3,6 @@
  * SPDX-License-Identifier: GPL-2.0-only */
 package org.key_project.util.collection;
 
-import org.jspecify.annotations.Nullable;
-
 import java.lang.reflect.Array;
 import java.util.*;
 import java.util.function.Function;
@@ -14,6 +12,8 @@
 import java.util.stream.Stream;
 import java.util.stream.StreamSupport;
 
+import org.jspecify.annotations.Nullable;
+
 /**
  * List interface to be implemented by non-destructive lists
  */
@@ -80,7 +80,7 @@ public interface ImmutableList<T extends @Nullable Object>
     /**
      * Return a singleton immutable list.
      *
-     * @param e1  the element to put into the list
+     * @param e1 the element to put into the list
      * @param <T> the entry type of the list.
      * @return singleton immutable list.
      */
@@ -92,7 +92,7 @@ public interface ImmutableList<T extends @Nullable Object>
      * Return an immutable list with the iterated elements.
      * The iteration order is the order of the arguments
      *
-     * @param es  the elements to put into the list
+     * @param es the elements to put into the list
      * @param <T> the entry type of the list.
      * @return (e1, e2, e3, ...) as immutable list
      */
@@ -103,11 +103,12 @@ public interface ImmutableList<T extends @Nullable Object>
         return new ImmutableListArray<>(es);
 
         /*
-        ImmutableList<T> result = nil();
-        for (int i = es.length - 1; i >= 0; i--) {
-            result = result.prepend(es[i]);
-        }
-        return result;*/
+         * ImmutableList<T> result = nil();
+         * for (int i = es.length - 1; i >= 0; i--) {
+         * result = result.prepend(es[i]);
+         * }
+         * return result;
+         */
     }
 
     /**
@@ -331,8 +332,8 @@ default List<T> toList() {
      * the given predicate.
      *
      * @param predicate a non-interfering, stateless
-     *                  predicate to apply to each element to determine if it
-     *                  should be included
+     *        predicate to apply to each element to determine if it
+     *        should be included
      * @return the filtered list
      */
     default ImmutableList<T> filter(Predicate<? super T> predicate) {
@@ -343,7 +344,7 @@ default ImmutableList<T> filter(Predicate<? super T> predicate) {
      * Returns an immutable list consisting of the results of applying the given
      * function to the elements of this list.
      *
-     * @param <R>      The element type of the result list
+     * @param <R> The element type of the result list
      * @param function a non-interfering, stateless function to apply to each element
      * @return the mapped list of the same length as this
      */
@@ -411,7 +412,7 @@ default T last() throws NoSuchElementException {
      * @param idx the 0-based index of the element
      * @return the element at index idx.
      * @throws IndexOutOfBoundsException if idx is less than 0 or at
-     *                                   least {@link #size()}.
+     *         least {@link #size()}.
      */
     T get(int idx);
 

key.util/src/main/java/org/key_project/util/collection/ImmutableListArray.java

@@ -1,7 +1,8 @@
+/* This file is part of KeY - https://key-project.org
+ * KeY is licensed under the GNU General Public License Version 2
+ * SPDX-License-Identifier: GPL-2.0-only */
 package org.key_project.util.collection;
 
-import org.jspecify.annotations.Nullable;
-
 import java.lang.reflect.Array;
 import java.util.Arrays;
 import java.util.Iterator;
@@ -11,6 +12,8 @@
 import java.util.function.Predicate;
 import java.util.stream.Stream;
 
+import org.jspecify.annotations.Nullable;
+
 /**
  *
  * @author Alexander Weigl
@@ -101,7 +104,7 @@ public ImmutableList<T> removeAll(T obj) {
         return stream().filter(it -> !Objects.equals(it, obj)).collect(ImmutableList.collector());
     }
 
-    @SuppressWarnings({"unchecked", "argument.type.incompatible"})
+    @SuppressWarnings({ "unchecked", "argument.type.incompatible" })
     @Override
     public <S extends @Nullable Object> S[] toArray(S[] array) {
         if (array.length == size()) {

key.util/src/main/java/org/key_project/util/collection/ImmutableListConcat.java

@@ -1,11 +1,14 @@
+/* This file is part of KeY - https://key-project.org
+ * KeY is licensed under the GNU General Public License Version 2
+ * SPDX-License-Identifier: GPL-2.0-only */
 package org.key_project.util.collection;
 
-import org.jspecify.annotations.Nullable;
-
 import java.util.Objects;
 import java.util.function.Predicate;
 import java.util.stream.Collectors;
 
+import org.jspecify.annotations.Nullable;
+
 /**
  *
  * @author Alexander Weigl
@@ -64,7 +67,8 @@ public ImmutableList<T> removeAll(T obj) {
 
     @Override
     public boolean equals(Object obj) {
-        if (obj == this) return true;
+        if (obj == this)
+            return true;
         if (obj instanceof ImmutableList<?> other) {
             return ImmutableList.equals(this, other);
         }