diff --git a/build.gradle b/build.gradle index 5bb1ef3456b..e9d8cf09c22 100644 --- a/build.gradle +++ b/build.gradle @@ -64,9 +64,12 @@ subprojects { repositories { mavenCentral() - maven { + maven { // cleary if needed?! url 'https://git.key-project.org/api/v4/projects/35/packages/maven' } + maven { // remove if docking frames 1.1.3p2 on Maven Central + url "https://s01.oss.sonatype.org/content/repositories/snapshots/" + } } dependencies { @@ -77,8 +80,6 @@ subprojects { testImplementation 'org.junit.jupiter:junit-jupiter-params:5.10.2' testImplementation project(':key.util') - testCompileOnly 'junit:junit:4.13.2' - testRuntimeOnly 'org.junit.vintage:junit-vintage-engine:5.10.2' testRuntimeOnly 'org.junit.jupiter:junit-jupiter-engine:5.10.2' implementation("org.jspecify:jspecify:0.3.0") diff --git a/key.core.example/src/main/java/module-info.java b/key.core.example/src/main/java/module-info.java new file mode 100644 index 00000000000..01e7c518413 --- /dev/null +++ b/key.core.example/src/main/java/module-info.java @@ -0,0 +1,10 @@ +/** + * + * @author Alexander Weigl + * @version 1 (31.03.24) + */ +module org.key_project.core.example { + requires org.key_project.core; + requires org.key_project.util; + requires org.slf4j; +} \ No newline at end of file diff --git a/key.core.proof_references/src/main/java/module-info.java b/key.core.proof_references/src/main/java/module-info.java new file mode 100644 index 00000000000..caf7a2d3c10 --- /dev/null +++ b/key.core.proof_references/src/main/java/module-info.java @@ -0,0 +1,10 @@ +/** + * + * @author Alexander Weigl + * @version 1 (31.03.24) + */ +module org.key_project.proof_references { + requires org.key_project.core; + requires org.key_project.ncore; + requires org.key_project.util; +} \ No newline at end of file diff --git a/key.core.rifl/src/main/java/module-info.java b/key.core.rifl/src/main/java/module-info.java new file mode 100644 index 00000000000..6a21411cf8d --- /dev/null +++ b/key.core.rifl/src/main/java/module-info.java @@ -0,0 +1,13 @@ +/** + * + * @author Alexander Weigl + * @version 1 (31.03.24) + */ +module org.key_project.core.rifl { + exports de.uka.ilkd.key.util.rifl; + requires org.key_project.core; + requires key.recoder; + requires java.xml; + requires org.slf4j; + requires org.key_project.util; +} \ No newline at end of file diff --git a/key.core.symbolic_execution.example/src/main/java/module-info.java b/key.core.symbolic_execution.example/src/main/java/module-info.java new file mode 100644 index 00000000000..a708dfbef82 --- /dev/null +++ b/key.core.symbolic_execution.example/src/main/java/module-info.java @@ -0,0 +1,11 @@ +/** + * + * @author Alexander Weigl + * @version 1 (31.03.24) + */ +module key.core.symbolic_execution.example { + requires transitive org.key_project.symbolic_execution; + requires org.key_project.core; + requires org.key_project.util; + requires org.slf4j; +} \ No newline at end of file diff --git a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/rule/label/BlockContractValidityTermLabelUpdate.java b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/label/BlockContractValidityTermLabelUpdate.java similarity index 95% rename from key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/rule/label/BlockContractValidityTermLabelUpdate.java rename to key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/label/BlockContractValidityTermLabelUpdate.java index 313d77c0f91..6d72e3bc0b5 100644 --- a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/rule/label/BlockContractValidityTermLabelUpdate.java +++ b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/label/BlockContractValidityTermLabelUpdate.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.label; +package de.uka.ilkd.key.symbolic_execution.label; import java.util.Set; @@ -15,6 +15,7 @@ import de.uka.ilkd.key.rule.LoopContractInternalRule; import de.uka.ilkd.key.rule.Rule; import de.uka.ilkd.key.rule.RuleApp; +import de.uka.ilkd.key.rule.label.TermLabelUpdate; import de.uka.ilkd.key.symbolic_execution.util.SymbolicExecutionUtil; import org.key_project.logic.Name; diff --git a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/rule/label/FormulaTermLabelMerger.java b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/label/FormulaTermLabelMerger.java similarity index 94% rename from key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/rule/label/FormulaTermLabelMerger.java rename to key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/label/FormulaTermLabelMerger.java index da7e85f8a9e..9bb27da2d7a 100644 --- a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/rule/label/FormulaTermLabelMerger.java +++ b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/label/FormulaTermLabelMerger.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.label; +package de.uka.ilkd.key.symbolic_execution.label; import java.util.ArrayList; import java.util.Arrays; @@ -11,6 +11,7 @@ import de.uka.ilkd.key.logic.Term; import de.uka.ilkd.key.logic.label.FormulaTermLabel; import de.uka.ilkd.key.logic.label.TermLabel; +import de.uka.ilkd.key.rule.label.TermLabelMerger; /** * The {@link TermLabelMerger} used to merge {@link FormulaTermLabel}s. diff --git a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/rule/label/FormulaTermLabelRefactoring.java b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/label/FormulaTermLabelRefactoring.java similarity index 99% rename from key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/rule/label/FormulaTermLabelRefactoring.java rename to key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/label/FormulaTermLabelRefactoring.java index 8773f536ec1..7126d919feb 100644 --- a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/rule/label/FormulaTermLabelRefactoring.java +++ b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/label/FormulaTermLabelRefactoring.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.label; +package de.uka.ilkd.key.symbolic_execution.label; import java.util.*; @@ -15,6 +15,8 @@ import de.uka.ilkd.key.proof.Proof; import de.uka.ilkd.key.rule.Rule; import de.uka.ilkd.key.rule.SyntacticalReplaceVisitor; +import de.uka.ilkd.key.rule.label.StayOnOperatorTermLabelPolicy; +import de.uka.ilkd.key.rule.label.TermLabelRefactoring; import de.uka.ilkd.key.rule.merge.CloseAfterMerge; import de.uka.ilkd.key.symbolic_execution.TruthValueTracingUtil; diff --git a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/rule/label/FormulaTermLabelUpdate.java b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/label/FormulaTermLabelUpdate.java similarity index 98% rename from key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/rule/label/FormulaTermLabelUpdate.java rename to key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/label/FormulaTermLabelUpdate.java index 2ae4dbc912d..1c68b0d8984 100644 --- a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/rule/label/FormulaTermLabelUpdate.java +++ b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/label/FormulaTermLabelUpdate.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.label; +package de.uka.ilkd.key.symbolic_execution.label; import java.util.Collections; import java.util.LinkedHashMap; @@ -21,6 +21,7 @@ import de.uka.ilkd.key.rule.Taclet.TacletLabelHint; import de.uka.ilkd.key.rule.Taclet.TacletLabelHint.TacletOperation; import de.uka.ilkd.key.rule.TacletApp; +import de.uka.ilkd.key.rule.label.TermLabelUpdate; import de.uka.ilkd.key.symbolic_execution.TruthValueTracingUtil; import org.key_project.logic.Name; diff --git a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/rule/label/LoopBodyTermLabelUpdate.java b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/label/LoopBodyTermLabelUpdate.java similarity index 94% rename from key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/rule/label/LoopBodyTermLabelUpdate.java rename to key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/label/LoopBodyTermLabelUpdate.java index c53d6be78c0..9083cb56442 100644 --- a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/rule/label/LoopBodyTermLabelUpdate.java +++ b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/label/LoopBodyTermLabelUpdate.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.label; +package de.uka.ilkd.key.symbolic_execution.label; import java.util.Set; @@ -13,6 +13,7 @@ import de.uka.ilkd.key.rule.Rule; import de.uka.ilkd.key.rule.RuleApp; import de.uka.ilkd.key.rule.WhileInvariantRule; +import de.uka.ilkd.key.rule.label.TermLabelUpdate; import de.uka.ilkd.key.symbolic_execution.util.SymbolicExecutionUtil; import org.key_project.logic.Name; diff --git a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/rule/label/LoopInvariantNormalBehaviorTermLabelUpdate.java b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/label/LoopInvariantNormalBehaviorTermLabelUpdate.java similarity index 94% rename from key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/rule/label/LoopInvariantNormalBehaviorTermLabelUpdate.java rename to key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/label/LoopInvariantNormalBehaviorTermLabelUpdate.java index 1ad966ad364..8f0fcb0d43a 100644 --- a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/rule/label/LoopInvariantNormalBehaviorTermLabelUpdate.java +++ b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/label/LoopInvariantNormalBehaviorTermLabelUpdate.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.label; +package de.uka.ilkd.key.symbolic_execution.label; import java.util.Set; @@ -13,6 +13,7 @@ import de.uka.ilkd.key.rule.Rule; import de.uka.ilkd.key.rule.RuleApp; import de.uka.ilkd.key.rule.WhileInvariantRule; +import de.uka.ilkd.key.rule.label.TermLabelUpdate; import de.uka.ilkd.key.symbolic_execution.util.SymbolicExecutionUtil; import org.key_project.logic.Name; diff --git a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/rule/label/RemoveInCheckBranchesTermLabelRefactoring.java b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/label/RemoveInCheckBranchesTermLabelRefactoring.java similarity index 97% rename from key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/rule/label/RemoveInCheckBranchesTermLabelRefactoring.java rename to key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/label/RemoveInCheckBranchesTermLabelRefactoring.java index 065bde102a4..c85d1d9f645 100644 --- a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/rule/label/RemoveInCheckBranchesTermLabelRefactoring.java +++ b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/label/RemoveInCheckBranchesTermLabelRefactoring.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.label; +package de.uka.ilkd.key.symbolic_execution.label; import de.uka.ilkd.key.java.Services; import de.uka.ilkd.key.logic.PosInOccurrence; @@ -18,6 +18,7 @@ import de.uka.ilkd.key.rule.Rule; import de.uka.ilkd.key.rule.UseOperationContractRule; import de.uka.ilkd.key.rule.WhileInvariantRule; +import de.uka.ilkd.key.rule.label.TermLabelRefactoring; import org.key_project.logic.Name; import org.key_project.util.collection.ImmutableList; diff --git a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/rule/label/StayOnFormulaTermLabelPolicy.java b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/label/StayOnFormulaTermLabelPolicy.java similarity index 98% rename from key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/rule/label/StayOnFormulaTermLabelPolicy.java rename to key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/label/StayOnFormulaTermLabelPolicy.java index 7d2ea52c692..a20bfdf22ae 100644 --- a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/rule/label/StayOnFormulaTermLabelPolicy.java +++ b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/label/StayOnFormulaTermLabelPolicy.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.label; +package de.uka.ilkd.key.symbolic_execution.label; import java.util.Deque; import java.util.LinkedHashSet; @@ -18,6 +18,7 @@ import de.uka.ilkd.key.rule.Rule; import de.uka.ilkd.key.rule.Taclet.TacletLabelHint; import de.uka.ilkd.key.rule.Taclet.TacletLabelHint.TacletOperation; +import de.uka.ilkd.key.rule.label.TermLabelPolicy; import de.uka.ilkd.key.symbolic_execution.TruthValueTracingUtil; import org.key_project.util.collection.ImmutableArray; diff --git a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/rule/label/SymbolicExecutionTermLabelUpdate.java b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/label/SymbolicExecutionTermLabelUpdate.java similarity index 96% rename from key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/rule/label/SymbolicExecutionTermLabelUpdate.java rename to key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/label/SymbolicExecutionTermLabelUpdate.java index 49c0ba3a0a9..de1ea5d5d92 100644 --- a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/rule/label/SymbolicExecutionTermLabelUpdate.java +++ b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/label/SymbolicExecutionTermLabelUpdate.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.label; +package de.uka.ilkd.key.symbolic_execution.label; import java.util.Set; @@ -12,6 +12,7 @@ import de.uka.ilkd.key.logic.label.TermLabel; import de.uka.ilkd.key.logic.label.TermLabelState; import de.uka.ilkd.key.rule.*; +import de.uka.ilkd.key.rule.label.TermLabelUpdate; import org.key_project.logic.Name; import org.key_project.util.collection.ImmutableList; diff --git a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/model/IExecutionTermination.java b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/model/IExecutionTermination.java index 5b07fb2f76b..4e71b6ba876 100644 --- a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/model/IExecutionTermination.java +++ b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/model/IExecutionTermination.java @@ -8,7 +8,6 @@ import de.uka.ilkd.key.logic.op.IProgramVariable; import de.uka.ilkd.key.proof.Proof; import de.uka.ilkd.key.symbolic_execution.SymbolicExecutionTreeBuilder; -import de.uka.ilkd.key.symbolic_execution.model.impl.ExecutionTermination; import org.key_project.logic.sort.Sort; @@ -19,7 +18,9 @@ * in case of exceptional termination. *

*

- * The default implementation is {@link ExecutionTermination} which is instantiated via a + * The default implementation is + * {@link de.uka.ilkd.key.symbolic_execution.model.impl.ExecutionTermination} + * which is instantiated via a * {@link SymbolicExecutionTreeBuilder} instance. *

* diff --git a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/profile/SymbolicExecutionJavaProfile.java b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/profile/SymbolicExecutionJavaProfile.java index 9b477da0217..86d3218e809 100644 --- a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/profile/SymbolicExecutionJavaProfile.java +++ b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/profile/SymbolicExecutionJavaProfile.java @@ -18,20 +18,20 @@ import de.uka.ilkd.key.proof.init.Profile; import de.uka.ilkd.key.prover.GoalChooserBuilder; import de.uka.ilkd.key.rule.BuiltInRule; -import de.uka.ilkd.key.rule.label.BlockContractValidityTermLabelUpdate; -import de.uka.ilkd.key.rule.label.FormulaTermLabelMerger; -import de.uka.ilkd.key.rule.label.FormulaTermLabelRefactoring; -import de.uka.ilkd.key.rule.label.FormulaTermLabelUpdate; -import de.uka.ilkd.key.rule.label.LoopBodyTermLabelUpdate; -import de.uka.ilkd.key.rule.label.LoopInvariantNormalBehaviorTermLabelUpdate; -import de.uka.ilkd.key.rule.label.RemoveInCheckBranchesTermLabelRefactoring; -import de.uka.ilkd.key.rule.label.StayOnFormulaTermLabelPolicy; import de.uka.ilkd.key.rule.label.StayOnOperatorTermLabelPolicy; -import de.uka.ilkd.key.rule.label.SymbolicExecutionTermLabelUpdate; import de.uka.ilkd.key.rule.label.TermLabelPolicy; import de.uka.ilkd.key.rule.label.TermLabelRefactoring; import de.uka.ilkd.key.rule.label.TermLabelUpdate; import de.uka.ilkd.key.strategy.StrategyFactory; +import de.uka.ilkd.key.symbolic_execution.label.BlockContractValidityTermLabelUpdate; +import de.uka.ilkd.key.symbolic_execution.label.FormulaTermLabelMerger; +import de.uka.ilkd.key.symbolic_execution.label.FormulaTermLabelRefactoring; +import de.uka.ilkd.key.symbolic_execution.label.FormulaTermLabelUpdate; +import de.uka.ilkd.key.symbolic_execution.label.LoopBodyTermLabelUpdate; +import de.uka.ilkd.key.symbolic_execution.label.LoopInvariantNormalBehaviorTermLabelUpdate; +import de.uka.ilkd.key.symbolic_execution.label.RemoveInCheckBranchesTermLabelRefactoring; +import de.uka.ilkd.key.symbolic_execution.label.StayOnFormulaTermLabelPolicy; +import de.uka.ilkd.key.symbolic_execution.label.SymbolicExecutionTermLabelUpdate; import de.uka.ilkd.key.symbolic_execution.rule.ModalitySideProofRule; import de.uka.ilkd.key.symbolic_execution.rule.QuerySideProofRule; import de.uka.ilkd.key.symbolic_execution.strategy.SymbolicExecutionGoalChooserBuilder; diff --git a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/proof/TermProgramVariableCollectorKeepUpdatesForBreakpointconditions.java b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/proof/TermProgramVariableCollectorKeepUpdatesForBreakpointconditions.java similarity index 90% rename from key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/proof/TermProgramVariableCollectorKeepUpdatesForBreakpointconditions.java rename to key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/proof/TermProgramVariableCollectorKeepUpdatesForBreakpointconditions.java index 5dc88746613..e83141d4cf4 100644 --- a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/proof/TermProgramVariableCollectorKeepUpdatesForBreakpointconditions.java +++ b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/proof/TermProgramVariableCollectorKeepUpdatesForBreakpointconditions.java @@ -1,13 +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 de.uka.ilkd.key.proof; +package de.uka.ilkd.key.symbolic_execution.proof; import de.uka.ilkd.key.java.Services; import de.uka.ilkd.key.logic.Term; import de.uka.ilkd.key.logic.op.LocationVariable; import de.uka.ilkd.key.logic.op.Modality; -import de.uka.ilkd.key.strategy.IBreakpointStopCondition; +import de.uka.ilkd.key.proof.TermProgramVariableCollector; +import de.uka.ilkd.key.symbolic_execution.strategy.IBreakpointStopCondition; import de.uka.ilkd.key.symbolic_execution.strategy.breakpoint.AbstractConditionalBreakpoint; import de.uka.ilkd.key.symbolic_execution.strategy.breakpoint.IBreakpoint; diff --git a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/strategy/BreakpointStopCondition.java b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/strategy/BreakpointStopCondition.java index a6adc3159d0..06447d62f5f 100644 --- a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/strategy/BreakpointStopCondition.java +++ b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/strategy/BreakpointStopCondition.java @@ -15,7 +15,6 @@ import de.uka.ilkd.key.proof.Proof; import de.uka.ilkd.key.prover.impl.SingleRuleApplicationInfo; import de.uka.ilkd.key.rule.RuleApp; -import de.uka.ilkd.key.strategy.IBreakpointStopCondition; import de.uka.ilkd.key.symbolic_execution.strategy.breakpoint.IBreakpoint; /** diff --git a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/strategy/IBreakpointStopCondition.java b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/strategy/IBreakpointStopCondition.java similarity index 95% rename from key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/strategy/IBreakpointStopCondition.java rename to key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/strategy/IBreakpointStopCondition.java index 59d9346631d..58eed615d8a 100644 --- a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/strategy/IBreakpointStopCondition.java +++ b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/strategy/IBreakpointStopCondition.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.strategy; +package de.uka.ilkd.key.symbolic_execution.strategy; import java.util.Set; diff --git a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/strategy/SymbolicExecutionBreakpointStopCondition.java b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/strategy/SymbolicExecutionBreakpointStopCondition.java index aac43f10d51..9bb2e5ab060 100644 --- a/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/strategy/SymbolicExecutionBreakpointStopCondition.java +++ b/key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/strategy/SymbolicExecutionBreakpointStopCondition.java @@ -14,7 +14,6 @@ import de.uka.ilkd.key.proof.NodeInfo; import de.uka.ilkd.key.proof.Proof; import de.uka.ilkd.key.rule.RuleApp; -import de.uka.ilkd.key.strategy.IBreakpointStopCondition; import de.uka.ilkd.key.symbolic_execution.strategy.breakpoint.IBreakpoint; /** diff --git a/key.core.symbolic_execution/src/main/java/module-info.java b/key.core.symbolic_execution/src/main/java/module-info.java new file mode 100644 index 00000000000..85d5f648cdd --- /dev/null +++ b/key.core.symbolic_execution/src/main/java/module-info.java @@ -0,0 +1,13 @@ +import de.uka.ilkd.key.proof.init.DefaultProfileResolver; +import de.uka.ilkd.key.proof.init.POExtension; +import de.uka.ilkd.key.symbolic_execution.po.TruthValuePOExtension; +import de.uka.ilkd.key.symbolic_execution.profile.SymbolicExecutionJavaProfileDefaultProfileResolver; + +/** + * + * @author Alexander Weigl + * @version 1 (31.03.24) + */ +module org.key_project.symbolic_execution{exports de.uka.ilkd.key.symbolic_execution;exports de.uka.ilkd.key.symbolic_execution.model;exports de.uka.ilkd.key.symbolic_execution.po;exports de.uka.ilkd.key.symbolic_execution.profile;exports de.uka.ilkd.key.symbolic_execution.strategy;exports de.uka.ilkd.key.symbolic_execution.strategy.breakpoint;exports de.uka.ilkd.key.symbolic_execution.util;requires java.xml;requires org.key_project.core;requires org.key_project.ncore;requires org.key_project.util;requires java.desktop;requires org.slf4j;requires org.jspecify; + +provides DefaultProfileResolver with SymbolicExecutionJavaProfileDefaultProfileResolver;provides POExtension with TruthValuePOExtension;} diff --git a/key.core.symbolic_execution/src/test/java/de/uka/ilkd/key/symbolic_execution/testcase/AbstractSymbolicExecutionTestCase.java b/key.core.symbolic_execution/src/test/java/de/uka/ilkd/key/symbolic_execution/testcase/AbstractSymbolicExecutionTestCase.java index 95c6da8fe33..37d7ae297ed 100644 --- a/key.core.symbolic_execution/src/test/java/de/uka/ilkd/key/symbolic_execution/testcase/AbstractSymbolicExecutionTestCase.java +++ b/key.core.symbolic_execution/src/test/java/de/uka/ilkd/key/symbolic_execution/testcase/AbstractSymbolicExecutionTestCase.java @@ -20,7 +20,6 @@ import de.uka.ilkd.key.proof.Goal; import de.uka.ilkd.key.proof.Node; import de.uka.ilkd.key.proof.Proof; -import de.uka.ilkd.key.proof.TermProgramVariableCollectorKeepUpdatesForBreakpointconditions; import de.uka.ilkd.key.proof.init.FunctionalOperationContractPO; import de.uka.ilkd.key.proof.init.ProofInputException; import de.uka.ilkd.key.proof.init.ProofOblInput; @@ -39,6 +38,7 @@ import de.uka.ilkd.key.symbolic_execution.po.ProgramMethodPO; import de.uka.ilkd.key.symbolic_execution.po.ProgramMethodSubsetPO; import de.uka.ilkd.key.symbolic_execution.profile.SymbolicExecutionJavaProfile; +import de.uka.ilkd.key.symbolic_execution.proof.TermProgramVariableCollectorKeepUpdatesForBreakpointconditions; import de.uka.ilkd.key.symbolic_execution.strategy.*; import de.uka.ilkd.key.symbolic_execution.util.SymbolicExecutionEnvironment; import de.uka.ilkd.key.symbolic_execution.util.SymbolicExecutionUtil; diff --git a/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/ModelGenerator.java b/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/ModelGenerator.java index 0b66418b71b..83f710ef535 100644 --- a/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/ModelGenerator.java +++ b/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/ModelGenerator.java @@ -21,12 +21,12 @@ import de.uka.ilkd.key.settings.ProofDependentSMTSettings; import de.uka.ilkd.key.settings.ProofIndependentSMTSettings; import de.uka.ilkd.key.settings.ProofIndependentSettings; -import de.uka.ilkd.key.settings.TestGenerationSettings; import de.uka.ilkd.key.smt.*; import de.uka.ilkd.key.smt.lang.SMTSort; import de.uka.ilkd.key.smt.model.Model; import de.uka.ilkd.key.smt.solvertypes.SolverType; import de.uka.ilkd.key.smt.solvertypes.SolverTypes; +import de.uka.ilkd.key.testgen.settings.TestGenerationSettings; import org.key_project.util.collection.ImmutableList; import org.key_project.util.collection.ImmutableSLList; diff --git a/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/TestCaseGenerator.java b/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/TestCaseGenerator.java index c652b73a373..c908a86a118 100644 --- a/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/TestCaseGenerator.java +++ b/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/TestCaseGenerator.java @@ -20,15 +20,15 @@ import de.uka.ilkd.key.proof.Node; import de.uka.ilkd.key.proof.Proof; import de.uka.ilkd.key.settings.ProofIndependentSettings; -import de.uka.ilkd.key.settings.TestGenerationSettings; import de.uka.ilkd.key.smt.SMTSolver; import de.uka.ilkd.key.smt.model.Heap; import de.uka.ilkd.key.smt.model.Model; import de.uka.ilkd.key.smt.model.ObjectVal; -import de.uka.ilkd.key.smt.testgen.TestGenerationLog; import de.uka.ilkd.key.testgen.oracle.OracleGenerator; import de.uka.ilkd.key.testgen.oracle.OracleMethod; import de.uka.ilkd.key.testgen.oracle.OracleMethodCall; +import de.uka.ilkd.key.testgen.settings.TestGenerationSettings; +import de.uka.ilkd.key.testgen.smt.testgen.TestGenerationLog; import de.uka.ilkd.key.util.KeYConstants; import org.key_project.logic.op.Function; diff --git a/key.core.testgen/src/main/java/de/uka/ilkd/key/macros/SemanticsBlastingMacro.java b/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/macros/SemanticsBlastingMacro.java similarity index 98% rename from key.core.testgen/src/main/java/de/uka/ilkd/key/macros/SemanticsBlastingMacro.java rename to key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/macros/SemanticsBlastingMacro.java index 30e2db9dc14..47e751e406a 100644 --- a/key.core.testgen/src/main/java/de/uka/ilkd/key/macros/SemanticsBlastingMacro.java +++ b/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/macros/SemanticsBlastingMacro.java @@ -1,11 +1,12 @@ /* 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.macros; +package de.uka.ilkd.key.testgen.macros; import java.util.HashSet; import java.util.Set; +import de.uka.ilkd.key.macros.AbstractBlastingMacro; import de.uka.ilkd.key.proof.rulefilter.RuleFilter; import de.uka.ilkd.key.rule.Rule; diff --git a/key.core.testgen/src/main/java/de/uka/ilkd/key/macros/TestGenMacro.java b/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/macros/TestGenMacro.java similarity index 94% rename from key.core.testgen/src/main/java/de/uka/ilkd/key/macros/TestGenMacro.java rename to key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/macros/TestGenMacro.java index 8a5da4014c5..866454c1782 100644 --- a/key.core.testgen/src/main/java/de/uka/ilkd/key/macros/TestGenMacro.java +++ b/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/macros/TestGenMacro.java @@ -1,22 +1,25 @@ /* 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.macros; +package de.uka.ilkd.key.testgen.macros; import java.util.HashSet; import java.util.Set; import de.uka.ilkd.key.logic.PosInOccurrence; +import de.uka.ilkd.key.macros.FilterStrategy; +import de.uka.ilkd.key.macros.ModalityCache; +import de.uka.ilkd.key.macros.StrategyProofMacro; import de.uka.ilkd.key.proof.Goal; import de.uka.ilkd.key.proof.Node; import de.uka.ilkd.key.proof.Proof; import de.uka.ilkd.key.rule.Rule; import de.uka.ilkd.key.rule.RuleApp; -import de.uka.ilkd.key.settings.TestGenerationSettings; import de.uka.ilkd.key.strategy.NumberRuleAppCost; import de.uka.ilkd.key.strategy.RuleAppCost; import de.uka.ilkd.key.strategy.Strategy; import de.uka.ilkd.key.strategy.feature.MutableState; +import de.uka.ilkd.key.testgen.settings.TestGenerationSettings; import org.key_project.logic.Name; diff --git a/key.core.testgen/src/main/java/de/uka/ilkd/key/settings/TestGenerationSettings.java b/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/settings/TestGenerationSettings.java similarity index 97% rename from key.core.testgen/src/main/java/de/uka/ilkd/key/settings/TestGenerationSettings.java rename to key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/settings/TestGenerationSettings.java index 96d99994211..6fc02bb25d8 100644 --- a/key.core.testgen/src/main/java/de/uka/ilkd/key/settings/TestGenerationSettings.java +++ b/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/settings/TestGenerationSettings.java @@ -1,11 +1,16 @@ /* 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.settings; +package de.uka.ilkd.key.testgen.settings; import java.io.File; import java.util.Properties; +import de.uka.ilkd.key.settings.AbstractSettings; +import de.uka.ilkd.key.settings.Configuration; +import de.uka.ilkd.key.settings.ProofIndependentSettings; +import de.uka.ilkd.key.settings.SettingsConverter; + import org.jspecify.annotations.NonNull; import org.jspecify.annotations.Nullable; diff --git a/key.core.testgen/src/main/java/de/uka/ilkd/key/smt/counterexample/AbstractCounterExampleGenerator.java b/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/smt/counterexample/AbstractCounterExampleGenerator.java similarity index 98% rename from key.core.testgen/src/main/java/de/uka/ilkd/key/smt/counterexample/AbstractCounterExampleGenerator.java rename to key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/smt/counterexample/AbstractCounterExampleGenerator.java index 61546a95392..bb4d41100dd 100644 --- a/key.core.testgen/src/main/java/de/uka/ilkd/key/smt/counterexample/AbstractCounterExampleGenerator.java +++ b/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/smt/counterexample/AbstractCounterExampleGenerator.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.smt.counterexample; +package de.uka.ilkd.key.testgen.smt.counterexample; import java.util.LinkedList; import java.util.List; @@ -9,7 +9,6 @@ import de.uka.ilkd.key.control.UserInterfaceControl; import de.uka.ilkd.key.logic.Sequent; import de.uka.ilkd.key.macros.ProofMacroFinishedInfo; -import de.uka.ilkd.key.macros.SemanticsBlastingMacro; import de.uka.ilkd.key.proof.Proof; import de.uka.ilkd.key.proof.init.ProofInputException; import de.uka.ilkd.key.prover.ProverTaskListener; @@ -21,6 +20,7 @@ import de.uka.ilkd.key.smt.*; import de.uka.ilkd.key.smt.solvertypes.SolverType; import de.uka.ilkd.key.smt.solvertypes.SolverTypes; +import de.uka.ilkd.key.testgen.macros.SemanticsBlastingMacro; import org.slf4j.Logger; import org.slf4j.LoggerFactory; diff --git a/key.core.testgen/src/main/java/de/uka/ilkd/key/smt/counterexample/AbstractSideProofCounterExampleGenerator.java b/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/smt/counterexample/AbstractSideProofCounterExampleGenerator.java similarity index 96% rename from key.core.testgen/src/main/java/de/uka/ilkd/key/smt/counterexample/AbstractSideProofCounterExampleGenerator.java rename to key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/smt/counterexample/AbstractSideProofCounterExampleGenerator.java index 4345c938cb4..1b824ad3067 100644 --- a/key.core.testgen/src/main/java/de/uka/ilkd/key/smt/counterexample/AbstractSideProofCounterExampleGenerator.java +++ b/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/smt/counterexample/AbstractSideProofCounterExampleGenerator.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.smt.counterexample; +package de.uka.ilkd.key.testgen.smt.counterexample; import de.uka.ilkd.key.control.UserInterfaceControl; import de.uka.ilkd.key.logic.Choice; diff --git a/key.core.testgen/src/main/java/de/uka/ilkd/key/smt/testgen/AbstractTestGenerator.java b/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/smt/testgen/AbstractTestGenerator.java similarity index 98% rename from key.core.testgen/src/main/java/de/uka/ilkd/key/smt/testgen/AbstractTestGenerator.java rename to key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/smt/testgen/AbstractTestGenerator.java index 2fbfc7b1ce4..42feebac6e8 100644 --- a/key.core.testgen/src/main/java/de/uka/ilkd/key/smt/testgen/AbstractTestGenerator.java +++ b/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/smt/testgen/AbstractTestGenerator.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.smt.testgen; +package de.uka.ilkd.key.testgen.smt.testgen; import java.io.IOException; import java.util.*; @@ -15,8 +15,6 @@ import de.uka.ilkd.key.logic.Term; import de.uka.ilkd.key.logic.op.UpdateApplication; import de.uka.ilkd.key.macros.ProofMacroFinishedInfo; -import de.uka.ilkd.key.macros.SemanticsBlastingMacro; -import de.uka.ilkd.key.macros.TestGenMacro; import de.uka.ilkd.key.proof.Goal; import de.uka.ilkd.key.proof.Node; import de.uka.ilkd.key.proof.Proof; @@ -33,12 +31,14 @@ import de.uka.ilkd.key.settings.ProofDependentSMTSettings; import de.uka.ilkd.key.settings.ProofIndependentSMTSettings; import de.uka.ilkd.key.settings.ProofIndependentSettings; -import de.uka.ilkd.key.settings.TestGenerationSettings; import de.uka.ilkd.key.smt.*; import de.uka.ilkd.key.smt.model.Model; import de.uka.ilkd.key.smt.solvertypes.SolverType; import de.uka.ilkd.key.smt.solvertypes.SolverTypes; import de.uka.ilkd.key.testgen.TestCaseGenerator; +import de.uka.ilkd.key.testgen.macros.SemanticsBlastingMacro; +import de.uka.ilkd.key.testgen.macros.TestGenMacro; +import de.uka.ilkd.key.testgen.settings.TestGenerationSettings; import de.uka.ilkd.key.util.ProofStarter; import de.uka.ilkd.key.util.SideProofUtil; diff --git a/key.core.testgen/src/main/java/de/uka/ilkd/key/smt/testgen/MemoryTestGenerationLog.java b/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/smt/testgen/MemoryTestGenerationLog.java similarity index 96% rename from key.core.testgen/src/main/java/de/uka/ilkd/key/smt/testgen/MemoryTestGenerationLog.java rename to key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/smt/testgen/MemoryTestGenerationLog.java index 9edcd12b5da..26ec40fb318 100644 --- a/key.core.testgen/src/main/java/de/uka/ilkd/key/smt/testgen/MemoryTestGenerationLog.java +++ b/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/smt/testgen/MemoryTestGenerationLog.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.smt.testgen; +package de.uka.ilkd.key.testgen.smt.testgen; import de.uka.ilkd.key.testgen.TestCaseGenerator; diff --git a/key.core.testgen/src/main/java/de/uka/ilkd/key/smt/testgen/StopRequest.java b/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/smt/testgen/StopRequest.java similarity index 83% rename from key.core.testgen/src/main/java/de/uka/ilkd/key/smt/testgen/StopRequest.java rename to key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/smt/testgen/StopRequest.java index 1907bae9a00..cafa74721ee 100644 --- a/key.core.testgen/src/main/java/de/uka/ilkd/key/smt/testgen/StopRequest.java +++ b/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/smt/testgen/StopRequest.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.smt.testgen; +package de.uka.ilkd.key.testgen.smt.testgen; public interface StopRequest { boolean shouldStop(); diff --git a/key.core.testgen/src/main/java/de/uka/ilkd/key/smt/testgen/TestGenerationLog.java b/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/smt/testgen/TestGenerationLog.java similarity index 88% rename from key.core.testgen/src/main/java/de/uka/ilkd/key/smt/testgen/TestGenerationLog.java rename to key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/smt/testgen/TestGenerationLog.java index 76a3881c74d..589c38e881e 100644 --- a/key.core.testgen/src/main/java/de/uka/ilkd/key/smt/testgen/TestGenerationLog.java +++ b/key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/smt/testgen/TestGenerationLog.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.smt.testgen; +package de.uka.ilkd.key.testgen.smt.testgen; public interface TestGenerationLog { void writeln(String string); diff --git a/key.core.testgen/src/main/java/module-info.java b/key.core.testgen/src/main/java/module-info.java new file mode 100644 index 00000000000..32db629691d --- /dev/null +++ b/key.core.testgen/src/main/java/module-info.java @@ -0,0 +1,11 @@ +import de.uka.ilkd.key.macros.ProofMacro; +import de.uka.ilkd.key.testgen.macros.TestGenMacro; + +/** + * + * @author Alexander Weigl + * @version 1 (04.04.24) + */ +module org.key_project.core.testgen{requires org.key_project.core;requires org.slf4j;requires org.key_project.util;requires org.key_project.ncore;requires org.jspecify;exports de.uka.ilkd.key.testgen.smt.testgen;exports de.uka.ilkd.key.testgen.macros;exports de.uka.ilkd.key.testgen.smt.counterexample;exports de.uka.ilkd.key.testgen.settings; + +provides ProofMacro with TestGenMacro;} diff --git a/key.core.testgen/src/main/resources/services/de.uka.ilkd.key.macros.ProofMacro b/key.core.testgen/src/main/resources/services/de.uka.ilkd.key.macros.ProofMacro index 4480e78c800..0eb775fb6b3 100644 --- a/key.core.testgen/src/main/resources/services/de.uka.ilkd.key.macros.ProofMacro +++ b/key.core.testgen/src/main/resources/services/de.uka.ilkd.key.macros.ProofMacro @@ -2,4 +2,4 @@ # Macros to appear in the context menu # -de.uka.ilkd.key.macros.TestGenMacro +de.uka.ilkd.key.testgen.macros.TestGenMacro diff --git a/key.core.testgen/src/test/java/de/uka/ilkd/key/testcase/smt/ce/TestCE.java b/key.core.testgen/src/test/java/de/uka/ilkd/key/testcase/smt/ce/TestCE.java index 4c6b368f59f..3290c5385d3 100644 --- a/key.core.testgen/src/test/java/de/uka/ilkd/key/testcase/smt/ce/TestCE.java +++ b/key.core.testgen/src/test/java/de/uka/ilkd/key/testcase/smt/ce/TestCE.java @@ -8,7 +8,6 @@ import de.uka.ilkd.key.control.DefaultUserInterfaceControl; import de.uka.ilkd.key.control.KeYEnvironment; import de.uka.ilkd.key.macros.FinishSymbolicExecutionMacro; -import de.uka.ilkd.key.macros.SemanticsBlastingMacro; import de.uka.ilkd.key.macros.TryCloseMacro; import de.uka.ilkd.key.proof.Goal; import de.uka.ilkd.key.proof.Proof; @@ -16,6 +15,7 @@ import de.uka.ilkd.key.smt.solvertypes.SolverType; import de.uka.ilkd.key.smt.solvertypes.SolverTypes; import de.uka.ilkd.key.suite.util.HelperClassForTestgenTests; +import de.uka.ilkd.key.testgen.macros.SemanticsBlastingMacro; import org.junit.jupiter.api.Assertions; import org.junit.jupiter.api.Test; diff --git a/key.core.testgen/src/test/java/de/uka/ilkd/key/testcase/smt/testgen/TestTestgen.java b/key.core.testgen/src/test/java/de/uka/ilkd/key/testcase/smt/testgen/TestTestgen.java index 210a8b84db9..9e6ec93974c 100644 --- a/key.core.testgen/src/test/java/de/uka/ilkd/key/testcase/smt/testgen/TestTestgen.java +++ b/key.core.testgen/src/test/java/de/uka/ilkd/key/testcase/smt/testgen/TestTestgen.java @@ -7,12 +7,12 @@ import de.uka.ilkd.key.control.DefaultUserInterfaceControl; import de.uka.ilkd.key.control.KeYEnvironment; -import de.uka.ilkd.key.macros.TestGenMacro; import de.uka.ilkd.key.proof.Proof; import de.uka.ilkd.key.smt.solvertypes.SolverType; import de.uka.ilkd.key.smt.solvertypes.SolverTypes; import de.uka.ilkd.key.suite.util.HelperClassForTestgenTests; import de.uka.ilkd.key.testcase.smt.ce.TestCommons; +import de.uka.ilkd.key.testgen.macros.TestGenMacro; import org.junit.jupiter.api.BeforeEach; import org.junit.jupiter.api.Test; diff --git a/key.core/src/main/java/de/uka/ilkd/key/axiom_abstraction/predicateabstraction/AbstractionPredicate.java b/key.core/src/main/java/de/uka/ilkd/key/axiom_abstraction/predicateabstraction/AbstractionPredicate.java index 1ad934571b8..12a05465eeb 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/axiom_abstraction/predicateabstraction/AbstractionPredicate.java +++ b/key.core/src/main/java/de/uka/ilkd/key/axiom_abstraction/predicateabstraction/AbstractionPredicate.java @@ -8,7 +8,6 @@ import java.util.function.Function; import java.util.regex.Matcher; import java.util.regex.Pattern; -import javax.naming.NameAlreadyBoundException; import de.uka.ilkd.key.java.Services; import de.uka.ilkd.key.logic.*; diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/ConvertException.java b/key.core/src/main/java/de/uka/ilkd/key/java/ConvertException.java index 9410674d641..10637c1f206 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/ConvertException.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/ConvertException.java @@ -31,19 +31,4 @@ public ConvertException(String errmsg, Throwable cause) { super(errmsg, cause); } - public recoder.parser.ParseException parseException() { - if (getCause() instanceof recoder.parser.ParseException) { - return (recoder.parser.ParseException) getCause(); - } else { - return null; - } - } - - public de.uka.ilkd.key.parser.proofjava.ParseException proofJavaException() { - if (getCause() instanceof de.uka.ilkd.key.parser.proofjava.ParseException) { - return (de.uka.ilkd.key.parser.proofjava.ParseException) getCause(); - } else { - return null; - } - } } diff --git a/key.core/src/main/java/recoder/service/KeYCrossReferenceSourceInfo.java b/key.core/src/main/java/de/uka/ilkd/key/java/KeYCrossReferenceSourceInfo.java similarity index 99% rename from key.core/src/main/java/recoder/service/KeYCrossReferenceSourceInfo.java rename to key.core/src/main/java/de/uka/ilkd/key/java/KeYCrossReferenceSourceInfo.java index 65dcb2554a8..094de25f254 100644 --- a/key.core/src/main/java/recoder/service/KeYCrossReferenceSourceInfo.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/KeYCrossReferenceSourceInfo.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 recoder.service; +package de.uka.ilkd.key.java; import java.lang.reflect.InvocationTargetException; import java.lang.reflect.Method; @@ -64,6 +64,7 @@ import recoder.java.reference.VariableReference; import recoder.java.statement.Case; import recoder.list.generic.ASTList; +import recoder.service.*; public class KeYCrossReferenceSourceInfo extends DefaultCrossReferenceSourceInfo { @@ -221,7 +222,7 @@ public void modelChanged(ChangeHistoryEvent event) { } } - void registerSubtype(ClassType c1, ClassType c2) { + protected void registerSubtype(ClassType c1, ClassType c2) { try { super.registerSubtype(c1, c2); diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/Recoder2KeY.java b/key.core/src/main/java/de/uka/ilkd/key/java/Recoder2KeY.java index 04f81ecef57..b9d6a84ff1e 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/Recoder2KeY.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/Recoder2KeY.java @@ -51,7 +51,6 @@ import recoder.list.generic.ASTList; import recoder.service.ChangeHistory; import recoder.service.CrossReferenceSourceInfo; -import recoder.service.KeYCrossReferenceSourceInfo; import recoder.service.UnresolvedReferenceException; /** diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/recoderext/ClassFileDeclarationManager.java b/key.core/src/main/java/de/uka/ilkd/key/java/recoderext/ClassFileDeclarationManager.java index a583b6631ce..e3a95976293 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/recoderext/ClassFileDeclarationManager.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/recoderext/ClassFileDeclarationManager.java @@ -15,6 +15,7 @@ import java.util.Map; import de.uka.ilkd.key.java.ConvertException; +import de.uka.ilkd.key.java.KeYCrossReferenceSourceInfo; import de.uka.ilkd.key.util.DirectoryFileCollection; import de.uka.ilkd.key.util.FileCollection; import de.uka.ilkd.key.util.FileCollection.Walker; @@ -29,7 +30,6 @@ import recoder.io.DataLocation; import recoder.java.CompilationUnit; import recoder.java.JavaProgramFactory; -import recoder.service.KeYCrossReferenceSourceInfo; /** * This class provides an infrastructure to read in multiple class files and to manufacture diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/recoderext/KeYCrossReferenceServiceConfiguration.java b/key.core/src/main/java/de/uka/ilkd/key/java/recoderext/KeYCrossReferenceServiceConfiguration.java index 372a2ae8edd..06be748e251 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/recoderext/KeYCrossReferenceServiceConfiguration.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/recoderext/KeYCrossReferenceServiceConfiguration.java @@ -3,13 +3,13 @@ * SPDX-License-Identifier: GPL-2.0-only */ package de.uka.ilkd.key.java.recoderext; +import de.uka.ilkd.key.java.KeYCrossReferenceSourceInfo; import de.uka.ilkd.key.java.KeYProgModelInfo; import de.uka.ilkd.key.util.KeYRecoderExcHandler; import recoder.CrossReferenceServiceConfiguration; import recoder.ProgramFactory; import recoder.io.SourceFileRepository; -import recoder.service.KeYCrossReferenceSourceInfo; import recoder.service.NameInfo; import recoder.service.SourceInfo; diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/recoderext/SchemaCrossReferenceSourceInfo.java b/key.core/src/main/java/de/uka/ilkd/key/java/recoderext/SchemaCrossReferenceSourceInfo.java index 896fa816974..8451a02f844 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/recoderext/SchemaCrossReferenceSourceInfo.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/recoderext/SchemaCrossReferenceSourceInfo.java @@ -3,6 +3,8 @@ * SPDX-License-Identifier: GPL-2.0-only */ package de.uka.ilkd.key.java.recoderext; +import de.uka.ilkd.key.java.KeYCrossReferenceSourceInfo; + import recoder.ServiceConfiguration; import recoder.abstraction.PrimitiveType; import recoder.abstraction.Type; @@ -10,7 +12,6 @@ import recoder.java.declaration.VariableSpecification; import recoder.java.reference.TypeReference; import recoder.java.reference.UncollatedReferenceQualifier; -import recoder.service.KeYCrossReferenceSourceInfo; public class SchemaCrossReferenceSourceInfo extends KeYCrossReferenceSourceInfo { diff --git a/key.core/src/main/java/de/uka/ilkd/key/java/visitor/ProgramContextAdder.java b/key.core/src/main/java/de/uka/ilkd/key/java/visitor/ProgramContextAdder.java index 589b1cb9d4d..c7eddcbfef2 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/java/visitor/ProgramContextAdder.java +++ b/key.core/src/main/java/de/uka/ilkd/key/java/visitor/ProgramContextAdder.java @@ -3,8 +3,6 @@ * SPDX-License-Identifier: GPL-2.0-only */ package de.uka.ilkd.key.java.visitor; -import java.rmi.UnexpectedException; - import de.uka.ilkd.key.java.JavaNonTerminalProgramElement; import de.uka.ilkd.key.java.ProgramElement; import de.uka.ilkd.key.java.Statement; @@ -85,7 +83,7 @@ protected JavaNonTerminalProgramElement wrap(JavaNonTerminalProgramElement conte return createExecStatementWrapper((StatementBlock) body, (Exec) context); } else { throw new RuntimeException( - new UnexpectedException("Unexpected block type: " + context.getClass())); + new RuntimeException("Unexpected block type: " + context.getClass())); } } } diff --git a/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/TacletPBuilder.java b/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/TacletPBuilder.java index a80a85e8728..e536f5e3054 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/TacletPBuilder.java +++ b/key.core/src/main/java/de/uka/ilkd/key/nparser/builder/TacletPBuilder.java @@ -33,7 +33,6 @@ import org.key_project.util.collection.ImmutableSet; import org.key_project.util.collection.Pair; -import antlr.RecognitionException; import org.antlr.v4.runtime.ParserRuleContext; import org.antlr.v4.runtime.RuleContext; import org.antlr.v4.runtime.Token; @@ -796,7 +795,7 @@ private void addGoalTemplate(String id, Object rwObj, Sequent addSeq, } else { if (b instanceof NoFindTacletBuilder) { // there is a replacewith without a find. - throwEx(new RecognitionException("")); + throwEx(new RuntimeException("there is a replacewith without a find")); } else if (b instanceof SuccTacletBuilder || b instanceof AntecTacletBuilder) { if (rwObj instanceof Sequent) { gt = new AntecSuccTacletGoalTemplate(addSeq, addRList, (Sequent) rwObj, pvs); diff --git a/key.core/src/main/java/de/uka/ilkd/key/parser/WarningException.java b/key.core/src/main/java/de/uka/ilkd/key/parser/WarningException.java deleted file mode 100644 index 820755ec2fc..00000000000 --- a/key.core/src/main/java/de/uka/ilkd/key/parser/WarningException.java +++ /dev/null @@ -1,27 +0,0 @@ -/* 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.parser; - -public class WarningException extends antlr.ANTLRException { - - /** - * - */ - private static final long serialVersionUID = 3421160418830554998L; - private String errorStr = ""; - - public WarningException(String errorStr) { - this.errorStr = errorStr; - } - - public String getMessage() { - return errorStr; - } - - - public String toString() { - return errorStr; - } - -} diff --git a/key.core/src/main/java/de/uka/ilkd/key/proof/io/AbstractProblemLoader.java b/key.core/src/main/java/de/uka/ilkd/key/proof/io/AbstractProblemLoader.java index 8417e0fbbc3..a5ba764104c 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/proof/io/AbstractProblemLoader.java +++ b/key.core/src/main/java/de/uka/ilkd/key/proof/io/AbstractProblemLoader.java @@ -44,7 +44,6 @@ import org.key_project.util.java.IOUtil; import org.key_project.util.reflection.ClassLoaderUtil; -import org.antlr.runtime.MismatchedTokenException; import org.slf4j.Logger; import org.slf4j.LoggerFactory; @@ -379,33 +378,35 @@ private Throwable unwrap(Throwable e) { */ protected ProblemLoaderException recoverParserErrorMessage(Exception e) { // try to resolve error message - final Throwable c0 = unwrap(e); - if (c0 instanceof org.antlr.runtime.RecognitionException re) { - final org.antlr.runtime.Token occurrence = re.token; // may be null - if (c0 instanceof org.antlr.runtime.MismatchedTokenException) { - if (c0 instanceof org.antlr.runtime.MissingTokenException) { - final org.antlr.runtime.MissingTokenException mte = - (org.antlr.runtime.MissingTokenException) c0; - // TODO: other commonly missed tokens - final String readable = missedErrors.get(mte.expecting); - final String token = readable == null ? "token id " + mte.expecting : readable; - final String msg = "Syntax error: missing " + token - + (occurrence == null ? "" : " at " + occurrence.getText()) + " statement (" - + mte.input.getSourceName() + ":" + mte.line + ")"; - return new ProblemLoaderException(this, msg, mte); - // TODO other ANTLR exceptions - } else { - final org.antlr.runtime.MismatchedTokenException mte = - (MismatchedTokenException) c0; - final String genericMsg = "expected " + mte.expecting + ", but found " + mte.c; - final String readable = - mismatchErrors.get(new Pair<>(mte.expecting, mte.c)); - final String msg = "Syntax error: " + (readable == null ? genericMsg : readable) - + " (" + mte.input.getSourceName() + ":" + mte.line + ")"; - return new ProblemLoaderException(this, msg, mte); - } - } - } + + /* + * weigl These are exception from antlr3, these should not happen anymore + * final Throwable c0 = unwrap(e); + * if (c0 instanceof org.antlr.runtime.RecognitionException re) { + * final org.antlr.runtime.Token occurrence = re.token; // may be null + * if (c0 instanceof org.antlr.runtime.MismatchedTokenException) { + * if (c0 instanceof org.antlr.runtime.MissingTokenException) { + * final org.antlr.runtime.MissingTokenException mte = + * (org.antlr.runtime.MissingTokenException) c0; + * final String readable = missedErrors.get(mte.expecting); + * final String token = readable == null ? "token id " + mte.expecting : readable; + * final String msg = "Syntax error: missing " + token + * + (occurrence == null ? "" : " at " + occurrence.getText()) + " statement (" + * + mte.input.getSourceName() + ":" + mte.line + ")"; + * return new ProblemLoaderException(this, msg, mte); + * } else { + * final org.antlr.runtime.MismatchedTokenException mte = + * (MismatchedTokenException) c0; + * final String genericMsg = "expected " + mte.expecting + ", but found " + mte.c; + * final String readable = + * mismatchErrors.get(new Pair<>(mte.expecting, mte.c)); + * final String msg = "Syntax error: " + (readable == null ? genericMsg : readable) + * + " (" + mte.input.getSourceName() + ":" + mte.line + ")"; + * return new ProblemLoaderException(this, msg, mte); + * } + * } + * } + */ // default return new ProblemLoaderException(this, "Loading proof input failed", e); } diff --git a/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/JmlTermFactory.java b/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/JmlTermFactory.java index c04b662a9e7..faeb8ab3bb5 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/JmlTermFactory.java +++ b/key.core/src/main/java/de/uka/ilkd/key/speclang/njml/JmlTermFactory.java @@ -37,7 +37,7 @@ import org.key_project.util.collection.ImmutableSLList; import org.key_project.util.collection.Pair; -import org.antlr.runtime.Token; +import org.antlr.v4.runtime.Token; import org.jspecify.annotations.NonNull; import org.jspecify.annotations.Nullable; import org.slf4j.Logger; diff --git a/key.core/src/main/java/module-info.java b/key.core/src/main/java/module-info.java new file mode 100644 index 00000000000..59349dc6f7c --- /dev/null +++ b/key.core/src/main/java/module-info.java @@ -0,0 +1,18 @@ +import de.uka.ilkd.key.macros.ProofMacro; +import de.uka.ilkd.key.macros.scripts.ProofScriptCommand; +import de.uka.ilkd.key.proof.init.DefaultProfileResolver; + +/** + * + * @author Alexander Weigl + * @version 1 (31.03.24) + */ +module org.key_project.core{exports de.uka.ilkd.key.java;exports de.uka.ilkd.key.java.abstraction;exports de.uka.ilkd.key.logic.op;exports de.uka.ilkd.key.proof;exports de.uka.ilkd.key.proof.init;exports de.uka.ilkd.key.rule;exports de.uka.ilkd.key.speclang;exports de.uka.ilkd.key.util;exports de.uka.ilkd.key.java.statement;exports de.uka.ilkd.key.java.expression;exports de.uka.ilkd.key.java.reference;exports de.uka.ilkd.key.logic;exports de.uka.ilkd.key.java.expression.operator;exports de.uka.ilkd.key.proof.mgt;exports de.uka.ilkd.key.rule.inst;exports de.uka.ilkd.key.java.recoderext;exports de.uka.ilkd.key.logic.label;exports de.uka.ilkd.key.prover.impl;exports de.uka.ilkd.key.strategy;exports de.uka.ilkd.key.pp;exports de.uka.ilkd.key.speclang.jml.translation;exports de.uka.ilkd.key.speclang.njml;exports de.uka.ilkd.key.java.visitor;exports de.uka.ilkd.key.control;exports de.uka.ilkd.key.ldt;exports de.uka.ilkd.key.rule.tacletbuilder;exports de.uka.ilkd.key.settings;exports de.uka.ilkd.key.rule.merge;exports de.uka.ilkd.key.java.declaration;exports de.uka.ilkd.key.logic.sort;exports de.uka.ilkd.key.proof.io;exports de.uka.ilkd.key.logic.equality;exports de.uka.ilkd.key.rule.label;exports de.uka.ilkd.key.macros;exports de.uka.ilkd.key.macros.scripts;exports de.uka.ilkd.key.prover;exports de.uka.ilkd.key.strategy.feature;exports de.uka.ilkd.key.strategy.definition;exports de.uka.ilkd.key.speclang.translation;exports de.uka.ilkd.key.proof.rulefilter;exports de.uka.ilkd.key.strategy.feature.instantiator;exports de.uka.ilkd.key.strategy.termProjection;exports de.uka.ilkd.key.strategy.termfeature;exports de.uka.ilkd.key.strategy.termgenerator;exports de.uka.ilkd.key.control.instantiation_model;exports de.uka.ilkd.key.parser;exports de.uka.ilkd.key.proof.event;exports de.uka.ilkd.key.proof.join;exports org.key_project.proof;exports de.uka.ilkd.key.util.mergerule;exports de.uka.ilkd.key.proof.reference;exports de.uka.ilkd.key.smt;exports de.uka.ilkd.key.smt.solvertypes;exports de.uka.ilkd.key.taclettranslation.assumptions;exports de.uka.ilkd.key.smt.model;exports de.uka.ilkd.key.rule.merge.procedures;exports de.uka.ilkd.key.axiom_abstraction.predicateabstraction;exports de.uka.ilkd.key.control.event;exports de.uka.ilkd.key.informationflow.macros;exports de.uka.ilkd.key.proof.io.consistency;exports de.uka.ilkd.key.taclettranslation.lemma;exports de.uka.ilkd.key.nparser;exports de.uka.ilkd.key.proof.delayedcut;exports de.uka.ilkd.key.speclang.jml;exports de.uka.ilkd.key.smt.newsmt2;exports de.uka.ilkd.key.util.pp;exports de.uka.ilkd.key.axiom_abstraction;exports de.uka.ilkd.key.proof.replay;exports de.uka.ilkd.key.smt.communication;exports de.uka.ilkd.key.proof.io.intermediate;exports de.uka.ilkd.key.proof.proofevent;exports de.uka.ilkd.key.util.parsing;exports de.uka.ilkd.key.smt.lang;requires org.slf4j;requires key.recoder;requires org.key_project.ncore;requires org.key_project.util;requires java.desktop;requires org.jspecify;requires org.antlr.antlr4.runtime;requires java.scripting; + +provides ProofMacro with de.uka.ilkd.key.informationflow.macros.FullInformationFlowAutoPilotMacro,de.uka.ilkd.key.informationflow.macros.AuxiliaryComputationAutoPilotMacro,de.uka.ilkd.key.informationflow.macros.StartAuxiliaryComputationMacro,de.uka.ilkd.key.informationflow.macros.FinishAuxiliaryComputationMacro,de.uka.ilkd.key.macros.FullAutoPilotProofMacro,de.uka.ilkd.key.macros.AutoPilotPrepareProofMacro,de.uka.ilkd.key.macros.SMTPreparationMacro,de.uka.ilkd.key.informationflow.macros.StateExpansionAndInfFlowContractApplicationMacro,de.uka.ilkd.key.informationflow.macros.SelfcompositionStateExpansionMacro,de.uka.ilkd.key.informationflow.macros.FullUseInformationFlowContractMacro,de.uka.ilkd.key.macros.PropositionalExpansionMacro,de.uka.ilkd.key.macros.FullPropositionalExpansionMacro,de.uka.ilkd.key.macros.TryCloseMacro,de.uka.ilkd.key.macros.FinishSymbolicExecutionMacro,de.uka.ilkd.key.macros.AutoMacro,de.uka.ilkd.key.macros.HeapSimplificationMacro,de.uka.ilkd.key.macros.IntegerSimplificationMacro,de.uka.ilkd.key.macros.OneStepProofMacro,de.uka.ilkd.key.macros.WellDefinednessMacro,de.uka.ilkd.key.macros.UpdateSimplificationMacro,de.uka.ilkd.key.macros.TranscendentalFloatSMTMacro; + +provides ProofScriptCommand with de.uka.ilkd.key.macros.scripts.EchoCommand,de.uka.ilkd.key.macros.scripts.MacroCommand,de.uka.ilkd.key.macros.scripts.FocusCommand,de.uka.ilkd.key.macros.scripts.AutoCommand,de.uka.ilkd.key.macros.scripts.CutCommand,de.uka.ilkd.key.macros.scripts.SetCommand,de.uka.ilkd.key.macros.scripts.SetEchoCommand,de.uka.ilkd.key.macros.scripts.SetFailOnClosedCommand,de.uka.ilkd.key.macros.scripts.SMTCommand,de.uka.ilkd.key.macros.scripts.RuleCommand,de.uka.ilkd.key.macros.scripts.ActivateCommand,de.uka.ilkd.key.macros.scripts.LeaveCommand,de.uka.ilkd.key.macros.scripts.TryCloseCommand,de.uka.ilkd.key.macros.scripts.ExitCommand,de.uka.ilkd.key.macros.scripts.InstantiateCommand,de.uka.ilkd.key.macros.scripts.SelectCommand,de.uka.ilkd.key.macros.scripts.ScriptCommand,de.uka.ilkd.key.macros.scripts.LetCommand,de.uka.ilkd.key.macros.scripts.SaveInstCommand,de.uka.ilkd.key.macros.scripts.SaveNewNameCommand,de.uka.ilkd.key.macros.scripts.SchemaVarCommand,de.uka.ilkd.key.macros.scripts.JavascriptCommand,de.uka.ilkd.key.macros.scripts.SkipCommand,de.uka.ilkd.key.macros.scripts.AxiomCommand,de.uka.ilkd.key.macros.scripts.AssumeCommand,de.uka.ilkd.key.macros.scripts.AssertCommand,de.uka.ilkd.key.macros.scripts.RewriteCommand,de.uka.ilkd.key.macros.scripts.AllCommand,de.uka.ilkd.key.macros.scripts.HideCommand,de.uka.ilkd.key.macros.scripts.UnhideCommand; + +provides DefaultProfileResolver with de.uka.ilkd.key.proof.init.JavaProfileDefaultProfileResolver,de.uka.ilkd.key.proof.init.JavaProfileWithPermissionsDefaultProfileResolver; + +} diff --git a/key.core/src/main/resources/META-INF/services/de.uka.ilkd.key.proof.init.DefaultProfileResolver b/key.core/src/main/resources/META-INF/services/de.uka.ilkd.key.proof.init.DefaultProfileResolver index 24b975ab0ea..3270b9b1557 100644 --- a/key.core/src/main/resources/META-INF/services/de.uka.ilkd.key.proof.init.DefaultProfileResolver +++ b/key.core/src/main/resources/META-INF/services/de.uka.ilkd.key.proof.init.DefaultProfileResolver @@ -4,4 +4,4 @@ de.uka.ilkd.key.proof.init.JavaProfileDefaultProfileResolver de.uka.ilkd.key.proof.init.JavaProfileWithPermissionsDefaultProfileResolver -de.tud.cs.se.ds.specstr.profile.StrengthAnalysisSEProfileDefaultProfileResolver + diff --git a/key.core/src/test/java/de/uka/ilkd/key/smt/newsmt2/TestSMTMod.java b/key.core/src/test/java/de/uka/ilkd/key/smt/newsmt2/TestSMTMod.java index 664b631aca8..8c84069e5e4 100644 --- a/key.core/src/test/java/de/uka/ilkd/key/smt/newsmt2/TestSMTMod.java +++ b/key.core/src/test/java/de/uka/ilkd/key/smt/newsmt2/TestSMTMod.java @@ -20,7 +20,7 @@ import org.key_project.util.helper.FindResources; -import org.junit.Test; +import org.junit.jupiter.api.Test; import org.slf4j.Logger; import org.slf4j.LoggerFactory; diff --git a/key.removegenerics/src/main/java/module-info.java b/key.removegenerics/src/main/java/module-info.java new file mode 100644 index 00000000000..27f1eb8cef0 --- /dev/null +++ b/key.removegenerics/src/main/java/module-info.java @@ -0,0 +1,9 @@ +/** + * + * @author Alexander Weigl + * @version 1 (31.03.24) + */ +module org.key_project.removegenerics { + requires key.recoder; + requires org.slf4j; +} \ No newline at end of file diff --git a/key.ui/build.gradle b/key.ui/build.gradle index 93edbc44890..fbc953cf4d1 100644 --- a/key.ui/build.gradle +++ b/key.ui/build.gradle @@ -10,6 +10,7 @@ plugins { id 'com.github.johnrengelman.shadow' version "8.1.1" } + description "User interface for the deductive verification of Java programs" dependencies { @@ -25,8 +26,8 @@ dependencies { //logging implementation used by the slf4j implementation 'ch.qos.logback:logback-classic:1.5.6' - api 'org.key-project:docking-frames-common:1.1.3p1' - api 'org.key-project:docking-frames-core:1.1.3p1' + api 'org.key-project:docking-frames-common:1.1.3p4-SNAPSHOT' + api 'org.key-project:docking-frames-core:1.1.3p4-SNAPSHOT' runtimeOnly project(":keyext.ui.testgen") runtimeOnly project(":keyext.caching") diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/ApplyTacletDialog.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/ApplyTacletDialog.java index 24dbf6c9f7e..db41dcf7d26 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/ApplyTacletDialog.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/ApplyTacletDialog.java @@ -13,7 +13,6 @@ import javax.swing.border.TitledBorder; import de.uka.ilkd.key.control.instantiation_model.TacletInstantiationModel; -import de.uka.ilkd.key.core.KeYMediator; import de.uka.ilkd.key.gui.utilities.GuiUtilities; import de.uka.ilkd.key.logic.op.IProgramVariable; import de.uka.ilkd.key.pp.NotationInfo; @@ -21,6 +20,7 @@ import de.uka.ilkd.key.rule.Taclet; import de.uka.ilkd.key.rule.inst.SVInstantiations; import de.uka.ilkd.key.settings.ProofIndependentSettings; +import de.uka.ilkd.key.ui.core.KeYMediator; import org.slf4j.Logger; import org.slf4j.LoggerFactory; diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/GoalList.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/GoalList.java index 36f80c07666..7fc3f1e7617 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/GoalList.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/GoalList.java @@ -20,9 +20,6 @@ import javax.swing.event.ListSelectionListener; import de.uka.ilkd.key.control.AutoModeListener; -import de.uka.ilkd.key.core.KeYMediator; -import de.uka.ilkd.key.core.KeYSelectionEvent; -import de.uka.ilkd.key.core.KeYSelectionListener; import de.uka.ilkd.key.gui.configuration.Config; import de.uka.ilkd.key.gui.extension.api.KeYGuiExtension; import de.uka.ilkd.key.gui.extension.api.TabPanel; @@ -37,6 +34,9 @@ import de.uka.ilkd.key.pp.SequentViewLogicPrinter; import de.uka.ilkd.key.pp.VisibleTermLabels; import de.uka.ilkd.key.proof.*; +import de.uka.ilkd.key.ui.core.KeYMediator; +import de.uka.ilkd.key.ui.core.KeYSelectionEvent; +import de.uka.ilkd.key.ui.core.KeYSelectionListener; import org.key_project.logic.Name; import org.key_project.util.collection.ImmutableList; diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/InfoTreeModel.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/InfoTreeModel.java index e5c2656b37e..27a39578207 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/InfoTreeModel.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/InfoTreeModel.java @@ -12,8 +12,8 @@ import de.uka.ilkd.key.rule.NoPosTacletApp; import de.uka.ilkd.key.rule.OneStepSimplifier; import de.uka.ilkd.key.rule.Taclet; +import de.uka.ilkd.key.ui.util.XMLResources; import de.uka.ilkd.key.util.MiscTools; -import de.uka.ilkd.key.util.XMLResources; import org.key_project.logic.Name; diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/InfoView.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/InfoView.java index f1ea7dac7b5..68acabf166c 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/InfoView.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/InfoView.java @@ -11,10 +11,6 @@ import javax.swing.event.TreeSelectionEvent; import javax.swing.event.TreeSelectionListener; -import de.uka.ilkd.key.core.KeYMediator; -import de.uka.ilkd.key.core.KeYSelectionEvent; -import de.uka.ilkd.key.core.KeYSelectionListener; -import de.uka.ilkd.key.core.KeYSelectionModel; import de.uka.ilkd.key.gui.extension.api.DefaultContextMenuKind; import de.uka.ilkd.key.gui.extension.api.KeYGuiExtension; import de.uka.ilkd.key.gui.extension.api.TabPanel; @@ -25,8 +21,12 @@ import de.uka.ilkd.key.proof.event.ProofDisposedEvent; import de.uka.ilkd.key.proof.event.ProofDisposedListener; import de.uka.ilkd.key.rule.Rule; -import de.uka.ilkd.key.util.ThreadUtilities; -import de.uka.ilkd.key.util.XMLResources; +import de.uka.ilkd.key.ui.core.KeYMediator; +import de.uka.ilkd.key.ui.core.KeYSelectionEvent; +import de.uka.ilkd.key.ui.core.KeYSelectionListener; +import de.uka.ilkd.key.ui.core.KeYSelectionModel; +import de.uka.ilkd.key.ui.util.ThreadUtilities; +import de.uka.ilkd.key.ui.util.XMLResources; /** * Class for info contents displayed in {@link MainWindow}. diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/IssueDialog.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/IssueDialog.java index 6e36b867321..0ac73ab6e7c 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/IssueDialog.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/IssueDialog.java @@ -34,12 +34,12 @@ import de.uka.ilkd.key.pp.LogicPrinter; import de.uka.ilkd.key.speclang.PositionedString; import de.uka.ilkd.key.speclang.SLEnvInput; +import de.uka.ilkd.key.ui.util.SwingUtil; import de.uka.ilkd.key.util.ExceptionTools; import org.key_project.util.collection.ImmutableSet; import org.key_project.util.java.IOUtil; import org.key_project.util.java.StringUtil; -import org.key_project.util.java.SwingUtil; import org.antlr.v4.runtime.InputMismatchException; import org.antlr.v4.runtime.NoViableAltException; diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/KeYFileChooser.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/KeYFileChooser.java index 97c247a1bb6..2bd76afcf53 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/KeYFileChooser.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/KeYFileChooser.java @@ -11,7 +11,7 @@ import javax.swing.filechooser.FileFilter; import javax.swing.filechooser.FileNameExtensionFilter; -import de.uka.ilkd.key.core.Main; +import de.uka.ilkd.key.ui.core.Main; import org.key_project.util.java.IOUtil; diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/KeyboardTacletExtension.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/KeyboardTacletExtension.java index 1e5dc67fef0..74d2a086860 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/KeyboardTacletExtension.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/KeyboardTacletExtension.java @@ -14,9 +14,6 @@ import javax.swing.event.DocumentEvent; import javax.swing.event.DocumentListener; -import de.uka.ilkd.key.core.KeYMediator; -import de.uka.ilkd.key.core.KeYSelectionEvent; -import de.uka.ilkd.key.core.KeYSelectionListener; import de.uka.ilkd.key.gui.actions.KeyAction; import de.uka.ilkd.key.gui.docking.DockingHelper; import de.uka.ilkd.key.gui.extension.api.KeYGuiExtension; @@ -33,12 +30,15 @@ import de.uka.ilkd.key.rule.Taclet; import de.uka.ilkd.key.rule.TacletApp; import de.uka.ilkd.key.ui.MediatorProofControl; +import de.uka.ilkd.key.ui.core.KeYMediator; +import de.uka.ilkd.key.ui.core.KeYSelectionEvent; +import de.uka.ilkd.key.ui.core.KeYSelectionListener; +import org.key_project.dockingframes.common.common.action.CAction; +import org.key_project.dockingframes.common.common.action.CDropDownButton; import org.key_project.util.collection.ImmutableList; import org.key_project.util.collection.ImmutableSet; -import bibliothek.gui.dock.common.action.CAction; -import bibliothek.gui.dock.common.action.CDropDownButton; import net.miginfocom.layout.CC; import net.miginfocom.swing.MigLayout; import org.jspecify.annotations.NonNull; diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/LogView.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/LogView.java index c9a4685bbb1..0cb8d967462 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/LogView.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/LogView.java @@ -18,11 +18,11 @@ import javax.swing.text.SimpleAttributeSet; import javax.swing.text.StyleConstants; -import de.uka.ilkd.key.core.Log; import de.uka.ilkd.key.gui.actions.KeyAction; import de.uka.ilkd.key.gui.extension.api.KeYGuiExtension; import de.uka.ilkd.key.gui.fonticons.FontAwesomeSolid; import de.uka.ilkd.key.gui.fonticons.IconFontProvider; +import de.uka.ilkd.key.ui.core.Log; import net.miginfocom.layout.CC; import net.miginfocom.swing.MigLayout; diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/MainWindow.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/MainWindow.java index e25b78cf31f..7df299437e7 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/MainWindow.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/MainWindow.java @@ -28,9 +28,6 @@ import de.uka.ilkd.key.control.AutoModeListener; import de.uka.ilkd.key.control.TermLabelVisibilityManager; -import de.uka.ilkd.key.core.KeYMediator; -import de.uka.ilkd.key.core.KeYSelectionEvent; -import de.uka.ilkd.key.core.KeYSelectionListener; import de.uka.ilkd.key.gui.actions.*; import de.uka.ilkd.key.gui.actions.useractions.ProofLoadUserAction; import de.uka.ilkd.key.gui.configuration.Config; @@ -66,15 +63,20 @@ import de.uka.ilkd.key.smt.SolverTypeCollection; import de.uka.ilkd.key.smt.solvertypes.SolverType; import de.uka.ilkd.key.ui.AbstractMediatorUserInterfaceControl; +import de.uka.ilkd.key.ui.core.KeYMediator; +import de.uka.ilkd.key.ui.core.KeYSelectionEvent; +import de.uka.ilkd.key.ui.core.KeYSelectionListener; +import de.uka.ilkd.key.ui.util.PreferenceSaver; +import de.uka.ilkd.key.ui.util.ThreadUtilities; import de.uka.ilkd.key.util.*; +import org.key_project.dockingframes.common.common.CControl; +import org.key_project.dockingframes.common.common.SingleCDockable; +import org.key_project.dockingframes.common.common.intern.CDockable; +import org.key_project.dockingframes.core.gui.dock.StackDockStation; +import org.key_project.dockingframes.core.gui.dock.station.stack.tab.layouting.TabPlacement; import org.key_project.logic.Name; -import bibliothek.gui.dock.StackDockStation; -import bibliothek.gui.dock.common.CControl; -import bibliothek.gui.dock.common.SingleCDockable; -import bibliothek.gui.dock.common.intern.CDockable; -import bibliothek.gui.dock.station.stack.tab.layouting.TabPlacement; import org.jspecify.annotations.NonNull; import org.slf4j.Logger; import org.slf4j.LoggerFactory; diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/MainWindowTabbedPane.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/MainWindowTabbedPane.java index cb991480cf9..390edffe002 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/MainWindowTabbedPane.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/MainWindowTabbedPane.java @@ -8,11 +8,11 @@ import java.util.stream.Stream; import javax.swing.*; -import de.uka.ilkd.key.core.KeYMediator; import de.uka.ilkd.key.gui.actions.AutoModeAction; import de.uka.ilkd.key.gui.extension.api.TabPanel; import de.uka.ilkd.key.gui.extension.impl.KeYGuiExtensionFacade; import de.uka.ilkd.key.gui.prooftree.ProofTreeView; +import de.uka.ilkd.key.ui.core.KeYMediator; /** * {@link JTabbedPane} displayed in {@link MainWindow}, to the left of diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/MaxRuleAppSlider.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/MaxRuleAppSlider.java index 3ca46aab2f7..cd9bff5c8b6 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/MaxRuleAppSlider.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/MaxRuleAppSlider.java @@ -7,7 +7,7 @@ import java.util.LinkedList; import javax.swing.*; -import de.uka.ilkd.key.core.KeYMediator; +import de.uka.ilkd.key.ui.core.KeYMediator; public class MaxRuleAppSlider extends JSlider { /** diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/ProofMacroMenu.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/ProofMacroMenu.java index 9a41bca4fd1..7d69c668957 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/ProofMacroMenu.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/ProofMacroMenu.java @@ -6,7 +6,6 @@ import java.util.*; import javax.swing.*; -import de.uka.ilkd.key.core.KeYMediator; import de.uka.ilkd.key.gui.actions.ProofScriptFromFileAction; import de.uka.ilkd.key.gui.actions.ProofScriptInputAction; import de.uka.ilkd.key.gui.actions.useractions.ProofMacroUserAction; @@ -15,6 +14,7 @@ import de.uka.ilkd.key.macros.ProofMacro; import de.uka.ilkd.key.proof.Node; import de.uka.ilkd.key.settings.FeatureSettings; +import de.uka.ilkd.key.ui.core.KeYMediator; import org.key_project.util.reflection.ClassLoaderUtil; diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/ProofMacroWorker.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/ProofMacroWorker.java index 6f634c192f1..8a9f7d62e81 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/ProofMacroWorker.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/ProofMacroWorker.java @@ -8,8 +8,6 @@ import javax.swing.*; import de.uka.ilkd.key.control.InteractionListener; -import de.uka.ilkd.key.core.InterruptListener; -import de.uka.ilkd.key.core.KeYMediator; import de.uka.ilkd.key.logic.PosInOccurrence; import de.uka.ilkd.key.macros.ProofMacro; import de.uka.ilkd.key.macros.ProofMacroFinishedInfo; @@ -20,6 +18,8 @@ import de.uka.ilkd.key.prover.ProverTaskListener; import de.uka.ilkd.key.prover.TaskStartedInfo; import de.uka.ilkd.key.prover.impl.DefaultTaskStartedInfo; +import de.uka.ilkd.key.ui.core.InterruptListener; +import de.uka.ilkd.key.ui.core.KeYMediator; import org.slf4j.Logger; import org.slf4j.LoggerFactory; diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/ProofManagementDialog.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/ProofManagementDialog.java index 54a0ddc0f86..fb320284b69 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/ProofManagementDialog.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/ProofManagementDialog.java @@ -17,7 +17,6 @@ import javax.swing.*; import javax.swing.border.TitledBorder; -import de.uka.ilkd.key.core.KeYMediator; import de.uka.ilkd.key.gui.fonticons.IconFactory; import de.uka.ilkd.key.gui.utilities.GuiUtilities; import de.uka.ilkd.key.java.Services; @@ -38,6 +37,7 @@ import de.uka.ilkd.key.proof.mgt.SpecificationRepository; import de.uka.ilkd.key.speclang.Contract; import de.uka.ilkd.key.ui.AbstractMediatorUserInterfaceControl; +import de.uka.ilkd.key.ui.core.KeYMediator; import org.key_project.logic.Name; import org.key_project.util.collection.DefaultImmutableSet; diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/ProofScriptWorker.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/ProofScriptWorker.java index 6c94d762e00..81af7bb3279 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/ProofScriptWorker.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/ProofScriptWorker.java @@ -16,15 +16,15 @@ import javax.swing.text.BadLocationException; import javax.swing.text.Document; -import de.uka.ilkd.key.core.InterruptListener; -import de.uka.ilkd.key.core.KeYMediator; -import de.uka.ilkd.key.core.KeYSelectionModel; import de.uka.ilkd.key.java.Position; import de.uka.ilkd.key.macros.scripts.ProofScriptEngine; import de.uka.ilkd.key.macros.scripts.ScriptException; import de.uka.ilkd.key.parser.Location; import de.uka.ilkd.key.proof.Goal; import de.uka.ilkd.key.proof.Proof; +import de.uka.ilkd.key.ui.core.InterruptListener; +import de.uka.ilkd.key.ui.core.KeYMediator; +import de.uka.ilkd.key.ui.core.KeYSelectionModel; import org.slf4j.Logger; import org.slf4j.LoggerFactory; diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/RecentFileMenu.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/RecentFileMenu.java index 98d47b13694..629ddb6b2a6 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/RecentFileMenu.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/RecentFileMenu.java @@ -12,10 +12,10 @@ import java.util.stream.Collectors; import javax.swing.*; -import de.uka.ilkd.key.core.KeYMediator; import de.uka.ilkd.key.gui.fonticons.IconFactory; import de.uka.ilkd.key.settings.Configuration; import de.uka.ilkd.key.settings.PathConfig; +import de.uka.ilkd.key.ui.core.KeYMediator; import org.slf4j.Logger; import org.slf4j.LoggerFactory; diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/SelectionHistory.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/SelectionHistory.java index f95e50d94d5..9351b4f88ea 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/SelectionHistory.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/SelectionHistory.java @@ -11,13 +11,13 @@ import java.util.HashSet; import java.util.Set; -import de.uka.ilkd.key.core.KeYMediator; -import de.uka.ilkd.key.core.KeYSelectionEvent; -import de.uka.ilkd.key.core.KeYSelectionListener; import de.uka.ilkd.key.proof.Node; import de.uka.ilkd.key.proof.Proof; import de.uka.ilkd.key.proof.event.ProofDisposedEvent; import de.uka.ilkd.key.proof.event.ProofDisposedListener; +import de.uka.ilkd.key.ui.core.KeYMediator; +import de.uka.ilkd.key.ui.core.KeYSelectionEvent; +import de.uka.ilkd.key.ui.core.KeYSelectionListener; /** * Traces the proof nodes selected by the user. Allows navigating forwards and backwards to diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/StrategySelectionView.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/StrategySelectionView.java index ca11ccaa58e..8d70df6266e 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/StrategySelectionView.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/StrategySelectionView.java @@ -9,9 +9,6 @@ import java.util.Map.Entry; import javax.swing.*; -import de.uka.ilkd.key.core.KeYMediator; -import de.uka.ilkd.key.core.KeYSelectionEvent; -import de.uka.ilkd.key.core.KeYSelectionListener; import de.uka.ilkd.key.gui.extension.api.KeYGuiExtension; import de.uka.ilkd.key.gui.extension.api.TabPanel; import de.uka.ilkd.key.gui.extension.impl.KeYGuiExtensionFacade; @@ -25,6 +22,9 @@ import de.uka.ilkd.key.strategy.StrategyFactory; import de.uka.ilkd.key.strategy.StrategyProperties; import de.uka.ilkd.key.strategy.definition.*; +import de.uka.ilkd.key.ui.core.KeYMediator; +import de.uka.ilkd.key.ui.core.KeYSelectionEvent; +import de.uka.ilkd.key.ui.core.KeYSelectionListener; import de.uka.ilkd.key.util.Triple; import org.slf4j.Logger; diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/TacletMatchCompletionDialog.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/TacletMatchCompletionDialog.java index abc51d2775a..f1093abcdfc 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/TacletMatchCompletionDialog.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/TacletMatchCompletionDialog.java @@ -21,7 +21,6 @@ import de.uka.ilkd.key.control.InstantiationFileHandler; import de.uka.ilkd.key.control.instantiation_model.TacletInstantiationModel; -import de.uka.ilkd.key.core.KeYMediator; import de.uka.ilkd.key.gui.nodeviews.PosInSequentTransferable; import de.uka.ilkd.key.gui.utilities.BracketMatchingTextArea; import de.uka.ilkd.key.java.Services; @@ -39,6 +38,7 @@ import de.uka.ilkd.key.proof.ModelEvent; import de.uka.ilkd.key.proof.SVInstantiationExceptionWithPosition; import de.uka.ilkd.key.rule.TacletApp; +import de.uka.ilkd.key.ui.core.KeYMediator; import org.slf4j.Logger; import org.slf4j.LoggerFactory; diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/TaskTree.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/TaskTree.java index bc7f539dfe3..45d31bce3b8 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/TaskTree.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/TaskTree.java @@ -18,21 +18,21 @@ import javax.swing.tree.TreePath; import de.uka.ilkd.key.control.AutoModeListener; -import de.uka.ilkd.key.core.KeYMediator; -import de.uka.ilkd.key.core.KeYSelectionEvent; -import de.uka.ilkd.key.core.KeYSelectionListener; import de.uka.ilkd.key.gui.configuration.Config; import de.uka.ilkd.key.gui.extension.api.DefaultContextMenuKind; import de.uka.ilkd.key.gui.extension.impl.KeYGuiExtensionFacade; import de.uka.ilkd.key.gui.fonticons.IconFactory; import de.uka.ilkd.key.gui.notification.events.AbandonTaskEvent; import de.uka.ilkd.key.proof.*; -import de.uka.ilkd.key.proof.mgt.BasicTask; -import de.uka.ilkd.key.proof.mgt.EnvNode; import de.uka.ilkd.key.proof.mgt.ProofEnvironment; import de.uka.ilkd.key.proof.mgt.ProofStatus; -import de.uka.ilkd.key.proof.mgt.TaskTreeModel; -import de.uka.ilkd.key.proof.mgt.TaskTreeNode; +import de.uka.ilkd.key.ui.core.KeYMediator; +import de.uka.ilkd.key.ui.core.KeYSelectionEvent; +import de.uka.ilkd.key.ui.core.KeYSelectionListener; +import de.uka.ilkd.key.ui.proof.mgt.BasicTask; +import de.uka.ilkd.key.ui.proof.mgt.EnvNode; +import de.uka.ilkd.key.ui.proof.mgt.TaskTreeModel; +import de.uka.ilkd.key.ui.proof.mgt.TaskTreeNode; import org.slf4j.Logger; import org.slf4j.LoggerFactory; diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/WindowUserInterfaceControl.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/WindowUserInterfaceControl.java index f9066745de7..85df7cb1418 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/WindowUserInterfaceControl.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/WindowUserInterfaceControl.java @@ -17,8 +17,6 @@ import de.uka.ilkd.key.control.TermLabelVisibilityManager; import de.uka.ilkd.key.control.UserInterfaceControl; import de.uka.ilkd.key.control.instantiation_model.TacletInstantiationModel; -import de.uka.ilkd.key.core.KeYMediator; -import de.uka.ilkd.key.gui.actions.ExitMainAction; import de.uka.ilkd.key.gui.mergerule.MergeRuleCompletion; import de.uka.ilkd.key.gui.notification.events.GeneralFailureEvent; import de.uka.ilkd.key.gui.notification.events.NotificationEvent; @@ -44,18 +42,20 @@ import de.uka.ilkd.key.strategy.StrategyProperties; import de.uka.ilkd.key.ui.AbstractMediatorUserInterfaceControl; import de.uka.ilkd.key.ui.MediatorProofControl; +import de.uka.ilkd.key.ui.core.KeYMediator; +import de.uka.ilkd.key.ui.proof.io.ProblemLoader; +import de.uka.ilkd.key.ui.util.SwingUtil; +import de.uka.ilkd.key.ui.util.ThreadUtilities; import de.uka.ilkd.key.util.KeYConstants; import de.uka.ilkd.key.util.MiscTools; -import de.uka.ilkd.key.util.ThreadUtilities; import org.key_project.util.collection.ImmutableSet; import org.key_project.util.collection.Pair; -import org.key_project.util.java.SwingUtil; import org.antlr.v4.runtime.misc.ParseCancellationException; import org.slf4j.Logger; import org.slf4j.LoggerFactory; -import sun.misc.Signal; +// import sun.misc.Signal; /** * Implementation of {@link UserInterfaceControl} which controls the {@link MainWindow} with the @@ -80,15 +80,18 @@ public WindowUserInterfaceControl(MainWindow mainWindow) { completions.add(new BlockContractExternalCompletion(mainWindow)); completions.add(MergeRuleCompletion.INSTANCE); try { - Signal.handle(new Signal("INT"), sig -> { - if (getMediator().isInAutoMode()) { - LOGGER.warn("Caught SIGINT, stopping automode..."); - getMediator().getUI().getProofControl().stopAutoMode(); - } else { - LOGGER.warn("Caught SIGINT, exiting..."); - new ExitMainAction(mainWindow).exitMainWithoutInteraction(); - } - }); + /* + * requires module dep to jdk.unsupported. + * Signal.handle(new Signal("INT"), sig -> { + * if (getMediator().isInAutoMode()) { + * LOGGER.warn("Caught SIGINT, stopping automode..."); + * getMediator().getUI().getProofControl().stopAutoMode(); + * } else { + * LOGGER.warn("Caught SIGINT, exiting..."); + * new ExitMainAction(mainWindow).exitMainWithoutInteraction(); + * } + * }); + */ } catch (Exception e) { // the above is optional functionality and may not work on every OS } diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/AutoModeAction.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/AutoModeAction.java index 5da01cc8080..93a4a96515f 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/AutoModeAction.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/AutoModeAction.java @@ -11,9 +11,6 @@ import javax.swing.KeyStroke; import de.uka.ilkd.key.control.AutoModeListener; -import de.uka.ilkd.key.core.KeYMediator; -import de.uka.ilkd.key.core.KeYSelectionEvent; -import de.uka.ilkd.key.core.KeYSelectionListener; import de.uka.ilkd.key.gui.MainWindow; import de.uka.ilkd.key.gui.actions.useractions.AutoModeUserAction; import de.uka.ilkd.key.gui.fonticons.IconFactory; @@ -23,6 +20,9 @@ import de.uka.ilkd.key.proof.ProofTreeAdapter; import de.uka.ilkd.key.proof.ProofTreeEvent; import de.uka.ilkd.key.proof.ProofTreeListener; +import de.uka.ilkd.key.ui.core.KeYMediator; +import de.uka.ilkd.key.ui.core.KeYSelectionEvent; +import de.uka.ilkd.key.ui.core.KeYSelectionListener; import org.key_project.util.collection.ImmutableList; diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/EditMostRecentFileAction.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/EditMostRecentFileAction.java index 42c4d2672b2..cf998f2f1bf 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/EditMostRecentFileAction.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/EditMostRecentFileAction.java @@ -8,10 +8,10 @@ import java.io.File; import java.io.IOException; -import de.uka.ilkd.key.core.KeYSelectionEvent; -import de.uka.ilkd.key.core.KeYSelectionListener; import de.uka.ilkd.key.gui.MainWindow; import de.uka.ilkd.key.gui.fonticons.IconFactory; +import de.uka.ilkd.key.ui.core.KeYSelectionEvent; +import de.uka.ilkd.key.ui.core.KeYSelectionListener; import org.slf4j.Logger; import org.slf4j.LoggerFactory; diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/GoalBackAction.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/GoalBackAction.java index 1988b642008..456ef87fd09 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/GoalBackAction.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/GoalBackAction.java @@ -6,8 +6,6 @@ import java.awt.event.ActionEvent; import de.uka.ilkd.key.control.AutoModeListener; -import de.uka.ilkd.key.core.KeYSelectionEvent; -import de.uka.ilkd.key.core.KeYSelectionListener; import de.uka.ilkd.key.gui.MainWindow; import de.uka.ilkd.key.gui.fonticons.IconFactory; import de.uka.ilkd.key.proof.Goal; @@ -16,6 +14,8 @@ import de.uka.ilkd.key.proof.ProofEvent; import de.uka.ilkd.key.rule.RuleApp; import de.uka.ilkd.key.settings.GeneralSettings; +import de.uka.ilkd.key.ui.core.KeYSelectionEvent; +import de.uka.ilkd.key.ui.core.KeYSelectionListener; import org.key_project.util.collection.ImmutableList; diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/HeatmapSettingsAction.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/HeatmapSettingsAction.java index dd7bd3e788a..16b6594be64 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/HeatmapSettingsAction.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/HeatmapSettingsAction.java @@ -5,12 +5,12 @@ import java.awt.event.ActionEvent; -import de.uka.ilkd.key.core.KeYSelectionEvent; -import de.uka.ilkd.key.core.KeYSelectionListener; import de.uka.ilkd.key.gui.HeatmapOptionsDialog; import de.uka.ilkd.key.gui.MainWindow; import de.uka.ilkd.key.gui.fonticons.IconFactory; import de.uka.ilkd.key.proof.Proof; +import de.uka.ilkd.key.ui.core.KeYSelectionEvent; +import de.uka.ilkd.key.ui.core.KeYSelectionListener; /** * Action for invoking the heatmap options dialog. diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/HeatmapToggleAction.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/HeatmapToggleAction.java index b7df2f6c0b5..5a8364faf40 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/HeatmapToggleAction.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/HeatmapToggleAction.java @@ -7,13 +7,13 @@ import java.beans.PropertyChangeListener; import javax.swing.*; -import de.uka.ilkd.key.core.KeYSelectionEvent; -import de.uka.ilkd.key.core.KeYSelectionListener; import de.uka.ilkd.key.gui.MainWindow; import de.uka.ilkd.key.gui.fonticons.IconFactory; import de.uka.ilkd.key.proof.Proof; import de.uka.ilkd.key.settings.ProofIndependentSettings; import de.uka.ilkd.key.settings.ViewSettings; +import de.uka.ilkd.key.ui.core.KeYSelectionEvent; +import de.uka.ilkd.key.ui.core.KeYSelectionListener; public class HeatmapToggleAction extends MainWindowAction { private static final long serialVersionUID = 1L; diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/KeYProjectHomepageAction.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/KeYProjectHomepageAction.java index 92d4186181e..8f4734d54f0 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/KeYProjectHomepageAction.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/KeYProjectHomepageAction.java @@ -3,7 +3,6 @@ * SPDX-License-Identifier: GPL-2.0-only */ package de.uka.ilkd.key.gui.actions; -import java.awt.*; import java.awt.event.ActionEvent; import java.io.IOException; import java.net.MalformedURLException; @@ -13,8 +12,7 @@ import de.uka.ilkd.key.gui.MainWindow; import de.uka.ilkd.key.gui.fonticons.IconFactory; - -import org.key_project.util.java.SwingUtil; +import de.uka.ilkd.key.ui.util.SwingUtil; /** * Open the KeY project homepage in the system default browser. May be inactive if Java 6 Desktop diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/MacroKeyBinding.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/MacroKeyBinding.java index bc7b0b19c1a..76302a90e05 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/MacroKeyBinding.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/MacroKeyBinding.java @@ -8,7 +8,6 @@ import javax.swing.JComponent; import javax.swing.KeyStroke; -import de.uka.ilkd.key.core.KeYMediator; import de.uka.ilkd.key.gui.ProofMacroMenu; import de.uka.ilkd.key.gui.actions.useractions.ProofMacroUserAction; import de.uka.ilkd.key.gui.keyshortcuts.KeyStrokeManager; @@ -16,6 +15,7 @@ import de.uka.ilkd.key.logic.PosInOccurrence; import de.uka.ilkd.key.macros.ProofMacro; import de.uka.ilkd.key.pp.PosInSequent; +import de.uka.ilkd.key.ui.core.KeYMediator; /** * This class provides means to run macros with key bindings such that these can be bound to the diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/MainWindowAction.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/MainWindowAction.java index be4a31013d0..4d0cd1f241a 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/MainWindowAction.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/MainWindowAction.java @@ -7,11 +7,11 @@ import java.util.Collection; import javax.swing.*; -import de.uka.ilkd.key.core.KeYMediator; -import de.uka.ilkd.key.core.KeYSelectionEvent; -import de.uka.ilkd.key.core.KeYSelectionListener; import de.uka.ilkd.key.gui.MainWindow; import de.uka.ilkd.key.gui.keyshortcuts.KeyStrokeManager; +import de.uka.ilkd.key.ui.core.KeYMediator; +import de.uka.ilkd.key.ui.core.KeYSelectionEvent; +import de.uka.ilkd.key.ui.core.KeYSelectionListener; import static de.uka.ilkd.key.gui.keyshortcuts.KeyStrokeManager.SHORTCUT_KEY_MASK; diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/OpenExampleAction.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/OpenExampleAction.java index 111b4f32bc1..a6cca557ed8 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/OpenExampleAction.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/OpenExampleAction.java @@ -6,11 +6,11 @@ import java.awt.event.ActionEvent; import java.io.File; -import de.uka.ilkd.key.core.Main; import de.uka.ilkd.key.gui.ExampleChooser; import de.uka.ilkd.key.gui.KeYFileChooser; import de.uka.ilkd.key.gui.MainWindow; import de.uka.ilkd.key.gui.fonticons.IconFactory; +import de.uka.ilkd.key.ui.core.Main; /** * Opens a file dialog allowing to select the example to be loaded diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/OpenMostRecentFileAction.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/OpenMostRecentFileAction.java index 32f08a0f2cd..879d87f969d 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/OpenMostRecentFileAction.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/OpenMostRecentFileAction.java @@ -7,12 +7,12 @@ import java.io.File; import java.nio.file.Path; -import de.uka.ilkd.key.core.KeYSelectionEvent; -import de.uka.ilkd.key.core.KeYSelectionListener; import de.uka.ilkd.key.gui.KeYFileChooser; import de.uka.ilkd.key.gui.MainWindow; import de.uka.ilkd.key.gui.ProofSelectionDialog; import de.uka.ilkd.key.gui.fonticons.IconFactory; +import de.uka.ilkd.key.ui.core.KeYSelectionEvent; +import de.uka.ilkd.key.ui.core.KeYSelectionListener; /** * Loads the last opened file diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/OpenSingleJavaFileAction.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/OpenSingleJavaFileAction.java index d11d99b4c73..81f4c89dafc 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/OpenSingleJavaFileAction.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/OpenSingleJavaFileAction.java @@ -11,7 +11,7 @@ import de.uka.ilkd.key.gui.KeYFileChooser; import de.uka.ilkd.key.gui.MainWindow; import de.uka.ilkd.key.gui.WindowUserInterfaceControl; -import de.uka.ilkd.key.proof.io.ProblemLoader; +import de.uka.ilkd.key.ui.proof.io.ProblemLoader; /** * Offers a loading of a single Java file, without considering the folder as part of a classpath. diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/ProofManagementAction.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/ProofManagementAction.java index 01a1bb5f9a3..3a85db12458 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/ProofManagementAction.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/ProofManagementAction.java @@ -5,12 +5,12 @@ import java.awt.event.ActionEvent; -import de.uka.ilkd.key.core.KeYSelectionEvent; -import de.uka.ilkd.key.core.KeYSelectionListener; import de.uka.ilkd.key.gui.MainWindow; import de.uka.ilkd.key.gui.ProofManagementDialog; import de.uka.ilkd.key.gui.fonticons.IconFactory; import de.uka.ilkd.key.gui.notification.events.GeneralFailureEvent; +import de.uka.ilkd.key.ui.core.KeYSelectionEvent; +import de.uka.ilkd.key.ui.core.KeYSelectionListener; /** * Shows the proof management dialog diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/ProofScriptFromFileAction.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/ProofScriptFromFileAction.java index c9287ec7252..a2eebe01b9c 100755 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/ProofScriptFromFileAction.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/ProofScriptFromFileAction.java @@ -7,12 +7,12 @@ import java.io.File; import javax.swing.*; -import de.uka.ilkd.key.core.KeYMediator; import de.uka.ilkd.key.gui.IssueDialog; import de.uka.ilkd.key.gui.KeYFileChooser; import de.uka.ilkd.key.gui.MainWindow; import de.uka.ilkd.key.gui.ProofScriptWorker; import de.uka.ilkd.key.proof.Proof; +import de.uka.ilkd.key.ui.core.KeYMediator; import org.slf4j.Logger; import org.slf4j.LoggerFactory; diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/ProofScriptInputAction.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/ProofScriptInputAction.java index 3eb39a51170..c357ddc7ca7 100755 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/ProofScriptInputAction.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/ProofScriptInputAction.java @@ -11,11 +11,11 @@ import javax.swing.JDialog; import javax.swing.JTextArea; -import de.uka.ilkd.key.core.KeYMediator; import de.uka.ilkd.key.gui.MainWindow; import de.uka.ilkd.key.gui.ProofScriptWorker; import de.uka.ilkd.key.java.Position; import de.uka.ilkd.key.parser.Location; +import de.uka.ilkd.key.ui.core.KeYMediator; /** * The Class ProofScriptInputAction. diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/PruneProofAction.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/PruneProofAction.java index 753211abcf4..ea007c1c3d5 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/PruneProofAction.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/PruneProofAction.java @@ -6,14 +6,14 @@ import java.awt.event.ActionEvent; import de.uka.ilkd.key.control.AutoModeListener; -import de.uka.ilkd.key.core.KeYSelectionEvent; -import de.uka.ilkd.key.core.KeYSelectionListener; import de.uka.ilkd.key.gui.MainWindow; import de.uka.ilkd.key.gui.fonticons.IconFactory; import de.uka.ilkd.key.proof.Node; import de.uka.ilkd.key.proof.Proof; import de.uka.ilkd.key.proof.ProofEvent; import de.uka.ilkd.key.settings.GeneralSettings; +import de.uka.ilkd.key.ui.core.KeYSelectionEvent; +import de.uka.ilkd.key.ui.core.KeYSelectionListener; /** * This action is one part of the previous UndoLastStepAction: It prunes the proof tree below the diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/RunAllProofsAction.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/RunAllProofsAction.java index ceaba6d1bb1..9c4de3ab818 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/RunAllProofsAction.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/RunAllProofsAction.java @@ -11,13 +11,13 @@ import java.util.List; import java.util.stream.Collectors; -import de.uka.ilkd.key.core.KeYMediator; -import de.uka.ilkd.key.core.Main; import de.uka.ilkd.key.gui.MainWindow; import de.uka.ilkd.key.gui.WindowUserInterfaceControl; import de.uka.ilkd.key.proof.Proof; -import de.uka.ilkd.key.proof.io.ProblemLoader; import de.uka.ilkd.key.ui.MediatorProofControl; +import de.uka.ilkd.key.ui.core.KeYMediator; +import de.uka.ilkd.key.ui.core.Main; +import de.uka.ilkd.key.ui.proof.io.ProblemLoader; import org.jspecify.annotations.NonNull; import org.jspecify.annotations.Nullable; diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/SMTInvokeAction.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/SMTInvokeAction.java index cdd94c9a3b0..2e645f48035 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/SMTInvokeAction.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/SMTInvokeAction.java @@ -5,7 +5,6 @@ import java.awt.event.ActionEvent; -import de.uka.ilkd.key.core.KeYMediator; import de.uka.ilkd.key.gui.MainWindow; import de.uka.ilkd.key.gui.smt.SolverListener; import de.uka.ilkd.key.proof.Proof; @@ -14,6 +13,7 @@ import de.uka.ilkd.key.smt.SMTProblem; import de.uka.ilkd.key.smt.SolverLauncher; import de.uka.ilkd.key.smt.SolverTypeCollection; +import de.uka.ilkd.key.ui.core.KeYMediator; /** * This action is responsible for the invocation of an SMT solver For example the toolbar button is diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/SaveBundleAction.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/SaveBundleAction.java index 871225b47fa..9ef87e02d2e 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/SaveBundleAction.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/SaveBundleAction.java @@ -5,13 +5,13 @@ import java.awt.event.ActionEvent; -import de.uka.ilkd.key.core.KeYSelectionEvent; -import de.uka.ilkd.key.core.KeYSelectionListener; import de.uka.ilkd.key.gui.MainWindow; import de.uka.ilkd.key.gui.fonticons.IconFactory; import de.uka.ilkd.key.proof.Proof; import de.uka.ilkd.key.settings.GeneralSettings; import de.uka.ilkd.key.settings.ProofIndependentSettings; +import de.uka.ilkd.key.ui.core.KeYSelectionEvent; +import de.uka.ilkd.key.ui.core.KeYSelectionListener; /** * Saves the currently selected proof as a zip archive with file extension "zproof". The bundle diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/SendFeedbackAction.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/SendFeedbackAction.java index 1d87d1712ac..f20243a704a 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/SendFeedbackAction.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/SendFeedbackAction.java @@ -21,7 +21,6 @@ import javax.swing.filechooser.FileFilter; import javax.swing.text.html.HTMLEditorKit; -import de.uka.ilkd.key.core.KeYMediator; import de.uka.ilkd.key.gui.IssueDialog; import de.uka.ilkd.key.gui.MainWindow; import de.uka.ilkd.key.parser.Location; @@ -29,6 +28,7 @@ import de.uka.ilkd.key.proof.Proof; import de.uka.ilkd.key.proof.io.OutputStreamProofSaver; import de.uka.ilkd.key.settings.ProofSettings; +import de.uka.ilkd.key.ui.core.KeYMediator; import de.uka.ilkd.key.util.ExceptionTools; import de.uka.ilkd.key.util.KeYConstants; import de.uka.ilkd.key.util.KeYResourceManager; diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/SystemInfoAction.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/SystemInfoAction.java deleted file mode 100644 index c6ce7b6646a..00000000000 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/SystemInfoAction.java +++ /dev/null @@ -1,130 +0,0 @@ -/* 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.gui.actions; - -import java.awt.event.ActionEvent; -import java.util.List; -import java.util.Map; -import javax.swing.JDialog; -import javax.swing.JOptionPane; -import javax.swing.JScrollPane; -import javax.swing.JTextArea; - -import de.uka.ilkd.key.gui.MainWindow; -import de.uka.ilkd.key.util.KeYConstants; - -public class SystemInfoAction extends MainWindowAction { - - private static final long serialVersionUID = -4197309658998177157L; - private static final int TEXT_ROWS = 20; - private static final int TEXT_COLS = 60; - - public SystemInfoAction(MainWindow mainWindow) { - super(mainWindow); - setName("System Info"); - // setIcon(IconFactory.help(16)); - } - - @Override - public void actionPerformed(ActionEvent e) { - Object[] contents = new Object[6]; - contents[0] = "KeY info:\n"; - String params = System.getProperty("sun.java.command"); - if (params == null) { - params = "(unknown)"; - } - int i = params.indexOf("Main"); - if (i > 0) { - params = params.substring(i + 4); - } - java.lang.management.RuntimeMXBean rmb = - java.lang.management.ManagementFactory.getRuntimeMXBean(); - final String keyInfoText = "Version: " + KeYConstants.VERSION + "\nKeY parameters: " - + params + "\nVM parameters: " + formatList(rmb.getInputArguments()); - JTextArea keyInfo = new JTextArea(keyInfoText, 3, TEXT_COLS); - keyInfo.setEditable(false); - contents[1] = keyInfo; - - contents[2] = getMemoryInfo() + "\n\nEnvironment variables:\n"; - JScrollPane scroll = new JScrollPane(); - JTextArea text = new JTextArea(getEnv(), TEXT_ROWS / 3, 40); - text.setEditable(false); - text.setCaretPosition(0); - scroll.setViewportView(text); - contents[3] = scroll; - - contents[4] = "\nJava properties:\n"; - JScrollPane scroll2 = new JScrollPane(); - JTextArea text2 = new JTextArea(getProperties(), TEXT_ROWS, 40); - text2.setEditable(false); - text2.setCaretPosition(0); - scroll2.setViewportView(text2); - contents[5] = scroll2; - - JOptionPane pane = - new JOptionPane(contents, JOptionPane.INFORMATION_MESSAGE, JOptionPane.DEFAULT_OPTION); - JDialog dialog = pane.createDialog(mainWindow, "System information"); - dialog.setVisible(true); - } - - @SuppressWarnings("finally") - private String getProperties() { - StringBuffer sb = new StringBuffer(); - java.util.Properties props; - try { - props = System.getProperties(); - formatMap(sb, props); - } finally { - return sb.toString(); - } - } - - - @SuppressWarnings("finally") - private String getEnv() { - StringBuffer sb = new StringBuffer(); - try { - formatMap(sb, System.getenv()); - } finally { - return sb.toString(); - } - } - - private void formatMap(StringBuffer sb, Map props) { - for (Object o : props.keySet()) { - sb.append(o); - sb.append("=\""); - sb.append(props.get(o)); - sb.append("\"\n"); - } - } - - private String formatList(List l) { - StringBuilder sb = new StringBuilder(); - for (Object o : l) { - sb.append(o); - sb.append(" "); - } - sb.deleteCharAt(sb.length() - 1); - return sb.toString(); - } - - private String getMemoryInfo() { - Runtime rt = Runtime.getRuntime(); - rt.gc(); // call garbage collection to normalize stats - - StringBuilder sb = new StringBuilder(); - long maxMemory = rt.maxMemory(); - long allocatedMemory = rt.totalMemory(); - long freeMemory = rt.freeMemory(); - - sb.append("\nAvailable processors: ").append(rt.availableProcessors()); - sb.append("\nFree VM memory: ").append(freeMemory / 1024 / 1024).append(" MB"); - sb.append("\nAllocated VM memory: ").append(allocatedMemory / 1024 / 1024).append(" MB"); - sb.append("\nMax VM memory: ").append(maxMemory / 1024 / 1024).append(" MB"); - sb.append("\nTotal free VM memory: ") - .append((freeMemory + (maxMemory - allocatedMemory)) / 1024 / 1024).append(" MB"); - return sb.toString(); - } -} diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/TermLabelMenu.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/TermLabelMenu.java index 1cca9da9dd1..a6af73022e6 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/TermLabelMenu.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/TermLabelMenu.java @@ -12,9 +12,9 @@ import de.uka.ilkd.key.control.TermLabelVisibilityManager; import de.uka.ilkd.key.control.event.TermLabelVisibilityManagerEvent; import de.uka.ilkd.key.control.event.TermLabelVisibilityManagerListener; -import de.uka.ilkd.key.core.KeYSelectionEvent; -import de.uka.ilkd.key.core.KeYSelectionListener; import de.uka.ilkd.key.gui.MainWindow; +import de.uka.ilkd.key.ui.core.KeYSelectionEvent; +import de.uka.ilkd.key.ui.core.KeYSelectionListener; import org.key_project.logic.Name; diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/useractions/AutoModeUserAction.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/useractions/AutoModeUserAction.java index aff954c6d91..2bba6a63a59 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/useractions/AutoModeUserAction.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/useractions/AutoModeUserAction.java @@ -3,8 +3,8 @@ * SPDX-License-Identifier: GPL-2.0-only */ package de.uka.ilkd.key.gui.actions.useractions; -import de.uka.ilkd.key.core.KeYMediator; import de.uka.ilkd.key.proof.Proof; +import de.uka.ilkd.key.ui.core.KeYMediator; /** * User action to start auto mode (automatic proof search). diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/useractions/FocussedAutoModeUserAction.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/useractions/FocussedAutoModeUserAction.java index db205ac39b9..e5688808e91 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/useractions/FocussedAutoModeUserAction.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/useractions/FocussedAutoModeUserAction.java @@ -3,9 +3,9 @@ * SPDX-License-Identifier: GPL-2.0-only */ package de.uka.ilkd.key.gui.actions.useractions; -import de.uka.ilkd.key.core.KeYMediator; import de.uka.ilkd.key.logic.PosInOccurrence; import de.uka.ilkd.key.proof.Proof; +import de.uka.ilkd.key.ui.core.KeYMediator; /** * User action for "Apply rules automatically here" (i.e. focussed auto mode). diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/useractions/ProofLoadUserAction.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/useractions/ProofLoadUserAction.java index ab1d28e0cda..ca3b3e319b3 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/useractions/ProofLoadUserAction.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/useractions/ProofLoadUserAction.java @@ -3,8 +3,8 @@ * SPDX-License-Identifier: GPL-2.0-only */ package de.uka.ilkd.key.gui.actions.useractions; -import de.uka.ilkd.key.core.KeYMediator; import de.uka.ilkd.key.proof.Proof; +import de.uka.ilkd.key.ui.core.KeYMediator; /** * Virtual user action to undo loading a proof. diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/useractions/ProofMacroUserAction.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/useractions/ProofMacroUserAction.java index 30ec29f1bbc..12b9efdb319 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/useractions/ProofMacroUserAction.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/useractions/ProofMacroUserAction.java @@ -3,10 +3,10 @@ * SPDX-License-Identifier: GPL-2.0-only */ package de.uka.ilkd.key.gui.actions.useractions; -import de.uka.ilkd.key.core.KeYMediator; import de.uka.ilkd.key.logic.PosInOccurrence; import de.uka.ilkd.key.macros.ProofMacro; import de.uka.ilkd.key.proof.Proof; +import de.uka.ilkd.key.ui.core.KeYMediator; /** * User action to apply a proof macro. diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/useractions/ProofModifyingUserAction.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/useractions/ProofModifyingUserAction.java index dd80e6e79e5..922567a6885 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/useractions/ProofModifyingUserAction.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/useractions/ProofModifyingUserAction.java @@ -7,10 +7,10 @@ import java.util.List; import java.util.stream.Collectors; -import de.uka.ilkd.key.core.KeYMediator; import de.uka.ilkd.key.proof.Goal; import de.uka.ilkd.key.proof.Node; import de.uka.ilkd.key.proof.Proof; +import de.uka.ilkd.key.ui.core.KeYMediator; /** * User action that modifies the proof in some way. diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/useractions/ProofRuleUserAction.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/useractions/ProofRuleUserAction.java index 354f1466a39..1553fb19495 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/useractions/ProofRuleUserAction.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/useractions/ProofRuleUserAction.java @@ -3,9 +3,9 @@ * SPDX-License-Identifier: GPL-2.0-only */ package de.uka.ilkd.key.gui.actions.useractions; -import de.uka.ilkd.key.core.KeYMediator; import de.uka.ilkd.key.proof.Node; import de.uka.ilkd.key.proof.Proof; +import de.uka.ilkd.key.ui.core.KeYMediator; /** * User action that represents the manual application of a rule. diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/useractions/ProofSMTApplyUserAction.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/useractions/ProofSMTApplyUserAction.java index 94f0d15e065..05dd78d8ab3 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/useractions/ProofSMTApplyUserAction.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/useractions/ProofSMTApplyUserAction.java @@ -7,7 +7,6 @@ import java.util.HashSet; import java.util.Iterator; -import de.uka.ilkd.key.core.KeYMediator; import de.uka.ilkd.key.gui.smt.SolverListener; import de.uka.ilkd.key.logic.PosInOccurrence; import de.uka.ilkd.key.proof.Goal; @@ -16,6 +15,7 @@ import de.uka.ilkd.key.rule.IBuiltInRuleApp; import de.uka.ilkd.key.smt.*; import de.uka.ilkd.key.smt.SMTRuleApp; +import de.uka.ilkd.key.ui.core.KeYMediator; import org.key_project.util.collection.ImmutableList; diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/useractions/RunStrategyOnNodeUserAction.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/useractions/RunStrategyOnNodeUserAction.java index 9e7eeea57b2..555ba8d5faf 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/useractions/RunStrategyOnNodeUserAction.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/useractions/RunStrategyOnNodeUserAction.java @@ -3,10 +3,10 @@ * SPDX-License-Identifier: GPL-2.0-only */ package de.uka.ilkd.key.gui.actions.useractions; -import de.uka.ilkd.key.core.KeYMediator; import de.uka.ilkd.key.proof.Goal; import de.uka.ilkd.key.proof.Node; import de.uka.ilkd.key.proof.Proof; +import de.uka.ilkd.key.ui.core.KeYMediator; import org.key_project.util.collection.ImmutableList; import org.key_project.util.collection.ImmutableSLList; diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/useractions/UserAction.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/useractions/UserAction.java index db364620b11..cd78fd203e7 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/useractions/UserAction.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/actions/useractions/UserAction.java @@ -6,8 +6,8 @@ import java.awt.event.ActionEvent; import java.awt.event.ActionListener; -import de.uka.ilkd.key.core.KeYMediator; import de.uka.ilkd.key.proof.Proof; +import de.uka.ilkd.key.ui.core.KeYMediator; /** * Abstract concept of an action performed by the user. diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/docking/DockingHelper.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/docking/DockingHelper.java index 5c76e148649..a30e29314cf 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/docking/DockingHelper.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/docking/DockingHelper.java @@ -20,18 +20,13 @@ import de.uka.ilkd.key.gui.prooftree.ProofTreeView; import de.uka.ilkd.key.gui.sourceview.SourceViewFrame; -import bibliothek.gui.dock.common.CGrid; -import bibliothek.gui.dock.common.DefaultSingleCDockable; -import bibliothek.gui.dock.common.MultipleCDockable; -import bibliothek.gui.dock.common.SingleCDockable; -import bibliothek.gui.dock.common.action.CAction; -import bibliothek.gui.dock.common.action.CButton; -import bibliothek.gui.dock.common.action.CCheckBox; -import bibliothek.gui.dock.common.action.core.CommonDecoratableDockAction; -import bibliothek.gui.dock.common.intern.CDockable; -import bibliothek.gui.dock.common.intern.action.CDecorateableAction; -import bibliothek.gui.dock.control.focus.DefaultFocusRequest; -import bibliothek.gui.dock.control.focus.FocusRequest; +import org.key_project.dockingframes.common.common.*; +import org.key_project.dockingframes.common.common.action.*; +import org.key_project.dockingframes.common.common.action.core.*; +import org.key_project.dockingframes.common.common.intern.*; +import org.key_project.dockingframes.common.common.intern.action.*; +import org.key_project.dockingframes.core.gui.dock.control.focus.*; + import org.jspecify.annotations.NonNull; public class DockingHelper { diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/docking/DockingLayout.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/docking/DockingLayout.java index 68fa871169e..5e113c26cb4 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/docking/DockingLayout.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/docking/DockingLayout.java @@ -13,7 +13,6 @@ import java.util.List; import javax.swing.*; -import de.uka.ilkd.key.core.KeYMediator; import de.uka.ilkd.key.gui.GUIListener; import de.uka.ilkd.key.gui.MainWindow; import de.uka.ilkd.key.gui.actions.MainWindowAction; @@ -24,10 +23,12 @@ import de.uka.ilkd.key.gui.fonticons.IconFontSwing; import de.uka.ilkd.key.gui.keyshortcuts.KeyStrokeManager; import de.uka.ilkd.key.settings.PathConfig; +import de.uka.ilkd.key.ui.core.KeYMediator; + +import org.key_project.dockingframes.common.common.CControl; +import org.key_project.dockingframes.core.gui.dock.util.IconManager; +import org.key_project.dockingframes.core.gui.dock.util.Priority; -import bibliothek.gui.dock.common.CControl; -import bibliothek.gui.dock.util.IconManager; -import bibliothek.gui.dock.util.Priority; import org.jspecify.annotations.NonNull; import org.slf4j.Logger; import org.slf4j.LoggerFactory; diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/docking/DynamicCMenu.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/docking/DynamicCMenu.java index c57dcedd03e..5a972dd55be 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/docking/DynamicCMenu.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/docking/DynamicCMenu.java @@ -6,17 +6,15 @@ import java.util.function.Supplier; import javax.swing.*; -import bibliothek.gui.Dockable; -import bibliothek.gui.dock.action.ActionType; -import bibliothek.gui.dock.action.DockActionSource; -import bibliothek.gui.dock.action.MenuDockAction; -import bibliothek.gui.dock.action.actions.SimpleDockAction; -import bibliothek.gui.dock.action.view.ActionViewConverter; -import bibliothek.gui.dock.action.view.ViewTarget; -import bibliothek.gui.dock.common.action.CAction; -import bibliothek.gui.dock.common.action.CMenu; -import bibliothek.gui.dock.common.action.core.CommonDecoratableDockAction; -import bibliothek.gui.dock.common.intern.action.CDecorateableAction; +import org.key_project.dockingframes.common.common.action.*; +import org.key_project.dockingframes.common.common.action.core.CommonDecoratableDockAction; +import org.key_project.dockingframes.common.common.intern.action.CDecorateableAction; +import org.key_project.dockingframes.core.gui.Dockable; +import org.key_project.dockingframes.core.gui.dock.action.*; +import org.key_project.dockingframes.core.gui.dock.action.actions.*; +import org.key_project.dockingframes.core.gui.dock.action.view.ActionViewConverter; +import org.key_project.dockingframes.core.gui.dock.action.view.ViewTarget; + /** * CMenu that gets (re-)generated when the action gets fired using the provided supplier. diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/extension/api/ContextMenuAdapter.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/extension/api/ContextMenuAdapter.java index 5aa68721268..ed82c60227e 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/extension/api/ContextMenuAdapter.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/extension/api/ContextMenuAdapter.java @@ -7,11 +7,11 @@ import java.util.List; import javax.swing.*; -import de.uka.ilkd.key.core.KeYMediator; import de.uka.ilkd.key.pp.PosInSequent; import de.uka.ilkd.key.proof.Node; import de.uka.ilkd.key.proof.Proof; import de.uka.ilkd.key.rule.Rule; +import de.uka.ilkd.key.ui.core.KeYMediator; import org.jspecify.annotations.NonNull; diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/extension/api/KeYGuiExtension.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/extension/api/KeYGuiExtension.java index ef94d9dc7df..ffba6e2b9f2 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/extension/api/KeYGuiExtension.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/extension/api/KeYGuiExtension.java @@ -12,7 +12,6 @@ import javax.swing.JMenu; import javax.swing.JToolBar; -import de.uka.ilkd.key.core.KeYMediator; import de.uka.ilkd.key.gui.GoalList; import de.uka.ilkd.key.gui.InfoView; import de.uka.ilkd.key.gui.MainWindow; @@ -23,6 +22,7 @@ import de.uka.ilkd.key.gui.settings.SettingsProvider; import de.uka.ilkd.key.gui.sourceview.SourceView; import de.uka.ilkd.key.pp.PosInSequent; +import de.uka.ilkd.key.ui.core.KeYMediator; import org.jspecify.annotations.NonNull; diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/extension/api/KeyboardShortcutAdapter.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/extension/api/KeyboardShortcutAdapter.java index 2f1f344a039..73ea5c0fa26 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/extension/api/KeyboardShortcutAdapter.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/extension/api/KeyboardShortcutAdapter.java @@ -8,13 +8,13 @@ import java.util.Objects; import javax.swing.*; -import de.uka.ilkd.key.core.KeYMediator; import de.uka.ilkd.key.gui.GoalList; import de.uka.ilkd.key.gui.InfoView; import de.uka.ilkd.key.gui.StrategySelectionView; import de.uka.ilkd.key.gui.nodeviews.SequentView; import de.uka.ilkd.key.gui.prooftree.ProofTreeView; import de.uka.ilkd.key.gui.sourceview.SourceView; +import de.uka.ilkd.key.ui.core.KeYMediator; /** * Adapter for {@link KeYGuiExtension.KeyboardShortcuts} interface. diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/extension/api/TabPanel.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/extension/api/TabPanel.java index 6c7dc4b05ba..0648ffd7dd4 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/extension/api/TabPanel.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/extension/api/TabPanel.java @@ -7,8 +7,9 @@ import java.util.Collections; import javax.swing.*; -import bibliothek.gui.dock.common.action.CAction; -import bibliothek.gui.dock.common.intern.DefaultCDockable; +import org.key_project.dockingframes.common.common.action.CAction; +import org.key_project.dockingframes.common.common.intern.DefaultCDockable; + import org.jspecify.annotations.NonNull; import org.jspecify.annotations.Nullable; diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/extension/impl/KeYGuiExtensionFacade.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/extension/impl/KeYGuiExtensionFacade.java index 1b2e01c96af..84123289f03 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/extension/impl/KeYGuiExtensionFacade.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/extension/impl/KeYGuiExtensionFacade.java @@ -12,7 +12,6 @@ import java.util.stream.Stream; import javax.swing.*; -import de.uka.ilkd.key.core.KeYMediator; import de.uka.ilkd.key.gui.MainWindow; import de.uka.ilkd.key.gui.actions.KeyAction; import de.uka.ilkd.key.gui.extension.api.ContextMenuKind; @@ -20,6 +19,7 @@ import de.uka.ilkd.key.gui.extension.api.TabPanel; import de.uka.ilkd.key.pp.PosInSequent; import de.uka.ilkd.key.proof.Proof; +import de.uka.ilkd.key.ui.core.KeYMediator; /** * Facade for retrieving the GUI extensions. diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/extension/impl/TestExtension.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/extension/impl/TestExtension.java index 549aedbd1d6..dfb3442dcf8 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/extension/impl/TestExtension.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/extension/impl/TestExtension.java @@ -11,7 +11,6 @@ import java.util.List; import javax.swing.*; -import de.uka.ilkd.key.core.KeYMediator; import de.uka.ilkd.key.gui.MainWindow; import de.uka.ilkd.key.gui.actions.KeyAction; import de.uka.ilkd.key.gui.extension.api.ContextMenuAdapter; @@ -26,6 +25,7 @@ import de.uka.ilkd.key.proof.Node; import de.uka.ilkd.key.proof.Proof; import de.uka.ilkd.key.rule.Rule; +import de.uka.ilkd.key.ui.core.KeYMediator; import org.jspecify.annotations.NonNull; import org.slf4j.Logger; diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/help/HelpFacade.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/help/HelpFacade.java index 3c753d3a3ed..59bdad324b2 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/help/HelpFacade.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/help/HelpFacade.java @@ -13,11 +13,11 @@ import de.uka.ilkd.key.gui.actions.KeyAction; import de.uka.ilkd.key.gui.fonticons.IconFactory; +import de.uka.ilkd.key.ui.util.SwingUtil; -import org.key_project.util.java.SwingUtil; +import org.key_project.dockingframes.common.common.action.CAction; +import org.key_project.dockingframes.common.common.action.CButton; -import bibliothek.gui.dock.common.action.CAction; -import bibliothek.gui.dock.common.action.CButton; import org.slf4j.Logger; import org.slf4j.LoggerFactory; diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/join/JoinMenuItem.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/join/JoinMenuItem.java index 2b55d03b369..200a49902d7 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/join/JoinMenuItem.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/join/JoinMenuItem.java @@ -7,7 +7,6 @@ import java.util.List; import javax.swing.*; -import de.uka.ilkd.key.core.KeYMediator; import de.uka.ilkd.key.gui.notification.events.ExceptionFailureEvent; import de.uka.ilkd.key.proof.Goal; import de.uka.ilkd.key.proof.Proof; @@ -15,6 +14,7 @@ import de.uka.ilkd.key.proof.join.JoinProcessor.Listener; import de.uka.ilkd.key.proof.join.PredicateEstimator; import de.uka.ilkd.key.proof.join.ProspectivePartner; +import de.uka.ilkd.key.ui.core.KeYMediator; import org.key_project.util.collection.ImmutableList; diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/lemmatagenerator/LemmataAutoModeOptions.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/lemmatagenerator/LemmataAutoModeOptions.java index b8f3a450684..3b5d655ca91 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/lemmatagenerator/LemmataAutoModeOptions.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/lemmatagenerator/LemmataAutoModeOptions.java @@ -7,10 +7,10 @@ import java.util.Collection; import java.util.LinkedList; -import de.uka.ilkd.key.core.Main; import de.uka.ilkd.key.proof.Proof; -import de.uka.ilkd.key.util.CommandLine; -import de.uka.ilkd.key.util.CommandLineException; +import de.uka.ilkd.key.ui.core.Main; +import de.uka.ilkd.key.ui.util.CommandLine; +import de.uka.ilkd.key.ui.util.CommandLineException; import org.slf4j.Logger; import org.slf4j.LoggerFactory; diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/mergerule/MergeRuleMenuItem.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/mergerule/MergeRuleMenuItem.java index b62d5323d79..2ae4bdd3720 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/mergerule/MergeRuleMenuItem.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/mergerule/MergeRuleMenuItem.java @@ -6,7 +6,6 @@ import java.awt.event.ActionEvent; import javax.swing.*; -import de.uka.ilkd.key.core.KeYMediator; import de.uka.ilkd.key.gui.notification.events.ExceptionFailureEvent; import de.uka.ilkd.key.java.Services; import de.uka.ilkd.key.logic.PosInOccurrence; @@ -16,6 +15,7 @@ import de.uka.ilkd.key.prover.impl.DefaultTaskStartedInfo; import de.uka.ilkd.key.rule.merge.MergeRule; import de.uka.ilkd.key.rule.merge.MergeRuleBuiltInRuleApp; +import de.uka.ilkd.key.ui.core.KeYMediator; /** * The menu item for the state merging rule. diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/nodeviews/CurrentGoalView.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/nodeviews/CurrentGoalView.java index 5704821655d..9e0bde820c3 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/nodeviews/CurrentGoalView.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/nodeviews/CurrentGoalView.java @@ -12,7 +12,6 @@ import java.util.LinkedList; import javax.swing.*; -import de.uka.ilkd.key.core.KeYMediator; import de.uka.ilkd.key.gui.ApplyTacletDialog; import de.uka.ilkd.key.gui.GUIListener; import de.uka.ilkd.key.gui.MainWindow; @@ -23,6 +22,7 @@ import de.uka.ilkd.key.pp.SequentViewLogicPrinter; import de.uka.ilkd.key.proof.Goal; import de.uka.ilkd.key.rule.TacletApp; +import de.uka.ilkd.key.ui.core.KeYMediator; import de.uka.ilkd.key.util.Debug; import org.slf4j.Logger; diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/nodeviews/CurrentGoalViewListener.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/nodeviews/CurrentGoalViewListener.java index 16a2d2d2ac8..8905affc761 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/nodeviews/CurrentGoalViewListener.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/nodeviews/CurrentGoalViewListener.java @@ -8,11 +8,11 @@ import java.awt.event.MouseEvent; import javax.swing.*; -import de.uka.ilkd.key.core.KeYMediator; import de.uka.ilkd.key.gui.ProofMacroMenu; import de.uka.ilkd.key.pp.PosInSequent; import de.uka.ilkd.key.rule.BuiltInRule; import de.uka.ilkd.key.settings.ProofIndependentSettings; +import de.uka.ilkd.key.ui.core.KeYMediator; import org.key_project.util.collection.ImmutableList; diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/nodeviews/CurrentGoalViewMenu.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/nodeviews/CurrentGoalViewMenu.java index 3fc648efbee..a78adf54d88 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/nodeviews/CurrentGoalViewMenu.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/nodeviews/CurrentGoalViewMenu.java @@ -17,7 +17,6 @@ import java.util.Set; import javax.swing.*; -import de.uka.ilkd.key.core.KeYMediator; import de.uka.ilkd.key.gui.MainWindow; import de.uka.ilkd.key.gui.ProofMacroMenu; import de.uka.ilkd.key.gui.actions.useractions.FocussedAutoModeUserAction; @@ -50,6 +49,7 @@ import de.uka.ilkd.key.smt.SMTProblem; import de.uka.ilkd.key.smt.SolverLauncher; import de.uka.ilkd.key.smt.SolverTypeCollection; +import de.uka.ilkd.key.ui.core.KeYMediator; import org.key_project.util.collection.ImmutableList; import org.key_project.util.collection.ImmutableSLList; diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/nodeviews/DragNDropInstantiator.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/nodeviews/DragNDropInstantiator.java index ad048dbd1b3..00d9468a367 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/nodeviews/DragNDropInstantiator.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/nodeviews/DragNDropInstantiator.java @@ -17,7 +17,6 @@ import java.util.List; import javax.swing.*; -import de.uka.ilkd.key.core.KeYMediator; import de.uka.ilkd.key.gui.MainWindow; import de.uka.ilkd.key.java.Services; import de.uka.ilkd.key.logic.PosInOccurrence; @@ -29,6 +28,7 @@ import de.uka.ilkd.key.rule.inst.IllegalInstantiationException; import de.uka.ilkd.key.rule.tacletbuilder.TacletGoalTemplate; import de.uka.ilkd.key.settings.ProofIndependentSettings; +import de.uka.ilkd.key.ui.core.KeYMediator; import org.key_project.util.collection.ImmutableList; import org.key_project.util.collection.ImmutableSLList; diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/nodeviews/SequentViewDock.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/nodeviews/SequentViewDock.java index 626bbb9e309..cac09f67a26 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/nodeviews/SequentViewDock.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/nodeviews/SequentViewDock.java @@ -7,7 +7,6 @@ import java.awt.event.ActionEvent; import javax.swing.*; -import de.uka.ilkd.key.core.KeYSelectionModel; import de.uka.ilkd.key.gui.MainWindow; import de.uka.ilkd.key.gui.actions.KeyAction; import de.uka.ilkd.key.gui.actions.MainWindowAction; @@ -15,10 +14,12 @@ import de.uka.ilkd.key.gui.fonticons.IconFactory; import de.uka.ilkd.key.proof.Node; import de.uka.ilkd.key.proof.Proof; +import de.uka.ilkd.key.ui.core.KeYSelectionModel; + +import org.key_project.dockingframes.common.common.CLocation; +import org.key_project.dockingframes.common.common.DefaultMultipleCDockable; +import org.key_project.dockingframes.common.common.NullMultipleCDockableFactory; -import bibliothek.gui.dock.common.CLocation; -import bibliothek.gui.dock.common.DefaultMultipleCDockable; -import bibliothek.gui.dock.common.NullMultipleCDockableFactory; /** * @author Alexander Weigl diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/nodeviews/TacletDescriber.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/nodeviews/TacletDescriber.java index 13dfee01edf..05e6bddac01 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/nodeviews/TacletDescriber.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/nodeviews/TacletDescriber.java @@ -5,13 +5,13 @@ import javax.swing.*; -import de.uka.ilkd.key.core.KeYMediator; import de.uka.ilkd.key.gui.MainWindow; import de.uka.ilkd.key.logic.op.*; import de.uka.ilkd.key.pp.SequentViewLogicPrinter; import de.uka.ilkd.key.pp.VisibleTermLabels; import de.uka.ilkd.key.rule.*; import de.uka.ilkd.key.rule.inst.GenericSortInstantiations; +import de.uka.ilkd.key.ui.core.KeYMediator; import org.key_project.util.collection.ImmutableSet; diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/notification/NotificationManager.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/notification/NotificationManager.java index 17ab2ea9f83..91c87248b10 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/notification/NotificationManager.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/notification/NotificationManager.java @@ -8,9 +8,9 @@ import javax.swing.JFrame; import de.uka.ilkd.key.control.AutoModeListener; -import de.uka.ilkd.key.core.KeYMediator; import de.uka.ilkd.key.gui.notification.events.NotificationEvent; import de.uka.ilkd.key.proof.ProofEvent; +import de.uka.ilkd.key.ui.core.KeYMediator; /** * The notificatin manager controls the list of active notification tasks. It receives KeY System diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/originlabels/OriginTermLabelVisualizer.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/originlabels/OriginTermLabelVisualizer.java index e08bdb030a5..2acb6402e03 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/originlabels/OriginTermLabelVisualizer.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/originlabels/OriginTermLabelVisualizer.java @@ -17,7 +17,6 @@ import javax.swing.tree.TreePath; import de.uka.ilkd.key.control.TermLabelVisibilityManager; -import de.uka.ilkd.key.core.KeYMediator; import de.uka.ilkd.key.gui.MainWindow; import de.uka.ilkd.key.gui.NodeInfoVisualizer; import de.uka.ilkd.key.gui.nodeviews.SequentView; @@ -29,13 +28,14 @@ import de.uka.ilkd.key.proof.*; import de.uka.ilkd.key.proof.event.ProofDisposedEvent; import de.uka.ilkd.key.proof.event.ProofDisposedListener; +import de.uka.ilkd.key.ui.core.KeYMediator; import de.uka.ilkd.key.util.pp.UnbalancedBlocksException; +import org.key_project.dockingframes.common.common.DefaultSingleCDockable; import org.key_project.util.collection.ImmutableArray; import org.key_project.util.collection.ImmutableList; import org.key_project.util.collection.ImmutableSLList; -import bibliothek.gui.dock.common.DefaultSingleCDockable; /** * This UI component visualizes the {@link OriginTermLabel}s of a term and its sub-terms. diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/originlabels/OriginTermLabelsExt.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/originlabels/OriginTermLabelsExt.java index fdfafb05674..674c59848ac 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/originlabels/OriginTermLabelsExt.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/originlabels/OriginTermLabelsExt.java @@ -10,7 +10,6 @@ import java.util.stream.Collectors; import javax.swing.Action; -import de.uka.ilkd.key.core.KeYMediator; import de.uka.ilkd.key.gui.MainWindow; import de.uka.ilkd.key.gui.NodeInfoVisualizer; import de.uka.ilkd.key.gui.actions.KeyAction; @@ -23,6 +22,7 @@ import de.uka.ilkd.key.logic.label.OriginTermLabel.Origin; import de.uka.ilkd.key.pp.PosInSequent; import de.uka.ilkd.key.proof.Node; +import de.uka.ilkd.key.ui.core.KeYMediator; /** * Extension adapter for {@link OriginTermLabel}s and {@link OriginTermLabelVisualizer}s. diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/action_history/ActionHistoryExtension.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/action_history/ActionHistoryExtension.java index 18fc71d4473..adb284e7bcd 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/action_history/ActionHistoryExtension.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/action_history/ActionHistoryExtension.java @@ -11,9 +11,6 @@ import java.util.WeakHashMap; import javax.swing.*; -import de.uka.ilkd.key.core.KeYMediator; -import de.uka.ilkd.key.core.KeYSelectionEvent; -import de.uka.ilkd.key.core.KeYSelectionListener; import de.uka.ilkd.key.gui.MainWindow; import de.uka.ilkd.key.gui.UserActionListener; import de.uka.ilkd.key.gui.actions.useractions.UserAction; @@ -22,6 +19,9 @@ import de.uka.ilkd.key.proof.Proof; import de.uka.ilkd.key.proof.event.ProofDisposedEvent; import de.uka.ilkd.key.proof.event.ProofDisposedListener; +import de.uka.ilkd.key.ui.core.KeYMediator; +import de.uka.ilkd.key.ui.core.KeYSelectionEvent; +import de.uka.ilkd.key.ui.core.KeYSelectionListener; /** diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/action_history/StateChangeListener.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/action_history/StateChangeListener.java index 8ec550848af..99a21927fa3 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/action_history/StateChangeListener.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/action_history/StateChangeListener.java @@ -6,7 +6,6 @@ import java.util.List; import de.uka.ilkd.key.control.InteractionListener; -import de.uka.ilkd.key.core.KeYMediator; import de.uka.ilkd.key.gui.actions.useractions.ProofRuleUserAction; import de.uka.ilkd.key.logic.PosInOccurrence; import de.uka.ilkd.key.macros.ProofMacro; @@ -18,6 +17,7 @@ import de.uka.ilkd.key.rule.IBuiltInRuleApp; import de.uka.ilkd.key.rule.RuleApp; import de.uka.ilkd.key.settings.Settings; +import de.uka.ilkd.key.ui.core.KeYMediator; /** * Listener object to record various user actions (currently only rule applications) diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/javac/JavacExtension.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/javac/JavacExtension.java index c8d62a2e080..9c365e85f70 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/javac/JavacExtension.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/javac/JavacExtension.java @@ -12,9 +12,6 @@ import java.util.concurrent.ExecutionException; import javax.swing.*; -import de.uka.ilkd.key.core.KeYMediator; -import de.uka.ilkd.key.core.KeYSelectionEvent; -import de.uka.ilkd.key.core.KeYSelectionListener; import de.uka.ilkd.key.gui.IssueDialog; import de.uka.ilkd.key.gui.MainWindow; import de.uka.ilkd.key.gui.PositionedIssueString; @@ -24,6 +21,9 @@ import de.uka.ilkd.key.gui.fonticons.MaterialDesignRegular; import de.uka.ilkd.key.proof.JavaModel; import de.uka.ilkd.key.proof.Proof; +import de.uka.ilkd.key.ui.core.KeYMediator; +import de.uka.ilkd.key.ui.core.KeYSelectionEvent; +import de.uka.ilkd.key.ui.core.KeYSelectionListener; import org.slf4j.Logger; import org.slf4j.LoggerFactory; diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/ProofTreePopupFactory.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/ProofTreePopupFactory.java index 3866cf218af..0c62f731a4e 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/ProofTreePopupFactory.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/ProofTreePopupFactory.java @@ -12,7 +12,6 @@ import javax.swing.tree.TreeNode; import javax.swing.tree.TreePath; -import de.uka.ilkd.key.core.KeYMediator; import de.uka.ilkd.key.gui.InspectorForDecisionPredicates; import de.uka.ilkd.key.gui.MainWindow; import de.uka.ilkd.key.gui.ProofMacroMenu; @@ -37,6 +36,7 @@ import de.uka.ilkd.key.rule.OneStepSimplifierRuleApp; import de.uka.ilkd.key.settings.FeatureSettings; import de.uka.ilkd.key.settings.GeneralSettings; +import de.uka.ilkd.key.ui.core.KeYMediator; import static de.uka.ilkd.key.settings.FeatureSettings.createFeature; diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/ProofTreeSettingsMenuFactory.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/ProofTreeSettingsMenuFactory.java index 9e83ad4c04e..605c2ffcf9b 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/ProofTreeSettingsMenuFactory.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/ProofTreeSettingsMenuFactory.java @@ -11,10 +11,7 @@ import de.uka.ilkd.key.proof.Goal; import de.uka.ilkd.key.proof.Proof; -import bibliothek.gui.dock.common.action.CAction; -import bibliothek.gui.dock.common.action.CButton; -import bibliothek.gui.dock.common.action.CCheckBox; -import bibliothek.gui.dock.common.action.CMenu; +import org.key_project.dockingframes.common.common.action.*; import static de.uka.ilkd.key.gui.prooftree.ProofTreePopupFactory.ICON_SIZE; diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/ProofTreeView.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/ProofTreeView.java index d0361823e12..588d29920de 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/ProofTreeView.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/ProofTreeView.java @@ -16,9 +16,6 @@ import javax.swing.tree.*; import de.uka.ilkd.key.control.AutoModeListener; -import de.uka.ilkd.key.core.KeYMediator; -import de.uka.ilkd.key.core.KeYSelectionEvent; -import de.uka.ilkd.key.core.KeYSelectionListener; import de.uka.ilkd.key.gui.GUIListener; import de.uka.ilkd.key.gui.NodeInfoVisualizer; import de.uka.ilkd.key.gui.NodeInfoVisualizerListener; @@ -38,11 +35,14 @@ import de.uka.ilkd.key.proof.reference.ClosedBy; import de.uka.ilkd.key.rule.RuleApp; import de.uka.ilkd.key.settings.ProofIndependentSettings; -import de.uka.ilkd.key.util.ThreadUtilities; +import de.uka.ilkd.key.ui.core.KeYMediator; +import de.uka.ilkd.key.ui.core.KeYSelectionEvent; +import de.uka.ilkd.key.ui.core.KeYSelectionListener; +import de.uka.ilkd.key.ui.util.ThreadUtilities; +import org.key_project.dockingframes.common.common.action.CAction; import org.key_project.util.collection.ImmutableList; -import bibliothek.gui.dock.common.action.CAction; import org.jspecify.annotations.NonNull; import org.slf4j.Logger; import org.slf4j.LoggerFactory; diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/smt/InformationWindow.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/smt/InformationWindow.java index 0a681e55bd4..cbeedf53396 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/smt/InformationWindow.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/smt/InformationWindow.java @@ -12,6 +12,7 @@ import de.uka.ilkd.key.gui.configuration.Config; import de.uka.ilkd.key.smt.SMTSolver; +import de.uka.ilkd.key.smt.communication.AbstractSolverSocket; import de.uka.ilkd.key.smt.model.Model; import de.uka.ilkd.key.smt.solvertypes.SolverTypes; @@ -92,11 +93,12 @@ private void initModel(SMTSolver solver) { if (solver.getType() != SolverTypes.Z3_CE_SOLVER) { return; } - if (solver.getSocket().getQuery() == null) { + AbstractSolverSocket socket = solver.getSocket(); + if (socket.getQuery() == null) { return; } - Model m = solver.getSocket().getQuery().getModel(); + Model m = socket.getQuery().getModel(); this.model = m; this.setTitle("Counterexample " + this.getTitle()); getTabbedPane().addTab("Counterexample", createModelTab()); diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/smt/ProgressDialog.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/smt/ProgressDialog.java index 338eb227509..0462a732cdc 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/smt/ProgressDialog.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/smt/ProgressDialog.java @@ -17,8 +17,7 @@ import de.uka.ilkd.key.gui.smt.ProgressModel.ProcessColumn.ProcessData; import de.uka.ilkd.key.gui.smt.ProgressTable.ProgressTableListener; import de.uka.ilkd.key.smt.SMTFocusResults; - -import org.key_project.util.java.SwingUtil; +import de.uka.ilkd.key.ui.util.SwingUtil; import org.slf4j.Logger; import org.slf4j.LoggerFactory; diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/smt/SolverListener.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/smt/SolverListener.java index c68bbc9fbeb..a1d8775b61a 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/smt/SolverListener.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/smt/SolverListener.java @@ -15,7 +15,6 @@ import java.util.Timer; import javax.swing.*; -import de.uka.ilkd.key.core.KeYMediator; import de.uka.ilkd.key.gui.MainWindow; import de.uka.ilkd.key.gui.actions.useractions.ProofSMTApplyUserAction; import de.uka.ilkd.key.gui.colors.ColorSettings; @@ -42,6 +41,7 @@ import de.uka.ilkd.key.smt.solvertypes.SolverType; import de.uka.ilkd.key.smt.solvertypes.SolverTypes; import de.uka.ilkd.key.taclettranslation.assumptions.TacletSetTranslation; +import de.uka.ilkd.key.ui.core.KeYMediator; public class SolverListener implements SolverLauncherListener { private ProgressDialog progressDialog; diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/sourceview/SourceView.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/sourceview/SourceView.java index 1ee7b710b81..c8e18db4365 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/sourceview/SourceView.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/sourceview/SourceView.java @@ -26,8 +26,6 @@ import javax.swing.text.Highlighter.HighlightPainter; import javax.swing.text.SimpleAttributeSet; -import de.uka.ilkd.key.core.KeYSelectionEvent; -import de.uka.ilkd.key.core.KeYSelectionListener; import de.uka.ilkd.key.gui.MainWindow; import de.uka.ilkd.key.gui.colors.ColorSettings; import de.uka.ilkd.key.gui.configuration.Config; @@ -49,6 +47,8 @@ import de.uka.ilkd.key.proof.ProofJavaSourceCollection; import de.uka.ilkd.key.proof.io.consistency.FileRepo; import de.uka.ilkd.key.settings.ProofIndependentSettings; +import de.uka.ilkd.key.ui.core.KeYSelectionEvent; +import de.uka.ilkd.key.ui.core.KeYSelectionListener; import org.key_project.logic.Visitor; import org.key_project.util.collection.ImmutableSet; diff --git a/key.ui/src/main/java/de/uka/ilkd/key/ui/AbstractMediatorUserInterfaceControl.java b/key.ui/src/main/java/de/uka/ilkd/key/ui/AbstractMediatorUserInterfaceControl.java index 5b547b0ca16..9c0b5618e97 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/ui/AbstractMediatorUserInterfaceControl.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/ui/AbstractMediatorUserInterfaceControl.java @@ -10,8 +10,6 @@ import de.uka.ilkd.key.control.AbstractUserInterfaceControl; import de.uka.ilkd.key.control.RuleCompletionHandler; import de.uka.ilkd.key.control.UserInterfaceControl; -import de.uka.ilkd.key.core.KeYMediator; -import de.uka.ilkd.key.core.Main; import de.uka.ilkd.key.gui.notification.events.NotificationEvent; import de.uka.ilkd.key.informationflow.macros.StartSideProofMacro; import de.uka.ilkd.key.macros.ProofMacro; @@ -24,7 +22,6 @@ import de.uka.ilkd.key.proof.init.AbstractProfile; import de.uka.ilkd.key.proof.init.InitConfig; import de.uka.ilkd.key.proof.init.ProofOblInput; -import de.uka.ilkd.key.proof.io.ProblemLoader; import de.uka.ilkd.key.proof.io.ProofSaver; import de.uka.ilkd.key.proof.mgt.ProofEnvironment; import de.uka.ilkd.key.proof.mgt.ProofEnvironmentEvent; @@ -32,9 +29,12 @@ import de.uka.ilkd.key.prover.ProverTaskListener; import de.uka.ilkd.key.prover.TaskStartedInfo; import de.uka.ilkd.key.prover.impl.DefaultTaskStartedInfo; +import de.uka.ilkd.key.ui.core.KeYMediator; +import de.uka.ilkd.key.ui.core.Main; +import de.uka.ilkd.key.ui.proof.io.ProblemLoader; +import de.uka.ilkd.key.ui.util.ThreadUtilities; import de.uka.ilkd.key.util.KeYResourceManager; import de.uka.ilkd.key.util.MiscTools; -import de.uka.ilkd.key.util.ThreadUtilities; import org.slf4j.Logger; import org.slf4j.LoggerFactory; diff --git a/key.ui/src/main/java/de/uka/ilkd/key/ui/ConsoleProofObligationSelector.java b/key.ui/src/main/java/de/uka/ilkd/key/ui/ConsoleProofObligationSelector.java index b86deb6382c..a7ac216ba6e 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/ui/ConsoleProofObligationSelector.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/ui/ConsoleProofObligationSelector.java @@ -10,7 +10,6 @@ import java.util.ArrayList; import java.util.List; -import de.uka.ilkd.key.core.KeYMediator; import de.uka.ilkd.key.proof.Proof; import de.uka.ilkd.key.proof.ProofAggregate; import de.uka.ilkd.key.proof.init.InitConfig; @@ -18,6 +17,7 @@ import de.uka.ilkd.key.proof.init.ProofInputException; import de.uka.ilkd.key.proof.init.ProofOblInput; import de.uka.ilkd.key.speclang.Contract; +import de.uka.ilkd.key.ui.core.KeYMediator; import de.uka.ilkd.key.util.KeYTypeUtil; import org.key_project.util.collection.ImmutableSet; diff --git a/key.ui/src/main/java/de/uka/ilkd/key/ui/ConsoleUserInterfaceControl.java b/key.ui/src/main/java/de/uka/ilkd/key/ui/ConsoleUserInterfaceControl.java index c0cf68fe6c7..e1027b6bb03 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/ui/ConsoleUserInterfaceControl.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/ui/ConsoleUserInterfaceControl.java @@ -11,8 +11,6 @@ import de.uka.ilkd.key.control.TermLabelVisibilityManager; import de.uka.ilkd.key.control.UserInterfaceControl; import de.uka.ilkd.key.control.instantiation_model.TacletInstantiationModel; -import de.uka.ilkd.key.core.KeYMediator; -import de.uka.ilkd.key.core.Main; import de.uka.ilkd.key.gui.actions.ShowProofStatistics; import de.uka.ilkd.key.gui.notification.events.NotificationEvent; import de.uka.ilkd.key.java.Services; @@ -30,7 +28,6 @@ import de.uka.ilkd.key.proof.init.ProblemInitializer; import de.uka.ilkd.key.proof.init.Profile; import de.uka.ilkd.key.proof.init.ProofOblInput; -import de.uka.ilkd.key.proof.io.ProblemLoader; import de.uka.ilkd.key.proof.io.ProofSaver; import de.uka.ilkd.key.prover.ProverCore; import de.uka.ilkd.key.prover.TaskFinishedInfo; @@ -39,6 +36,9 @@ import de.uka.ilkd.key.prover.impl.DefaultTaskStartedInfo; import de.uka.ilkd.key.rule.IBuiltInRuleApp; import de.uka.ilkd.key.speclang.PositionedString; +import de.uka.ilkd.key.ui.core.KeYMediator; +import de.uka.ilkd.key.ui.core.Main; +import de.uka.ilkd.key.ui.proof.io.ProblemLoader; import de.uka.ilkd.key.util.MiscTools; import org.key_project.util.collection.ImmutableList; diff --git a/key.ui/src/main/java/de/uka/ilkd/key/ui/MediatorProofControl.java b/key.ui/src/main/java/de/uka/ilkd/key/ui/MediatorProofControl.java index 54009075944..0266dc58b3b 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/ui/MediatorProofControl.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/ui/MediatorProofControl.java @@ -11,7 +11,6 @@ import de.uka.ilkd.key.control.AbstractProofControl; import de.uka.ilkd.key.control.ProofControl; -import de.uka.ilkd.key.core.KeYMediator; import de.uka.ilkd.key.gui.IssueDialog; import de.uka.ilkd.key.gui.MainWindow; import de.uka.ilkd.key.gui.ProofMacroWorker; @@ -25,6 +24,7 @@ import de.uka.ilkd.key.prover.impl.ApplyStrategyInfo; import de.uka.ilkd.key.rule.Taclet; import de.uka.ilkd.key.strategy.StrategyProperties; +import de.uka.ilkd.key.ui.core.KeYMediator; import org.key_project.util.collection.ImmutableList; diff --git a/key.ui/src/main/java/de/uka/ilkd/key/core/InterruptListener.java b/key.ui/src/main/java/de/uka/ilkd/key/ui/core/InterruptListener.java similarity index 92% rename from key.ui/src/main/java/de/uka/ilkd/key/core/InterruptListener.java rename to key.ui/src/main/java/de/uka/ilkd/key/ui/core/InterruptListener.java index 2a4b1853b9f..ca9f95ef6f0 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/core/InterruptListener.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/ui/core/InterruptListener.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.core; +package de.uka.ilkd.key.ui.core; import java.util.EventListener; diff --git a/key.ui/src/main/java/de/uka/ilkd/key/core/KeYMediator.java b/key.ui/src/main/java/de/uka/ilkd/key/ui/core/KeYMediator.java similarity index 99% rename from key.ui/src/main/java/de/uka/ilkd/key/core/KeYMediator.java rename to key.ui/src/main/java/de/uka/ilkd/key/ui/core/KeYMediator.java index d279e9f33ee..7fdcbaed032 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/core/KeYMediator.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/ui/core/KeYMediator.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.core; +package de.uka.ilkd.key.ui.core; import java.util.ArrayList; import java.util.Collection; @@ -34,7 +34,7 @@ import de.uka.ilkd.key.rule.Taclet; import de.uka.ilkd.key.settings.ProofSettings; import de.uka.ilkd.key.ui.AbstractMediatorUserInterfaceControl; -import de.uka.ilkd.key.util.ThreadUtilities; +import de.uka.ilkd.key.ui.util.ThreadUtilities; import org.key_project.proof.LocationVariableTracker; import org.key_project.util.collection.ImmutableList; diff --git a/key.ui/src/main/java/de/uka/ilkd/key/core/KeYSelectionEvent.java b/key.ui/src/main/java/de/uka/ilkd/key/ui/core/KeYSelectionEvent.java similarity index 97% rename from key.ui/src/main/java/de/uka/ilkd/key/core/KeYSelectionEvent.java rename to key.ui/src/main/java/de/uka/ilkd/key/ui/core/KeYSelectionEvent.java index 6577733f38f..58de0050cef 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/core/KeYSelectionEvent.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/ui/core/KeYSelectionEvent.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.core; +package de.uka.ilkd.key.ui.core; /** diff --git a/key.ui/src/main/java/de/uka/ilkd/key/core/KeYSelectionListener.java b/key.ui/src/main/java/de/uka/ilkd/key/ui/core/KeYSelectionListener.java similarity index 96% rename from key.ui/src/main/java/de/uka/ilkd/key/core/KeYSelectionListener.java rename to key.ui/src/main/java/de/uka/ilkd/key/ui/core/KeYSelectionListener.java index cc7514823a8..25ae73300ae 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/core/KeYSelectionListener.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/ui/core/KeYSelectionListener.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.core; +package de.uka.ilkd.key.ui.core; import de.uka.ilkd.key.proof.Node; diff --git a/key.ui/src/main/java/de/uka/ilkd/key/core/KeYSelectionModel.java b/key.ui/src/main/java/de/uka/ilkd/key/ui/core/KeYSelectionModel.java similarity index 99% rename from key.ui/src/main/java/de/uka/ilkd/key/core/KeYSelectionModel.java rename to key.ui/src/main/java/de/uka/ilkd/key/ui/core/KeYSelectionModel.java index b3a72e3f867..a49a61642d8 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/core/KeYSelectionModel.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/ui/core/KeYSelectionModel.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.core; +package de.uka.ilkd.key.ui.core; import java.util.*; diff --git a/key.ui/src/main/java/de/uka/ilkd/key/core/Log.java b/key.ui/src/main/java/de/uka/ilkd/key/ui/core/Log.java similarity index 99% rename from key.ui/src/main/java/de/uka/ilkd/key/core/Log.java rename to key.ui/src/main/java/de/uka/ilkd/key/ui/core/Log.java index 4d8d25cd644..e19e1e18e3d 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/core/Log.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/ui/core/Log.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.core; +package de.uka.ilkd.key.ui.core; import java.io.IOException; import java.nio.file.Files; diff --git a/key.ui/src/main/java/de/uka/ilkd/key/core/Main.java b/key.ui/src/main/java/de/uka/ilkd/key/ui/core/Main.java similarity index 99% rename from key.ui/src/main/java/de/uka/ilkd/key/core/Main.java rename to key.ui/src/main/java/de/uka/ilkd/key/ui/core/Main.java index f8563c3c62a..614524bc93c 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/core/Main.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/ui/core/Main.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.core; +package de.uka.ilkd.key.ui.core; import java.io.File; import java.io.IOException; @@ -31,8 +31,8 @@ import de.uka.ilkd.key.ui.AbstractMediatorUserInterfaceControl; import de.uka.ilkd.key.ui.ConsoleUserInterfaceControl; import de.uka.ilkd.key.ui.Verbosity; -import de.uka.ilkd.key.util.CommandLine; -import de.uka.ilkd.key.util.CommandLineException; +import de.uka.ilkd.key.ui.util.CommandLine; +import de.uka.ilkd.key.ui.util.CommandLineException; import de.uka.ilkd.key.util.Debug; import de.uka.ilkd.key.util.KeYConstants; import de.uka.ilkd.key.util.rifl.RIFLTransformer; diff --git a/key.ui/src/main/java/de/uka/ilkd/key/core/Watchdog.java b/key.ui/src/main/java/de/uka/ilkd/key/ui/core/Watchdog.java similarity index 98% rename from key.ui/src/main/java/de/uka/ilkd/key/core/Watchdog.java rename to key.ui/src/main/java/de/uka/ilkd/key/ui/core/Watchdog.java index 0439c08fd52..0fdb5ac97d8 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/core/Watchdog.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/ui/core/Watchdog.java @@ -1,12 +1,12 @@ /* 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.core; +package de.uka.ilkd.key.ui.core; import java.awt.*; import java.util.Set; -import de.uka.ilkd.key.util.ThreadUtilities; +import de.uka.ilkd.key.ui.util.ThreadUtilities; import org.slf4j.Logger; import org.slf4j.LoggerFactory; diff --git a/key.ui/src/main/java/de/uka/ilkd/key/proof/io/ProblemLoader.java b/key.ui/src/main/java/de/uka/ilkd/key/ui/proof/io/ProblemLoader.java similarity index 96% rename from key.ui/src/main/java/de/uka/ilkd/key/proof/io/ProblemLoader.java rename to key.ui/src/main/java/de/uka/ilkd/key/ui/proof/io/ProblemLoader.java index 1f4e9b91330..1a3a890f4cb 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/proof/io/ProblemLoader.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/ui/proof/io/ProblemLoader.java @@ -1,23 +1,25 @@ /* 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.proof.io; +package de.uka.ilkd.key.ui.proof.io; import java.io.File; import java.util.List; import java.util.Properties; import javax.swing.SwingWorker; -import de.uka.ilkd.key.core.KeYMediator; import de.uka.ilkd.key.gui.notification.events.ExceptionFailureEvent; import de.uka.ilkd.key.proof.init.InitConfig; import de.uka.ilkd.key.proof.init.Profile; +import de.uka.ilkd.key.proof.io.AbstractProblemLoader; +import de.uka.ilkd.key.proof.io.ProblemLoaderControl; import de.uka.ilkd.key.prover.ProverTaskListener; import de.uka.ilkd.key.prover.TaskFinishedInfo; import de.uka.ilkd.key.prover.TaskStartedInfo; import de.uka.ilkd.key.prover.TaskStartedInfo.TaskKind; import de.uka.ilkd.key.prover.impl.DefaultTaskFinishedInfo; import de.uka.ilkd.key.prover.impl.DefaultTaskStartedInfo; +import de.uka.ilkd.key.ui.core.KeYMediator; /** * This class extends the functionality of the {@link AbstractProblemLoader}. It allows to do the diff --git a/key.ui/src/main/java/de/uka/ilkd/key/proof/mgt/BasicTask.java b/key.ui/src/main/java/de/uka/ilkd/key/ui/proof/mgt/BasicTask.java similarity index 94% rename from key.ui/src/main/java/de/uka/ilkd/key/proof/mgt/BasicTask.java rename to key.ui/src/main/java/de/uka/ilkd/key/ui/proof/mgt/BasicTask.java index ba2680a9cf4..4e58f657fd9 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/proof/mgt/BasicTask.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/ui/proof/mgt/BasicTask.java @@ -1,13 +1,15 @@ /* 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.proof.mgt; +package de.uka.ilkd.key.ui.proof.mgt; import javax.swing.tree.DefaultMutableTreeNode; import javax.swing.tree.MutableTreeNode; import de.uka.ilkd.key.proof.Proof; import de.uka.ilkd.key.proof.ProofAggregate; +import de.uka.ilkd.key.proof.mgt.ProofEnvironment; +import de.uka.ilkd.key.proof.mgt.ProofStatus; /** diff --git a/key.ui/src/main/java/de/uka/ilkd/key/proof/mgt/EnvNode.java b/key.ui/src/main/java/de/uka/ilkd/key/ui/proof/mgt/EnvNode.java similarity index 91% rename from key.ui/src/main/java/de/uka/ilkd/key/proof/mgt/EnvNode.java rename to key.ui/src/main/java/de/uka/ilkd/key/ui/proof/mgt/EnvNode.java index bbfde9855fd..135a89f32a4 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/proof/mgt/EnvNode.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/ui/proof/mgt/EnvNode.java @@ -1,12 +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 de.uka.ilkd.key.proof.mgt; +package de.uka.ilkd.key.ui.proof.mgt; import javax.swing.tree.DefaultMutableTreeNode; import javax.swing.tree.MutableTreeNode; import de.uka.ilkd.key.proof.Proof; +import de.uka.ilkd.key.proof.mgt.ProofEnvironment; +import de.uka.ilkd.key.proof.mgt.ProofStatus; public class EnvNode extends DefaultMutableTreeNode implements TaskTreeNode { diff --git a/key.ui/src/main/java/de/uka/ilkd/key/proof/mgt/ProofAggregateTask.java b/key.ui/src/main/java/de/uka/ilkd/key/ui/proof/mgt/ProofAggregateTask.java similarity index 94% rename from key.ui/src/main/java/de/uka/ilkd/key/proof/mgt/ProofAggregateTask.java rename to key.ui/src/main/java/de/uka/ilkd/key/ui/proof/mgt/ProofAggregateTask.java index 6f336253747..280eaa923bc 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/proof/mgt/ProofAggregateTask.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/ui/proof/mgt/ProofAggregateTask.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.proof.mgt; +package de.uka.ilkd.key.ui.proof.mgt; import javax.swing.tree.DefaultMutableTreeNode; import javax.swing.tree.MutableTreeNode; @@ -9,6 +9,8 @@ import de.uka.ilkd.key.proof.Proof; import de.uka.ilkd.key.proof.ProofAggregate; import de.uka.ilkd.key.proof.SingleProof; +import de.uka.ilkd.key.proof.mgt.ProofEnvironment; +import de.uka.ilkd.key.proof.mgt.ProofStatus; public class ProofAggregateTask extends DefaultMutableTreeNode implements TaskTreeNode { diff --git a/key.ui/src/main/java/de/uka/ilkd/key/proof/mgt/TaskTreeModel.java b/key.ui/src/main/java/de/uka/ilkd/key/ui/proof/mgt/TaskTreeModel.java similarity index 97% rename from key.ui/src/main/java/de/uka/ilkd/key/proof/mgt/TaskTreeModel.java rename to key.ui/src/main/java/de/uka/ilkd/key/ui/proof/mgt/TaskTreeModel.java index 355768da45c..342c5b0311c 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/proof/mgt/TaskTreeModel.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/ui/proof/mgt/TaskTreeModel.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.proof.mgt; +package de.uka.ilkd.key.ui.proof.mgt; import java.util.LinkedHashMap; import java.util.Map; @@ -11,6 +11,7 @@ import de.uka.ilkd.key.proof.Proof; import de.uka.ilkd.key.proof.ProofAggregate; +import de.uka.ilkd.key.proof.mgt.ProofEnvironment; public class TaskTreeModel extends DefaultTreeModel { diff --git a/key.ui/src/main/java/de/uka/ilkd/key/proof/mgt/TaskTreeNode.java b/key.ui/src/main/java/de/uka/ilkd/key/ui/proof/mgt/TaskTreeNode.java similarity index 83% rename from key.ui/src/main/java/de/uka/ilkd/key/proof/mgt/TaskTreeNode.java rename to key.ui/src/main/java/de/uka/ilkd/key/ui/proof/mgt/TaskTreeNode.java index 6508357dac6..0c06c6cb08b 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/proof/mgt/TaskTreeNode.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/ui/proof/mgt/TaskTreeNode.java @@ -1,12 +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 de.uka.ilkd.key.proof.mgt; +package de.uka.ilkd.key.ui.proof.mgt; import javax.swing.tree.MutableTreeNode; import javax.swing.tree.TreeNode; import de.uka.ilkd.key.proof.Proof; +import de.uka.ilkd.key.proof.mgt.ProofEnvironment; +import de.uka.ilkd.key.proof.mgt.ProofStatus; public interface TaskTreeNode extends MutableTreeNode { diff --git a/key.ui/src/main/java/org/key_project/util/java/CheckedProcessBuilder.java b/key.ui/src/main/java/de/uka/ilkd/key/ui/util/CheckedProcessBuilder.java similarity index 98% rename from key.ui/src/main/java/org/key_project/util/java/CheckedProcessBuilder.java rename to key.ui/src/main/java/de/uka/ilkd/key/ui/util/CheckedProcessBuilder.java index 08b37eec378..b7676be260d 100644 --- a/key.ui/src/main/java/org/key_project/util/java/CheckedProcessBuilder.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/ui/util/CheckedProcessBuilder.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 org.key_project.util.java; +package de.uka.ilkd.key.ui.util; import java.io.IOException; import java.util.Arrays; diff --git a/key.ui/src/main/java/de/uka/ilkd/key/util/CommandLine.java b/key.ui/src/main/java/de/uka/ilkd/key/ui/util/CommandLine.java similarity index 99% rename from key.ui/src/main/java/de/uka/ilkd/key/util/CommandLine.java rename to key.ui/src/main/java/de/uka/ilkd/key/ui/util/CommandLine.java index a51a710d2d0..07c1f6f36f9 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/util/CommandLine.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/ui/util/CommandLine.java @@ -1,13 +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 de.uka.ilkd.key.util; +package de.uka.ilkd.key.ui.util; import java.io.File; import java.io.PrintStream; import java.util.*; -import de.uka.ilkd.key.core.Main; +import de.uka.ilkd.key.ui.core.Main; +import de.uka.ilkd.key.util.LinkedHashMap; /** * A small framework to handle command lines. diff --git a/key.ui/src/main/java/de/uka/ilkd/key/util/CommandLineException.java b/key.ui/src/main/java/de/uka/ilkd/key/ui/util/CommandLineException.java similarity index 97% rename from key.ui/src/main/java/de/uka/ilkd/key/util/CommandLineException.java rename to key.ui/src/main/java/de/uka/ilkd/key/ui/util/CommandLineException.java index 3607fee1684..720c1a4ec04 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/util/CommandLineException.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/ui/util/CommandLineException.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.util; +package de.uka.ilkd.key.ui.util; /** * Exception used by {@link CommandLine}. diff --git a/key.ui/src/main/java/de/uka/ilkd/key/util/PreferenceSaver.java b/key.ui/src/main/java/de/uka/ilkd/key/ui/util/PreferenceSaver.java similarity index 99% rename from key.ui/src/main/java/de/uka/ilkd/key/util/PreferenceSaver.java rename to key.ui/src/main/java/de/uka/ilkd/key/ui/util/PreferenceSaver.java index 6a56b8bf20c..e0dd060c4c1 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/util/PreferenceSaver.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/ui/util/PreferenceSaver.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.util; +package de.uka.ilkd.key.ui.util; import java.awt.*; import java.util.prefs.BackingStoreException; diff --git a/key.ui/src/main/java/org/key_project/util/java/SwingUtil.java b/key.ui/src/main/java/de/uka/ilkd/key/ui/util/SwingUtil.java similarity index 98% rename from key.ui/src/main/java/org/key_project/util/java/SwingUtil.java rename to key.ui/src/main/java/de/uka/ilkd/key/ui/util/SwingUtil.java index 8285a9b99da..242ef7460c8 100644 --- a/key.ui/src/main/java/org/key_project/util/java/SwingUtil.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/ui/util/SwingUtil.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 org.key_project.util.java; +package de.uka.ilkd.key.ui.util; import java.awt.*; @@ -17,7 +17,8 @@ import de.uka.ilkd.key.gui.fonticons.IconFactory; -import bibliothek.gui.dock.themes.basic.BasicDockableDisplayer; +import org.key_project.dockingframes.core.gui.dock.themes.basic.BasicDockableDisplayer; + import org.slf4j.Logger; import org.slf4j.LoggerFactory; diff --git a/key.ui/src/main/java/de/uka/ilkd/key/util/ThreadUtilities.java b/key.ui/src/main/java/de/uka/ilkd/key/ui/util/ThreadUtilities.java similarity index 98% rename from key.ui/src/main/java/de/uka/ilkd/key/util/ThreadUtilities.java rename to key.ui/src/main/java/de/uka/ilkd/key/ui/util/ThreadUtilities.java index 2588529aefd..631c1f7ab30 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/util/ThreadUtilities.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/ui/util/ThreadUtilities.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.util; +package de.uka.ilkd.key.ui.util; import java.awt.EventQueue; import java.lang.reflect.InvocationTargetException; diff --git a/key.ui/src/main/java/de/uka/ilkd/key/util/XMLResources.java b/key.ui/src/main/java/de/uka/ilkd/key/ui/util/XMLResources.java similarity index 98% rename from key.ui/src/main/java/de/uka/ilkd/key/util/XMLResources.java rename to key.ui/src/main/java/de/uka/ilkd/key/ui/util/XMLResources.java index 3c50b745530..9ad1a7981fd 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/util/XMLResources.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/ui/util/XMLResources.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.util; +package de.uka.ilkd.key.ui.util; import java.io.FileNotFoundException; import java.io.IOException; diff --git a/key.ui/src/main/java/module-info.java b/key.ui/src/main/java/module-info.java new file mode 100644 index 00000000000..9cc8a6495f9 --- /dev/null +++ b/key.ui/src/main/java/module-info.java @@ -0,0 +1,53 @@ +/** + * + * @author Alexander Weigl + * @version 1 (31.03.24) + */ +module org.key_project.ui { + exports de.uka.ilkd.key.gui.extension.api; + exports de.uka.ilkd.key.gui.help; + exports de.uka.ilkd.key.ui.core; + exports de.uka.ilkd.key.gui; + exports de.uka.ilkd.key.gui.settings; + exports de.uka.ilkd.key.gui.colors; + exports de.uka.ilkd.key.ui.util; + exports de.uka.ilkd.key.gui.actions; + exports de.uka.ilkd.key.gui.fonticons; + exports de.uka.ilkd.key.gui.prooftree; + exports de.uka.ilkd.key.gui.configuration; + exports de.uka.ilkd.key.gui.smt; + exports de.uka.ilkd.key.gui.keyshortcuts; + exports de.uka.ilkd.key.ui; + exports de.uka.ilkd.key.ui.proof.io; + + requires dockingframes.core; + requires dockingframes.common; + + requires org.slf4j; + requires java.desktop; + requires org.key_project.core; + requires java.prefs; + requires org.jspecify; + requires org.key_project.util; + requires org.key_project.ncore; + requires com.miglayout.core; + requires com.miglayout.swing; + requires ch.qos.logback.core; + requires ch.qos.logback.classic; + requires key.recoder; + requires org.key_project.core.rifl; + requires java.compiler; + + provides de.uka.ilkd.key.gui.extension.api.KeYGuiExtension with + de.uka.ilkd.key.gui.originlabels.OriginTermLabelsExt, + de.uka.ilkd.key.gui.extension.impl.HeatmapExt, + de.uka.ilkd.key.gui.extension.impl.TestExtension, + de.uka.ilkd.key.gui.docking.DockingLayout, + de.uka.ilkd.key.gui.KeyboardTacletExtension, + de.uka.ilkd.key.gui.nodeviews.ShowHashcodesExtension, + de.uka.ilkd.key.gui.LogView, + de.uka.ilkd.key.gui.plugins.javac.JavacExtension, + de.uka.ilkd.key.gui.utilities.HeapStatusExt, + de.uka.ilkd.key.gui.JmlEnabledKeysIndicator; + +} \ No newline at end of file diff --git a/key.ui/src/main/resources/META-INF/services/de.uka.ilkd.key.gui.extension.api.KeYGuiExtension b/key.ui/src/main/resources/META-INF/services/de.uka.ilkd.key.gui.extension.api.KeYGuiExtension index 99b38233d0c..8cb35eaba56 100644 --- a/key.ui/src/main/resources/META-INF/services/de.uka.ilkd.key.gui.extension.api.KeYGuiExtension +++ b/key.ui/src/main/resources/META-INF/services/de.uka.ilkd.key.gui.extension.api.KeYGuiExtension @@ -6,6 +6,5 @@ de.uka.ilkd.key.gui.KeyboardTacletExtension de.uka.ilkd.key.gui.nodeviews.ShowHashcodesExtension de.uka.ilkd.key.gui.LogView de.uka.ilkd.key.gui.plugins.javac.JavacExtension -de.uka.ilkd.key.gui.plugins.caching.CachingExtension de.uka.ilkd.key.gui.utilities.HeapStatusExt de.uka.ilkd.key.gui.JmlEnabledKeysIndicator \ No newline at end of file diff --git a/key.ui/src/test/java/de/uka/ilkd/key/gui/ChaosMonkey.java b/key.ui/src/test/java/de/uka/ilkd/key/gui/ChaosMonkey.java index fad4e66973a..0f00103f233 100644 --- a/key.ui/src/test/java/de/uka/ilkd/key/gui/ChaosMonkey.java +++ b/key.ui/src/test/java/de/uka/ilkd/key/gui/ChaosMonkey.java @@ -13,17 +13,17 @@ import java.util.stream.Collectors; import javax.swing.*; -import de.uka.ilkd.key.core.KeYMediator; -import de.uka.ilkd.key.core.Main; import de.uka.ilkd.key.gui.actions.EditMostRecentFileAction; import de.uka.ilkd.key.gui.actions.KeYProjectHomepageAction; import de.uka.ilkd.key.gui.actions.LemmaGenerationAction; import de.uka.ilkd.key.gui.keyshortcuts.KeyStrokeManager; import de.uka.ilkd.key.settings.ProofIndependentSettings; +import de.uka.ilkd.key.ui.core.KeYMediator; +import de.uka.ilkd.key.ui.core.Main; +import de.uka.ilkd.key.ui.util.SwingUtil; -import org.key_project.util.java.SwingUtil; +import org.key_project.dockingframes.core.gui.dock.dockable.AbstractDockable; -import bibliothek.gui.dock.dockable.AbstractDockable; import org.junit.jupiter.api.*; import org.slf4j.Logger; import org.slf4j.LoggerFactory; diff --git a/keyext.caching/src/main/java/de/uka/ilkd/key/gui/plugins/caching/CachingExtension.java b/keyext.caching/src/main/java/de/uka/ilkd/key/gui/plugins/caching/CachingExtension.java index c0f7f1d813c..5e1b3e7c3e2 100644 --- a/keyext.caching/src/main/java/de/uka/ilkd/key/gui/plugins/caching/CachingExtension.java +++ b/keyext.caching/src/main/java/de/uka/ilkd/key/gui/plugins/caching/CachingExtension.java @@ -9,9 +9,6 @@ import java.util.Set; import javax.swing.*; -import de.uka.ilkd.key.core.KeYMediator; -import de.uka.ilkd.key.core.KeYSelectionEvent; -import de.uka.ilkd.key.core.KeYSelectionListener; import de.uka.ilkd.key.gui.MainWindow; import de.uka.ilkd.key.gui.extension.api.ContextMenuKind; import de.uka.ilkd.key.gui.extension.api.KeYGuiExtension; @@ -36,12 +33,14 @@ import de.uka.ilkd.key.proof.event.ProofDisposedListener; import de.uka.ilkd.key.proof.reference.ClosedBy; import de.uka.ilkd.key.proof.reference.CopyReferenceResolver; -import de.uka.ilkd.key.proof.reference.ReferenceSearcher; import de.uka.ilkd.key.proof.replay.CopyingProofReplayer; import de.uka.ilkd.key.prover.ProverTaskListener; import de.uka.ilkd.key.prover.TaskFinishedInfo; import de.uka.ilkd.key.prover.TaskStartedInfo; import de.uka.ilkd.key.prover.impl.ApplyStrategy; +import de.uka.ilkd.key.ui.core.KeYMediator; +import de.uka.ilkd.key.ui.core.KeYSelectionEvent; +import de.uka.ilkd.key.ui.core.KeYSelectionListener; import org.key_project.util.collection.ImmutableList; diff --git a/keyext.caching/src/main/java/de/uka/ilkd/key/gui/plugins/caching/CachingPruneHandler.java b/keyext.caching/src/main/java/de/uka/ilkd/key/gui/plugins/caching/CachingPruneHandler.java index ef4cc2c269e..c5ba97d8abc 100644 --- a/keyext.caching/src/main/java/de/uka/ilkd/key/gui/plugins/caching/CachingPruneHandler.java +++ b/keyext.caching/src/main/java/de/uka/ilkd/key/gui/plugins/caching/CachingPruneHandler.java @@ -3,7 +3,6 @@ * SPDX-License-Identifier: GPL-2.0-only */ package de.uka.ilkd.key.gui.plugins.caching; -import de.uka.ilkd.key.core.KeYMediator; import de.uka.ilkd.key.gui.IssueDialog; import de.uka.ilkd.key.gui.MainWindow; import de.uka.ilkd.key.gui.plugins.caching.settings.CachingSettingsProvider; @@ -15,6 +14,7 @@ import de.uka.ilkd.key.proof.io.IntermediateProofReplayer; import de.uka.ilkd.key.proof.reference.ClosedBy; import de.uka.ilkd.key.proof.replay.CopyingProofReplayer; +import de.uka.ilkd.key.ui.core.KeYMediator; import org.slf4j.Logger; import org.slf4j.LoggerFactory; diff --git a/keyext.caching/src/main/java/de/uka/ilkd/key/gui/plugins/caching/DefaultReferenceSearchDialogListener.java b/keyext.caching/src/main/java/de/uka/ilkd/key/gui/plugins/caching/DefaultReferenceSearchDialogListener.java index 60324f307f3..827b6f3f325 100644 --- a/keyext.caching/src/main/java/de/uka/ilkd/key/gui/plugins/caching/DefaultReferenceSearchDialogListener.java +++ b/keyext.caching/src/main/java/de/uka/ilkd/key/gui/plugins/caching/DefaultReferenceSearchDialogListener.java @@ -6,12 +6,12 @@ import java.util.function.Consumer; import javax.swing.*; -import de.uka.ilkd.key.core.KeYMediator; import de.uka.ilkd.key.gui.IssueDialog; import de.uka.ilkd.key.gui.MainWindow; import de.uka.ilkd.key.gui.actions.ShowProofStatistics; import de.uka.ilkd.key.proof.Proof; import de.uka.ilkd.key.proof.reference.CopyReferenceResolver; +import de.uka.ilkd.key.ui.core.KeYMediator; import org.slf4j.Logger; import org.slf4j.LoggerFactory; diff --git a/keyext.caching/src/main/java/de/uka/ilkd/key/proof/reference/ProgramMethodFinder.java b/keyext.caching/src/main/java/de/uka/ilkd/key/gui/plugins/caching/ProgramMethodFinder.java similarity index 96% rename from keyext.caching/src/main/java/de/uka/ilkd/key/proof/reference/ProgramMethodFinder.java rename to keyext.caching/src/main/java/de/uka/ilkd/key/gui/plugins/caching/ProgramMethodFinder.java index 44ad71b7bf4..9796db4711d 100644 --- a/keyext.caching/src/main/java/de/uka/ilkd/key/proof/reference/ProgramMethodFinder.java +++ b/keyext.caching/src/main/java/de/uka/ilkd/key/gui/plugins/caching/ProgramMethodFinder.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.proof.reference; +package de.uka.ilkd.key.gui.plugins.caching; import de.uka.ilkd.key.logic.Term; import de.uka.ilkd.key.logic.op.ProgramMethod; diff --git a/keyext.caching/src/main/java/de/uka/ilkd/key/gui/plugins/caching/ReferenceSearchButton.java b/keyext.caching/src/main/java/de/uka/ilkd/key/gui/plugins/caching/ReferenceSearchButton.java index dec2bab3847..afa2d74d512 100644 --- a/keyext.caching/src/main/java/de/uka/ilkd/key/gui/plugins/caching/ReferenceSearchButton.java +++ b/keyext.caching/src/main/java/de/uka/ilkd/key/gui/plugins/caching/ReferenceSearchButton.java @@ -8,14 +8,13 @@ import java.awt.event.ActionListener; import javax.swing.*; -import de.uka.ilkd.key.core.KeYMediator; -import de.uka.ilkd.key.core.KeYSelectionEvent; -import de.uka.ilkd.key.core.KeYSelectionListener; import de.uka.ilkd.key.gui.colors.ColorSettings; import de.uka.ilkd.key.proof.Goal; import de.uka.ilkd.key.proof.Proof; import de.uka.ilkd.key.proof.reference.ClosedBy; -import de.uka.ilkd.key.proof.reference.ReferenceSearcher; +import de.uka.ilkd.key.ui.core.KeYMediator; +import de.uka.ilkd.key.ui.core.KeYSelectionEvent; +import de.uka.ilkd.key.ui.core.KeYSelectionListener; /** * Status line button to indicate whether cached goals are present. diff --git a/keyext.caching/src/main/java/de/uka/ilkd/key/gui/plugins/caching/ReferenceSearchDialog.java b/keyext.caching/src/main/java/de/uka/ilkd/key/gui/plugins/caching/ReferenceSearchDialog.java index 591367ebced..d805e28bf8f 100644 --- a/keyext.caching/src/main/java/de/uka/ilkd/key/gui/plugins/caching/ReferenceSearchDialog.java +++ b/keyext.caching/src/main/java/de/uka/ilkd/key/gui/plugins/caching/ReferenceSearchDialog.java @@ -10,8 +10,7 @@ import de.uka.ilkd.key.gui.MainWindow; import de.uka.ilkd.key.proof.Proof; import de.uka.ilkd.key.proof.reference.ClosedBy; - -import org.key_project.util.java.SwingUtil; +import de.uka.ilkd.key.ui.util.SwingUtil; import org.slf4j.Logger; import org.slf4j.LoggerFactory; diff --git a/keyext.caching/src/main/java/de/uka/ilkd/key/gui/plugins/caching/ReferenceSearchTable.java b/keyext.caching/src/main/java/de/uka/ilkd/key/gui/plugins/caching/ReferenceSearchTable.java index 645a539f746..721458c72b0 100644 --- a/keyext.caching/src/main/java/de/uka/ilkd/key/gui/plugins/caching/ReferenceSearchTable.java +++ b/keyext.caching/src/main/java/de/uka/ilkd/key/gui/plugins/caching/ReferenceSearchTable.java @@ -12,10 +12,10 @@ import javax.swing.event.TableModelListener; import javax.swing.table.TableModel; -import de.uka.ilkd.key.core.KeYMediator; import de.uka.ilkd.key.proof.Goal; import de.uka.ilkd.key.proof.Proof; import de.uka.ilkd.key.proof.reference.ClosedBy; +import de.uka.ilkd.key.ui.core.KeYMediator; /** * Table showing the results of searching for proof references. diff --git a/keyext.caching/src/main/java/de/uka/ilkd/key/proof/reference/ReferenceSearcher.java b/keyext.caching/src/main/java/de/uka/ilkd/key/gui/plugins/caching/ReferenceSearcher.java similarity index 98% rename from keyext.caching/src/main/java/de/uka/ilkd/key/proof/reference/ReferenceSearcher.java rename to keyext.caching/src/main/java/de/uka/ilkd/key/gui/plugins/caching/ReferenceSearcher.java index 14b5265c330..37f67abc126 100644 --- a/keyext.caching/src/main/java/de/uka/ilkd/key/proof/reference/ReferenceSearcher.java +++ b/keyext.caching/src/main/java/de/uka/ilkd/key/gui/plugins/caching/ReferenceSearcher.java @@ -1,11 +1,10 @@ /* 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.proof.reference; +package de.uka.ilkd.key.gui.plugins.caching; import java.util.*; import java.util.stream.Collectors; -import javax.swing.*; import de.uka.ilkd.key.logic.Semisequent; import de.uka.ilkd.key.logic.Sequent; @@ -13,6 +12,7 @@ import de.uka.ilkd.key.logic.Term; import de.uka.ilkd.key.proof.Node; import de.uka.ilkd.key.proof.Proof; +import de.uka.ilkd.key.proof.reference.ClosedBy; import de.uka.ilkd.key.rule.NoPosTacletApp; import de.uka.ilkd.key.rule.merge.CloseAfterMerge; diff --git a/keyext.caching/src/main/java/de/uka/ilkd/key/gui/plugins/caching/actions/CloseAllByReference.java b/keyext.caching/src/main/java/de/uka/ilkd/key/gui/plugins/caching/actions/CloseAllByReference.java index b2232ecaafe..23c97cf2e2e 100644 --- a/keyext.caching/src/main/java/de/uka/ilkd/key/gui/plugins/caching/actions/CloseAllByReference.java +++ b/keyext.caching/src/main/java/de/uka/ilkd/key/gui/plugins/caching/actions/CloseAllByReference.java @@ -8,14 +8,14 @@ import java.util.List; import javax.swing.*; -import de.uka.ilkd.key.core.KeYMediator; import de.uka.ilkd.key.gui.MainWindow; import de.uka.ilkd.key.gui.actions.KeyAction; import de.uka.ilkd.key.gui.plugins.caching.CachingExtension; +import de.uka.ilkd.key.gui.plugins.caching.ReferenceSearcher; import de.uka.ilkd.key.proof.Node; import de.uka.ilkd.key.proof.Proof; import de.uka.ilkd.key.proof.reference.ClosedBy; -import de.uka.ilkd.key.proof.reference.ReferenceSearcher; +import de.uka.ilkd.key.ui.core.KeYMediator; /** * Proof context menu action to perform proof caching for all open goals on that proof. diff --git a/keyext.caching/src/main/java/de/uka/ilkd/key/gui/plugins/caching/actions/CloseByReference.java b/keyext.caching/src/main/java/de/uka/ilkd/key/gui/plugins/caching/actions/CloseByReference.java index 7dcafc483f2..6e523373061 100644 --- a/keyext.caching/src/main/java/de/uka/ilkd/key/gui/plugins/caching/actions/CloseByReference.java +++ b/keyext.caching/src/main/java/de/uka/ilkd/key/gui/plugins/caching/actions/CloseByReference.java @@ -9,13 +9,13 @@ import java.util.List; import javax.swing.*; -import de.uka.ilkd.key.core.KeYMediator; import de.uka.ilkd.key.gui.MainWindow; import de.uka.ilkd.key.gui.actions.KeyAction; import de.uka.ilkd.key.gui.plugins.caching.CachingExtension; +import de.uka.ilkd.key.gui.plugins.caching.ReferenceSearcher; import de.uka.ilkd.key.proof.Node; import de.uka.ilkd.key.proof.reference.ClosedBy; -import de.uka.ilkd.key.proof.reference.ReferenceSearcher; +import de.uka.ilkd.key.ui.core.KeYMediator; /** * Action to search for suitable references on a single node. diff --git a/keyext.caching/src/main/java/de/uka/ilkd/key/gui/plugins/caching/actions/CopyReferencedProof.java b/keyext.caching/src/main/java/de/uka/ilkd/key/gui/plugins/caching/actions/CopyReferencedProof.java index cd818b55d8c..b7b13bdab21 100644 --- a/keyext.caching/src/main/java/de/uka/ilkd/key/gui/plugins/caching/actions/CopyReferencedProof.java +++ b/keyext.caching/src/main/java/de/uka/ilkd/key/gui/plugins/caching/actions/CopyReferencedProof.java @@ -5,7 +5,6 @@ import java.awt.event.ActionEvent; -import de.uka.ilkd.key.core.KeYMediator; import de.uka.ilkd.key.gui.IssueDialog; import de.uka.ilkd.key.gui.MainWindow; import de.uka.ilkd.key.gui.actions.KeyAction; @@ -13,6 +12,7 @@ import de.uka.ilkd.key.proof.Node; import de.uka.ilkd.key.proof.reference.ClosedBy; import de.uka.ilkd.key.proof.replay.CopyingProofReplayer; +import de.uka.ilkd.key.ui.core.KeYMediator; import org.slf4j.Logger; import org.slf4j.LoggerFactory; diff --git a/keyext.caching/src/main/java/de/uka/ilkd/key/gui/plugins/caching/actions/GotoReferenceAction.java b/keyext.caching/src/main/java/de/uka/ilkd/key/gui/plugins/caching/actions/GotoReferenceAction.java index 234749e63e6..2106c6a69af 100644 --- a/keyext.caching/src/main/java/de/uka/ilkd/key/gui/plugins/caching/actions/GotoReferenceAction.java +++ b/keyext.caching/src/main/java/de/uka/ilkd/key/gui/plugins/caching/actions/GotoReferenceAction.java @@ -5,10 +5,10 @@ import java.awt.event.ActionEvent; -import de.uka.ilkd.key.core.KeYMediator; import de.uka.ilkd.key.gui.actions.KeyAction; import de.uka.ilkd.key.proof.Node; import de.uka.ilkd.key.proof.reference.ClosedBy; +import de.uka.ilkd.key.ui.core.KeYMediator; /** * Action to go the referenced proof. diff --git a/keyext.caching/src/main/java/de/uka/ilkd/key/gui/plugins/caching/actions/RemoveCachingInformationAction.java b/keyext.caching/src/main/java/de/uka/ilkd/key/gui/plugins/caching/actions/RemoveCachingInformationAction.java index 7037248ea28..922442ad3ad 100644 --- a/keyext.caching/src/main/java/de/uka/ilkd/key/gui/plugins/caching/actions/RemoveCachingInformationAction.java +++ b/keyext.caching/src/main/java/de/uka/ilkd/key/gui/plugins/caching/actions/RemoveCachingInformationAction.java @@ -5,10 +5,10 @@ import java.awt.event.ActionEvent; -import de.uka.ilkd.key.core.KeYMediator; import de.uka.ilkd.key.gui.actions.KeyAction; import de.uka.ilkd.key.proof.Node; import de.uka.ilkd.key.proof.reference.ClosedBy; +import de.uka.ilkd.key.ui.core.KeYMediator; /** * Action to remove caching information on a goal closed by caching. diff --git a/keyext.caching/src/main/java/module-info.java b/keyext.caching/src/main/java/module-info.java new file mode 100644 index 00000000000..d2c0c0462bf --- /dev/null +++ b/keyext.caching/src/main/java/module-info.java @@ -0,0 +1,11 @@ +import de.uka.ilkd.key.gui.extension.api.KeYGuiExtension; +import de.uka.ilkd.key.gui.plugins.caching.CachingExtension; + +/** + * + * @author Alexander Weigl + * @version 1 (31.03.24) + */ +module keyext.caching{requires org.key_project.ui;requires org.key_project.core;requires org.slf4j;requires org.jspecify;requires java.desktop;requires org.key_project.util;requires org.key_project.ncore;requires keyext.slicing;requires com.miglayout.core; + +provides KeYGuiExtension with CachingExtension;} diff --git a/keyext.caching/src/test/java/de/uka/ilkd/key/proof/reference/TestReferenceSearcher.java b/keyext.caching/src/test/java/de/uka/ilkd/key/proof/reference/TestReferenceSearcher.java index 047eb9b2e2f..9ff6b4b8806 100644 --- a/keyext.caching/src/test/java/de/uka/ilkd/key/proof/reference/TestReferenceSearcher.java +++ b/keyext.caching/src/test/java/de/uka/ilkd/key/proof/reference/TestReferenceSearcher.java @@ -9,6 +9,7 @@ import de.uka.ilkd.key.control.DefaultUserInterfaceControl; import de.uka.ilkd.key.control.KeYEnvironment; +import de.uka.ilkd.key.gui.plugins.caching.ReferenceSearcher; import de.uka.ilkd.key.proof.Goal; import de.uka.ilkd.key.proof.Node; import de.uka.ilkd.key.proof.Proof; diff --git a/keyext.exploration/src/main/java/module-info.java b/keyext.exploration/src/main/java/module-info.java new file mode 100644 index 00000000000..322ba9b2bfd --- /dev/null +++ b/keyext.exploration/src/main/java/module-info.java @@ -0,0 +1,10 @@ +import de.uka.ilkd.key.gui.extension.api.KeYGuiExtension; + +/** + * + * @author Alexander Weigl + * @version 1 (31.03.24) + */ +module keyext.exploration{requires transitive org.key_project.ui;requires org.key_project.core;requires org.jspecify;requires java.desktop;requires org.key_project.ncore;requires org.key_project.util;requires dockingframes.common; + +provides KeYGuiExtension with org.key_project.exploration.ExplorationExtension;} diff --git a/keyext.exploration/src/main/java/org/key_project/exploration/ExplorationExtension.java b/keyext.exploration/src/main/java/org/key_project/exploration/ExplorationExtension.java index 0ea1280b2bb..a33ae2e827d 100644 --- a/keyext.exploration/src/main/java/org/key_project/exploration/ExplorationExtension.java +++ b/keyext.exploration/src/main/java/org/key_project/exploration/ExplorationExtension.java @@ -10,9 +10,6 @@ import java.util.List; import javax.swing.*; -import de.uka.ilkd.key.core.KeYMediator; -import de.uka.ilkd.key.core.KeYSelectionEvent; -import de.uka.ilkd.key.core.KeYSelectionListener; import de.uka.ilkd.key.gui.MainWindow; import de.uka.ilkd.key.gui.colors.ColorSettings; import de.uka.ilkd.key.gui.extension.api.ContextMenuAdapter; @@ -30,6 +27,9 @@ import de.uka.ilkd.key.proof.ProofTreeListener; import de.uka.ilkd.key.proof.event.ProofDisposedEvent; import de.uka.ilkd.key.proof.event.ProofDisposedListener; +import de.uka.ilkd.key.ui.core.KeYMediator; +import de.uka.ilkd.key.ui.core.KeYSelectionEvent; +import de.uka.ilkd.key.ui.core.KeYSelectionListener; import org.key_project.exploration.actions.*; import org.key_project.exploration.ui.ExplorationStepsList; diff --git a/keyext.exploration/src/main/java/org/key_project/exploration/ExplorationModeModel.java b/keyext.exploration/src/main/java/org/key_project/exploration/ExplorationModeModel.java index 3ef79c2ff5c..10e9694646d 100644 --- a/keyext.exploration/src/main/java/org/key_project/exploration/ExplorationModeModel.java +++ b/keyext.exploration/src/main/java/org/key_project/exploration/ExplorationModeModel.java @@ -14,6 +14,7 @@ import de.uka.ilkd.key.gui.prooftree.ProofTreeViewFilter; import de.uka.ilkd.key.proof.Proof; import de.uka.ilkd.key.settings.ProofIndependentSettings; +import de.uka.ilkd.key.ui.core.KeYMediator; import org.jspecify.annotations.NonNull; @@ -22,7 +23,7 @@ *

* This class holds the data and the state of proof exploration. *

- * For every {@link de.uka.ilkd.key.core.KeYMediator} or {@link MainWindow} should only exists one + * For every {@link KeYMediator} or {@link MainWindow} should only exists one * instance. * * @see ExplorationExtension diff --git a/keyext.exploration/src/main/java/org/key_project/exploration/ProofExplorationService.java b/keyext.exploration/src/main/java/org/key_project/exploration/ProofExplorationService.java index 310148a5efd..865cfe53157 100644 --- a/keyext.exploration/src/main/java/org/key_project/exploration/ProofExplorationService.java +++ b/keyext.exploration/src/main/java/org/key_project/exploration/ProofExplorationService.java @@ -5,7 +5,6 @@ import java.util.Objects; -import de.uka.ilkd.key.core.KeYMediator; import de.uka.ilkd.key.java.Services; import de.uka.ilkd.key.logic.*; import de.uka.ilkd.key.logic.op.SchemaVariable; @@ -14,6 +13,7 @@ import de.uka.ilkd.key.proof.Node; import de.uka.ilkd.key.proof.Proof; import de.uka.ilkd.key.rule.*; +import de.uka.ilkd.key.ui.core.KeYMediator; import org.key_project.logic.Name; import org.key_project.util.collection.ImmutableList; diff --git a/keyext.exploration/src/main/java/org/key_project/exploration/actions/ToggleExplorationAction.java b/keyext.exploration/src/main/java/org/key_project/exploration/actions/ToggleExplorationAction.java index e46442f4f2e..3a8c6a86105 100644 --- a/keyext.exploration/src/main/java/org/key_project/exploration/actions/ToggleExplorationAction.java +++ b/keyext.exploration/src/main/java/org/key_project/exploration/actions/ToggleExplorationAction.java @@ -5,10 +5,10 @@ import java.awt.event.ActionEvent; -import de.uka.ilkd.key.core.KeYSelectionEvent; -import de.uka.ilkd.key.core.KeYSelectionListener; import de.uka.ilkd.key.gui.MainWindow; import de.uka.ilkd.key.gui.actions.KeyAction; +import de.uka.ilkd.key.ui.core.KeYSelectionEvent; +import de.uka.ilkd.key.ui.core.KeYSelectionListener; import org.key_project.exploration.ExplorationModeModel; import org.key_project.exploration.Icons; diff --git a/keyext.exploration/src/main/java/org/key_project/exploration/ui/ExplorationStepsList.java b/keyext.exploration/src/main/java/org/key_project/exploration/ui/ExplorationStepsList.java index cfc68cf0b41..e6aa07e9bfd 100644 --- a/keyext.exploration/src/main/java/org/key_project/exploration/ui/ExplorationStepsList.java +++ b/keyext.exploration/src/main/java/org/key_project/exploration/ui/ExplorationStepsList.java @@ -10,7 +10,6 @@ import javax.swing.*; import javax.swing.tree.*; -import de.uka.ilkd.key.core.KeYMediator; import de.uka.ilkd.key.gui.MainWindow; import de.uka.ilkd.key.gui.actions.KeyAction; import de.uka.ilkd.key.gui.extension.api.TabPanel; @@ -19,11 +18,12 @@ import de.uka.ilkd.key.proof.Node; import de.uka.ilkd.key.proof.Proof; import de.uka.ilkd.key.proof.RuleAppListener; +import de.uka.ilkd.key.ui.core.KeYMediator; +import org.key_project.dockingframes.common.common.action.CAction; import org.key_project.exploration.ExplorationNodeData; import org.key_project.exploration.Icons; -import bibliothek.gui.dock.common.action.CAction; import org.jspecify.annotations.NonNull; import org.jspecify.annotations.Nullable; diff --git a/keyext.proofmanagement/src/main/java/module-info.java b/keyext.proofmanagement/src/main/java/module-info.java new file mode 100644 index 00000000000..974ce1e0f1a --- /dev/null +++ b/keyext.proofmanagement/src/main/java/module-info.java @@ -0,0 +1,12 @@ +import de.uka.ilkd.key.gui.extension.api.KeYGuiExtension; + +/** + * + * @author Alexander Weigl + * @version 1 (31.03.24) + */ +module keyext.proofmanagement{requires org.key_project.ui;requires org.jspecify;requires java.desktop;requires org.slf4j;requires org.key_project.core;requires org.key_project.util;requires org.key_project.ncore; +/* not available requires ST4; */ + + +provides KeYGuiExtension with org.key_project.proofmanagement.ProofManagementExt;} diff --git a/keyext.proofmanagement/src/main/java/org/key_project/proofmanagement/Main.java b/keyext.proofmanagement/src/main/java/org/key_project/proofmanagement/Main.java index 6745745cbc2..31ed6dbabeb 100644 --- a/keyext.proofmanagement/src/main/java/org/key_project/proofmanagement/Main.java +++ b/keyext.proofmanagement/src/main/java/org/key_project/proofmanagement/Main.java @@ -11,8 +11,8 @@ import java.util.List; import java.util.ResourceBundle; -import de.uka.ilkd.key.util.CommandLine; -import de.uka.ilkd.key.util.CommandLineException; +import de.uka.ilkd.key.ui.util.CommandLine; +import de.uka.ilkd.key.ui.util.CommandLineException; import org.key_project.proofmanagement.check.*; import org.key_project.proofmanagement.io.HTMLReport; diff --git a/keyext.slicing/src/main/java/module-info.java b/keyext.slicing/src/main/java/module-info.java new file mode 100644 index 00000000000..e27dea16fb9 --- /dev/null +++ b/keyext.slicing/src/main/java/module-info.java @@ -0,0 +1,10 @@ +import de.uka.ilkd.key.gui.extension.api.KeYGuiExtension; + +/** + * + * @author Alexander Weigl + * @version 1 (31.03.24) + */ +module keyext.slicing{requires org.key_project.core;requires org.key_project.ui;requires java.desktop;requires org.jspecify;requires org.slf4j;requires com.miglayout.core;requires org.key_project.util;requires org.key_project.ncore;requires dockingframes.common;requires dockingframes.core;exports org.key_project.slicing;exports org.key_project.slicing.analysis; + +provides KeYGuiExtension with org.key_project.slicing.SlicingExtension;} diff --git a/keyext.slicing/src/main/java/org/key_project/slicing/Main.java b/keyext.slicing/src/main/java/org/key_project/slicing/Main.java index a7cc16eee48..925241a626c 100644 --- a/keyext.slicing/src/main/java/org/key_project/slicing/Main.java +++ b/keyext.slicing/src/main/java/org/key_project/slicing/Main.java @@ -12,13 +12,13 @@ import de.uka.ilkd.key.control.DefaultUserInterfaceControl; import de.uka.ilkd.key.control.KeYEnvironment; -import de.uka.ilkd.key.core.Log; import de.uka.ilkd.key.proof.Proof; import de.uka.ilkd.key.proof.init.JavaProfile; import de.uka.ilkd.key.proof.io.ProblemLoaderControl; import de.uka.ilkd.key.settings.GeneralSettings; -import de.uka.ilkd.key.util.CommandLine; -import de.uka.ilkd.key.util.CommandLineException; +import de.uka.ilkd.key.ui.core.Log; +import de.uka.ilkd.key.ui.util.CommandLine; +import de.uka.ilkd.key.ui.util.CommandLineException; import org.key_project.slicing.analysis.AnalysisResults; diff --git a/keyext.slicing/src/main/java/org/key_project/slicing/SlicingExtension.java b/keyext.slicing/src/main/java/org/key_project/slicing/SlicingExtension.java index 13b32c6c07f..59c150fb291 100644 --- a/keyext.slicing/src/main/java/org/key_project/slicing/SlicingExtension.java +++ b/keyext.slicing/src/main/java/org/key_project/slicing/SlicingExtension.java @@ -11,9 +11,6 @@ import java.util.Map; import javax.swing.*; -import de.uka.ilkd.key.core.KeYMediator; -import de.uka.ilkd.key.core.KeYSelectionEvent; -import de.uka.ilkd.key.core.KeYSelectionListener; import de.uka.ilkd.key.gui.MainWindow; import de.uka.ilkd.key.gui.extension.api.ContextMenuAdapter; import de.uka.ilkd.key.gui.extension.api.ContextMenuKind; @@ -27,6 +24,9 @@ import de.uka.ilkd.key.proof.Proof; import de.uka.ilkd.key.proof.event.ProofDisposedEvent; import de.uka.ilkd.key.proof.event.ProofDisposedListener; +import de.uka.ilkd.key.ui.core.KeYMediator; +import de.uka.ilkd.key.ui.core.KeYSelectionEvent; +import de.uka.ilkd.key.ui.core.KeYSelectionListener; import org.key_project.slicing.graph.GraphNode; import org.key_project.slicing.ui.ShowCreatedByAction; diff --git a/keyext.slicing/src/main/java/org/key_project/slicing/ui/SliceToFixedPointDialog.java b/keyext.slicing/src/main/java/org/key_project/slicing/ui/SliceToFixedPointDialog.java index 75b673c64a1..33174898a4b 100644 --- a/keyext.slicing/src/main/java/org/key_project/slicing/ui/SliceToFixedPointDialog.java +++ b/keyext.slicing/src/main/java/org/key_project/slicing/ui/SliceToFixedPointDialog.java @@ -18,13 +18,13 @@ import java.util.stream.Collectors; import javax.swing.*; -import de.uka.ilkd.key.core.KeYMediator; -import de.uka.ilkd.key.core.KeYSelectionEvent; -import de.uka.ilkd.key.core.KeYSelectionListener; import de.uka.ilkd.key.gui.MainWindow; import de.uka.ilkd.key.gui.configuration.Config; import de.uka.ilkd.key.proof.Node; import de.uka.ilkd.key.proof.Proof; +import de.uka.ilkd.key.ui.core.KeYMediator; +import de.uka.ilkd.key.ui.core.KeYSelectionEvent; +import de.uka.ilkd.key.ui.core.KeYSelectionListener; import org.key_project.slicing.analysis.AnalysisResults; diff --git a/keyext.slicing/src/main/java/org/key_project/slicing/ui/SlicingLeftPanel.java b/keyext.slicing/src/main/java/org/key_project/slicing/ui/SlicingLeftPanel.java index 6af1fb82d77..afa7c46a311 100644 --- a/keyext.slicing/src/main/java/org/key_project/slicing/ui/SlicingLeftPanel.java +++ b/keyext.slicing/src/main/java/org/key_project/slicing/ui/SlicingLeftPanel.java @@ -19,9 +19,6 @@ import javax.swing.border.TitledBorder; import de.uka.ilkd.key.control.DefaultUserInterfaceControl; -import de.uka.ilkd.key.core.KeYMediator; -import de.uka.ilkd.key.core.KeYSelectionEvent; -import de.uka.ilkd.key.core.KeYSelectionListener; import de.uka.ilkd.key.gui.IssueDialog; import de.uka.ilkd.key.gui.KeYFileChooser; import de.uka.ilkd.key.gui.MainWindow; @@ -32,9 +29,13 @@ import de.uka.ilkd.key.proof.Proof; import de.uka.ilkd.key.proof.ProofTreeEvent; import de.uka.ilkd.key.proof.ProofTreeListener; -import de.uka.ilkd.key.proof.io.ProblemLoader; import de.uka.ilkd.key.proof.io.ProblemLoaderControl; +import de.uka.ilkd.key.ui.core.KeYMediator; +import de.uka.ilkd.key.ui.core.KeYSelectionEvent; +import de.uka.ilkd.key.ui.core.KeYSelectionListener; +import de.uka.ilkd.key.ui.proof.io.ProblemLoader; +import org.key_project.dockingframes.common.common.action.CAction; import org.key_project.slicing.DependencyTracker; import org.key_project.slicing.SlicingExtension; import org.key_project.slicing.SlicingProofReplayer; @@ -43,7 +44,6 @@ import org.key_project.slicing.util.GenericWorker; import org.key_project.slicing.util.GraphvizDotExecutor; -import bibliothek.gui.dock.common.action.CAction; import org.jspecify.annotations.NonNull; import org.slf4j.Logger; import org.slf4j.LoggerFactory; diff --git a/keyext.ui.testgen/src/main/java/de/uka/ilkd/key/gui/testgen/CounterExampleAction.java b/keyext.ui.testgen/src/main/java/de/uka/ilkd/key/gui/testgen/CounterExampleAction.java index a3b4c5deb74..c816e2f15a5 100644 --- a/keyext.ui.testgen/src/main/java/de/uka/ilkd/key/gui/testgen/CounterExampleAction.java +++ b/keyext.ui.testgen/src/main/java/de/uka/ilkd/key/gui/testgen/CounterExampleAction.java @@ -9,23 +9,23 @@ import javax.swing.*; import de.uka.ilkd.key.control.AutoModeListener; -import de.uka.ilkd.key.core.InterruptListener; -import de.uka.ilkd.key.core.KeYSelectionEvent; -import de.uka.ilkd.key.core.KeYSelectionListener; import de.uka.ilkd.key.gui.IssueDialog; import de.uka.ilkd.key.gui.MainWindow; import de.uka.ilkd.key.gui.actions.MainWindowAction; import de.uka.ilkd.key.gui.fonticons.IconFactory; import de.uka.ilkd.key.gui.smt.SolverListener; import de.uka.ilkd.key.logic.Sequent; -import de.uka.ilkd.key.macros.SemanticsBlastingMacro; import de.uka.ilkd.key.proof.*; import de.uka.ilkd.key.settings.DefaultSMTSettings; import de.uka.ilkd.key.settings.ProofIndependentSettings; import de.uka.ilkd.key.smt.SolverLauncherListener; -import de.uka.ilkd.key.smt.counterexample.AbstractCounterExampleGenerator; -import de.uka.ilkd.key.smt.counterexample.AbstractSideProofCounterExampleGenerator; import de.uka.ilkd.key.smt.solvertypes.SolverTypes; +import de.uka.ilkd.key.testgen.macros.SemanticsBlastingMacro; +import de.uka.ilkd.key.testgen.smt.counterexample.AbstractCounterExampleGenerator; +import de.uka.ilkd.key.testgen.smt.counterexample.AbstractSideProofCounterExampleGenerator; +import de.uka.ilkd.key.ui.core.InterruptListener; +import de.uka.ilkd.key.ui.core.KeYSelectionEvent; +import de.uka.ilkd.key.ui.core.KeYSelectionListener; import org.slf4j.Logger; import org.slf4j.LoggerFactory; diff --git a/keyext.ui.testgen/src/main/java/de/uka/ilkd/key/gui/testgen/TGInfoDialog.java b/keyext.ui.testgen/src/main/java/de/uka/ilkd/key/gui/testgen/TGInfoDialog.java index 087e4c5d59f..50eeea8e800 100644 --- a/keyext.ui.testgen/src/main/java/de/uka/ilkd/key/gui/testgen/TGInfoDialog.java +++ b/keyext.ui.testgen/src/main/java/de/uka/ilkd/key/gui/testgen/TGInfoDialog.java @@ -10,8 +10,8 @@ import de.uka.ilkd.key.gui.MainWindow; import de.uka.ilkd.key.gui.actions.KeyAction; -import de.uka.ilkd.key.smt.testgen.TestGenerationLog; -import de.uka.ilkd.key.util.ThreadUtilities; +import de.uka.ilkd.key.testgen.smt.testgen.TestGenerationLog; +import de.uka.ilkd.key.ui.util.ThreadUtilities; import org.slf4j.Logger; import org.slf4j.LoggerFactory; diff --git a/keyext.ui.testgen/src/main/java/de/uka/ilkd/key/gui/testgen/TGWorker.java b/keyext.ui.testgen/src/main/java/de/uka/ilkd/key/gui/testgen/TGWorker.java index e89942b18ac..3d879f3e400 100644 --- a/keyext.ui.testgen/src/main/java/de/uka/ilkd/key/gui/testgen/TGWorker.java +++ b/keyext.ui.testgen/src/main/java/de/uka/ilkd/key/gui/testgen/TGWorker.java @@ -7,8 +7,6 @@ import javax.swing.*; import de.uka.ilkd.key.control.UserInterfaceControl; -import de.uka.ilkd.key.core.InterruptListener; -import de.uka.ilkd.key.core.KeYMediator; import de.uka.ilkd.key.gui.MainWindow; import de.uka.ilkd.key.java.Services; import de.uka.ilkd.key.logic.Sequent; @@ -18,8 +16,10 @@ import de.uka.ilkd.key.proof.init.InitConfig; import de.uka.ilkd.key.proof.init.ProofInputException; import de.uka.ilkd.key.proof.mgt.SpecificationRepository; -import de.uka.ilkd.key.smt.testgen.AbstractTestGenerator; -import de.uka.ilkd.key.smt.testgen.StopRequest; +import de.uka.ilkd.key.testgen.smt.testgen.AbstractTestGenerator; +import de.uka.ilkd.key.testgen.smt.testgen.StopRequest; +import de.uka.ilkd.key.ui.core.InterruptListener; +import de.uka.ilkd.key.ui.core.KeYMediator; /** * The worker must be started using method {@link TGWorker#start()} and not diff --git a/keyext.ui.testgen/src/main/java/de/uka/ilkd/key/gui/testgen/TestGenerationAction.java b/keyext.ui.testgen/src/main/java/de/uka/ilkd/key/gui/testgen/TestGenerationAction.java index 88bba3bad03..07d6b2c78ed 100644 --- a/keyext.ui.testgen/src/main/java/de/uka/ilkd/key/gui/testgen/TestGenerationAction.java +++ b/keyext.ui.testgen/src/main/java/de/uka/ilkd/key/gui/testgen/TestGenerationAction.java @@ -9,8 +9,6 @@ import javax.swing.*; import de.uka.ilkd.key.control.AutoModeListener; -import de.uka.ilkd.key.core.KeYSelectionEvent; -import de.uka.ilkd.key.core.KeYSelectionListener; import de.uka.ilkd.key.gui.MainWindow; import de.uka.ilkd.key.gui.actions.MainWindowAction; import de.uka.ilkd.key.gui.fonticons.IconFactory; @@ -18,6 +16,8 @@ import de.uka.ilkd.key.proof.ProofEvent; import de.uka.ilkd.key.settings.ProofIndependentSettings; import de.uka.ilkd.key.smt.solvertypes.SolverTypes; +import de.uka.ilkd.key.ui.core.KeYSelectionEvent; +import de.uka.ilkd.key.ui.core.KeYSelectionListener; /** diff --git a/keyext.ui.testgen/src/main/java/de/uka/ilkd/key/gui/testgen/TestgenExtension.java b/keyext.ui.testgen/src/main/java/de/uka/ilkd/key/gui/testgen/TestgenExtension.java index a870a2441d4..2b50ca0e1f2 100644 --- a/keyext.ui.testgen/src/main/java/de/uka/ilkd/key/gui/testgen/TestgenExtension.java +++ b/keyext.ui.testgen/src/main/java/de/uka/ilkd/key/gui/testgen/TestgenExtension.java @@ -10,13 +10,13 @@ import java.util.List; import javax.swing.*; -import de.uka.ilkd.key.core.KeYMediator; import de.uka.ilkd.key.gui.MainWindow; import de.uka.ilkd.key.gui.extension.api.KeYGuiExtension; import de.uka.ilkd.key.gui.keyshortcuts.KeyStrokeManager; import de.uka.ilkd.key.gui.keyshortcuts.KeyStrokeSettings; import de.uka.ilkd.key.gui.settings.SettingsProvider; -import de.uka.ilkd.key.macros.TestGenMacro; +import de.uka.ilkd.key.testgen.macros.TestGenMacro; +import de.uka.ilkd.key.ui.core.KeYMediator; import org.jspecify.annotations.NonNull; diff --git a/keyext.ui.testgen/src/main/java/de/uka/ilkd/key/gui/testgen/TestgenOptionsPanel.java b/keyext.ui.testgen/src/main/java/de/uka/ilkd/key/gui/testgen/TestgenOptionsPanel.java index 886cae40008..4e1cf214e2b 100644 --- a/keyext.ui.testgen/src/main/java/de/uka/ilkd/key/gui/testgen/TestgenOptionsPanel.java +++ b/keyext.ui.testgen/src/main/java/de/uka/ilkd/key/gui/testgen/TestgenOptionsPanel.java @@ -8,7 +8,7 @@ import de.uka.ilkd.key.gui.MainWindow; import de.uka.ilkd.key.gui.settings.SettingsPanel; import de.uka.ilkd.key.gui.settings.SettingsProvider; -import de.uka.ilkd.key.settings.TestGenerationSettings; +import de.uka.ilkd.key.testgen.settings.TestGenerationSettings; public class TestgenOptionsPanel extends SettingsPanel implements SettingsProvider { private static final long serialVersionUID = -2170118134719823425L; diff --git a/keyext.ui.testgen/src/main/java/module-info.java b/keyext.ui.testgen/src/main/java/module-info.java new file mode 100644 index 00000000000..d6853b53e37 --- /dev/null +++ b/keyext.ui.testgen/src/main/java/module-info.java @@ -0,0 +1,10 @@ +import de.uka.ilkd.key.gui.extension.api.KeYGuiExtension; + +/** + * + * @author Alexander Weigl + * @version 1 (31.03.24) + */ +module keyext.ui.testgen{requires java.desktop;requires org.key_project.ui;requires org.slf4j;requires org.key_project.core;requires org.key_project.core.testgen;requires org.jspecify; + +provides KeYGuiExtension with de.uka.ilkd.key.gui.testgen.TestgenExtension;} diff --git a/recoder/src/main/java/module-info.java b/recoder/src/main/java/module-info.java new file mode 100644 index 00000000000..373c3347ab5 --- /dev/null +++ b/recoder/src/main/java/module-info.java @@ -0,0 +1,27 @@ +/** + * + * @author Alexander Weigl + * @version 1 (31.03.24) + */ +module key.recoder { + exports recoder; + exports recoder.abstraction; + exports recoder.convenience; + exports recoder.java.declaration; + exports recoder.java; + exports recoder.java.reference; + exports recoder.java.statement; + exports recoder.list.generic; + exports recoder.service; + exports recoder.parser; + exports recoder.io; + exports recoder.java.expression; + exports recoder.bytecode; + exports recoder.java.expression.operator; + exports recoder.util; + exports recoder.java.declaration.modifier; + exports recoder.kit; + exports recoder.java.expression.literal; + requires java.desktop; + requires org.slf4j; +} \ No newline at end of file diff --git a/recoder/src/main/java/recoder/service/DefaultProgramModelInfo.java b/recoder/src/main/java/recoder/service/DefaultProgramModelInfo.java index cd48ec0e173..c9800b533e0 100644 --- a/recoder/src/main/java/recoder/service/DefaultProgramModelInfo.java +++ b/recoder/src/main/java/recoder/service/DefaultProgramModelInfo.java @@ -63,7 +63,7 @@ protected final void updateModel() { /** * Internally used to register a subtype link. */ - void registerSubtype(ClassType subtype, ClassType supertype) { + protected void registerSubtype(ClassType subtype, ClassType supertype) { ProgramModelInfo pmi = supertype.getProgramModelInfo(); if (pmi != this) { ((DefaultProgramModelInfo) pmi).registerSubtype(subtype, supertype);