Move exception type "IllegalInstantiationException" to ncore

key.core/src/main/java/de/uka/ilkd/key/control/instantiation_model/TacletFindModel.java

@@ -33,6 +33,7 @@
 import org.key_project.logic.op.Function;
 import org.key_project.logic.op.sv.SchemaVariable;
 import org.key_project.logic.sort.Sort;
+import org.key_project.prover.rules.instantiation.IllegalInstantiationException;
 import org.key_project.util.collection.ImmutableList;
 import org.key_project.util.collection.ImmutableSLList;
 import org.key_project.util.collection.Pair;

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

@@ -16,7 +16,6 @@
 import de.uka.ilkd.key.proof.VariableNameProposer;
 import de.uka.ilkd.key.rule.inst.GenericSortCondition;
 import de.uka.ilkd.key.rule.inst.GenericSortException;
-import de.uka.ilkd.key.rule.inst.IllegalInstantiationException;
 import de.uka.ilkd.key.rule.inst.SVInstantiations.UpdateLabelPair;
 import de.uka.ilkd.key.util.Debug;
 
@@ -28,6 +27,7 @@
 import org.key_project.logic.sort.Sort;
 import org.key_project.prover.rules.*;
 import org.key_project.prover.rules.instantiation.*;
+import org.key_project.prover.rules.instantiation.IllegalInstantiationException;
 import org.key_project.prover.rules.instantiation.MatchConditions;
 import org.key_project.prover.sequent.*;
 import org.key_project.util.collection.*;

key.core/src/main/java/de/uka/ilkd/key/rule/inst/RigidnessException.java

@@ -5,6 +5,8 @@
 
 import java.io.Serial;
 
+import org.key_project.prover.rules.instantiation.IllegalInstantiationException;
+
 /**
  * this exception is thrown if non-rigid instantiation has been given for a schema variable only
  * allowing rigid instantiations

key.core/src/main/java/de/uka/ilkd/key/rule/inst/SVInstantiations.java

@@ -20,6 +20,7 @@
 import org.key_project.logic.LogicServices;
 import org.key_project.logic.Name;
 import org.key_project.logic.op.sv.SchemaVariable;
+import org.key_project.prover.rules.instantiation.IllegalInstantiationException;
 import org.key_project.prover.rules.instantiation.InstantiationEntry;
 import org.key_project.prover.rules.instantiation.ListInstantiation;
 import org.key_project.util.collection.DefaultImmutableMap;

key.core/src/main/java/de/uka/ilkd/key/rule/inst/SortException.java

@@ -3,6 +3,8 @@
  * SPDX-License-Identifier: GPL-2.0-only */
 package de.uka.ilkd.key.rule.inst;
 
+import org.key_project.prover.rules.instantiation.IllegalInstantiationException;
+
 /**
  * this exception is thrown from an "SVInstantiations"-Object if the sorts of a schema variable and
  * its instantiation are not compatible (and not generic)

key.core/src/main/java/de/uka/ilkd/key/rule/match/vm/instructions/MatchProgramSVInstruction.java

@@ -10,11 +10,11 @@
 import de.uka.ilkd.key.logic.op.ProgramSV;
 import de.uka.ilkd.key.logic.sort.ProgramSVSort;
 import de.uka.ilkd.key.rule.MatchConditions;
-import de.uka.ilkd.key.rule.inst.IllegalInstantiationException;
 import de.uka.ilkd.key.rule.inst.SVInstantiations;
 import de.uka.ilkd.key.rule.match.vm.TermNavigator;
 
 import org.key_project.logic.LogicServices;
+import org.key_project.prover.rules.instantiation.IllegalInstantiationException;
 
 import org.slf4j.Logger;
 import org.slf4j.LoggerFactory;

key.core/src/main/java/de/uka/ilkd/key/rule/match/vm/instructions/MatchSchemaVariableInstruction.java

@@ -7,11 +7,11 @@
 import de.uka.ilkd.key.java.Services;
 import de.uka.ilkd.key.logic.Term;
 import de.uka.ilkd.key.rule.MatchConditions;
-import de.uka.ilkd.key.rule.inst.IllegalInstantiationException;
 import de.uka.ilkd.key.rule.inst.SVInstantiations;
 
 import org.key_project.logic.LogicServices;
 import org.key_project.logic.op.sv.OperatorSV;
+import org.key_project.prover.rules.instantiation.IllegalInstantiationException;
 
 import org.slf4j.Logger;
 import org.slf4j.LoggerFactory;
@@ -71,8 +71,7 @@ protected final MatchConditions addInstantiation(Term term, MatchConditions matc
      *         the pair ({@link org.key_project.logic.op.sv.SchemaVariable}, {@link ProgramElement})
      *         added
      */
-    public MatchConditions match(ProgramElement instantiationCandidate,
-            MatchConditions mc,
+    public MatchConditions match(ProgramElement instantiationCandidate, MatchConditions mc,
             LogicServices services) {
         return null;
     }

key.core/src/main/java/de/uka/ilkd/key/settings/ViewSettings.java

@@ -12,7 +12,7 @@
  * maximal number of lines a tooltip with instantiated SchemaVariables is allowed to have. If this
  * number is exceeded no SchemaVariables get instantiated in the displayed tooltip. 3) whether
  * intermediate proofsteps should be hidden in the proof tree view
- *
+ * <br />
  * (see also StandardUISettings)
  *
  * @author unknown
@@ -167,7 +167,7 @@ public class ViewSettings extends AbstractPropertiesSettings {
     private final PropertyEntry<Boolean> showHeatmap = createBooleanProperty(HEATMAP_SHOW, false);
     private final PropertyEntry<Boolean> heatmapSF = createBooleanProperty(HEATMAP_SF, true);
     /**
-     * Highlight newest formulas/terms (true) or all formulas/terms below specified age (false)
+     * Highlight most recent formulas/terms (true) or all formulas/terms below specified age (false)
      */
     private final PropertyEntry<Boolean> heatmapNewest =
         createBooleanProperty(HEATMAP_NEWEST, true);
@@ -419,8 +419,9 @@ public void setUsePretty(boolean usePretty) {
     /**
      * Use Unicode Symbols is only allowed if pretty syntax is used
      *
-     * @return setting of use unicode symbols (if use pretty syntax is on, return the value which is
-     *         set, if use retty is false, return false)
+     * @return setting of "use unicode symbols" (if option "use pretty syntax" is on, return the
+     *         value which is
+     *         set, if "use pretty syntax" is off, return false)
      */
     public boolean isUseUnicode() {
         if (isUsePretty()) {

key.ncore.calculus/src/main/java/org/key_project/prover/rules/VariableCondition.java

@@ -9,7 +9,8 @@
 import org.key_project.prover.rules.instantiation.MatchConditions;
 
 /**
- * The instantiations of a schemavariable can be restricted on rule scope by attaching conditions on
+ * The instantiations of a schema variable can be restricted on rule scope by attaching conditions
+ * on
  * these variables. Such a condition is realized by a class which implements this interface.
  * <br>
  * The usual place where to put these implementations is inside package
@@ -25,7 +26,7 @@ public interface VariableCondition {
      * @param instCandidate the SVSubstitute (e.g. Term, ProgramElement) to be mapped to var
      * @param matchCond the MatchCondition with the current matching state and in particular the
      *        SVInstantiations that are already known to be needed
-     * @param services the program information object
+     * @param services the logic and program information object
      * @return modified match results if the condition can be satisfied, or <code>null</code>
      *         otherwise
      */

key.core/src/main/java/de/uka/ilkd/key/rule/inst/IllegalInstantiationException.java → key.ncore.calculus/src/main/java/org/key_project/prover/rules/instantiation/IllegalInstantiationException.java

@@ -1,7 +1,7 @@
 /* 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 de.uka.ilkd.key.rule.inst;
+package org.key_project.prover.rules.instantiation;
 
 /**
  * this exception is thrown if an invalid instantiation for a schema variable was given

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

@@ -23,13 +23,13 @@
 import de.uka.ilkd.key.logic.Term;
 import de.uka.ilkd.key.pp.PosInSequent;
 import de.uka.ilkd.key.rule.*;
-import de.uka.ilkd.key.rule.inst.IllegalInstantiationException;
 import de.uka.ilkd.key.settings.ProofIndependentSettings;
 
 import org.key_project.logic.PosInTerm;
 import org.key_project.logic.op.sv.SchemaVariable;
 import org.key_project.prover.rules.instantiation.AssumesFormulaInstSeq;
 import org.key_project.prover.rules.instantiation.AssumesFormulaInstantiation;
+import org.key_project.prover.rules.instantiation.IllegalInstantiationException;
 import org.key_project.prover.rules.tacletbuilder.TacletGoalTemplate;
 import org.key_project.prover.sequent.PosInOccurrence;
 import org.key_project.prover.sequent.Sequent;

keyext.rusty/src/main/java/org/key_project/rusty/rule/TacletApp.java

@@ -15,9 +15,7 @@
 import org.key_project.logic.sort.Sort;
 import org.key_project.prover.rules.Rule;
 import org.key_project.prover.rules.RuleApp;
-import org.key_project.prover.rules.instantiation.AssumesFormulaInstSeq;
-import org.key_project.prover.rules.instantiation.AssumesFormulaInstantiation;
-import org.key_project.prover.rules.instantiation.AssumesMatchResult;
+import org.key_project.prover.rules.instantiation.*;
 import org.key_project.prover.rules.instantiation.MatchConditions;
 import org.key_project.prover.rules.instantiation.SVInstantiations;
 import org.key_project.prover.sequent.*;

keyext.rusty/src/main/java/org/key_project/rusty/rule/inst/RigidnessException.java

@@ -5,6 +5,8 @@
 
 import java.io.Serial;
 
+import org.key_project.prover.rules.instantiation.IllegalInstantiationException;
+
 /**
  * this exception is thrown if non-rigid instantiation has been given for a schema variable only
  * allowing rigid instantiations

keyext.rusty/src/main/java/org/key_project/rusty/rule/inst/SVInstantiations.java

@@ -10,6 +10,7 @@
 import org.key_project.logic.Term;
 import org.key_project.logic.op.sv.OperatorSV;
 import org.key_project.logic.op.sv.SchemaVariable;
+import org.key_project.prover.rules.instantiation.IllegalInstantiationException;
 import org.key_project.prover.rules.instantiation.InstantiationEntry;
 import org.key_project.rusty.Services;
 import org.key_project.rusty.ast.RustyProgramElement;

keyext.rusty/src/main/java/org/key_project/rusty/rule/inst/SortException.java

@@ -5,6 +5,8 @@
 
 import java.io.Serial;
 
+import org.key_project.prover.rules.instantiation.IllegalInstantiationException;
+
 /**
  * this exception is thrown from an "SVInstantiations"-Object if the sorts of a schema variable and
  * its instantiation are not compatible (and not generic)
@@ -21,5 +23,4 @@ public SortException(String description) {
         super(description);
     }
 
-
 }

keyext.rusty/src/main/java/org/key_project/rusty/rule/match/instructions/MatchProgramSVInstruction.java

@@ -7,6 +7,7 @@
 import org.key_project.logic.SyntaxElementCursor;
 import org.key_project.logic.Term;
 import org.key_project.logic.op.Operator;
+import org.key_project.prover.rules.instantiation.IllegalInstantiationException;
 import org.key_project.prover.rules.instantiation.MatchConditions;
 import org.key_project.rusty.Services;
 import org.key_project.rusty.ast.RustyProgramElement;
@@ -17,7 +18,6 @@
 import org.key_project.rusty.logic.op.ProgramVariable;
 import org.key_project.rusty.logic.op.sv.ProgramSV;
 import org.key_project.rusty.logic.sort.ProgramSVSort;
-import org.key_project.rusty.rule.inst.IllegalInstantiationException;
 import org.key_project.rusty.rule.inst.SVInstantiations;
 
 import org.jspecify.annotations.NonNull;

keyext.rusty/src/main/java/org/key_project/rusty/rule/match/instructions/MatchSchemaVariableInstruction.java

@@ -7,10 +7,10 @@
 import org.key_project.logic.Term;
 import org.key_project.logic.op.sv.OperatorSV;
 import org.key_project.logic.op.sv.SchemaVariable;
+import org.key_project.prover.rules.instantiation.IllegalInstantiationException;
 import org.key_project.prover.rules.instantiation.MatchConditions;
 import org.key_project.rusty.Services;
 import org.key_project.rusty.ast.RustyProgramElement;
-import org.key_project.rusty.rule.inst.IllegalInstantiationException;
 import org.key_project.rusty.rule.inst.SVInstantiations;
 
 import org.jspecify.annotations.NonNull;