Skip to content

Commit f18f025

Browse files
committed
fix errors from rebasing
1 parent 6ef3301 commit f18f025

6 files changed

Lines changed: 43 additions & 10 deletions

File tree

key.core/src/main/java/de/uka/ilkd/key/control/AbstractUserInterfaceControl.java

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -22,6 +22,7 @@
2222
import de.uka.ilkd.key.proof.io.ProblemLoaderException;
2323
import de.uka.ilkd.key.proof.io.SingleThreadProblemLoader;
2424
import de.uka.ilkd.key.proof.mgt.ProofEnvironment;
25+
import de.uka.ilkd.key.settings.Configuration;
2526

2627
import org.key_project.prover.engine.ProverCore;
2728
import org.key_project.prover.engine.ProverTaskListener;

key.core/src/main/java/de/uka/ilkd/key/nparser/KeyAst.java

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -185,6 +185,17 @@ public String getProblemHeader() {
185185
}
186186
return "";
187187
}
188+
189+
/// Returns the raw settings within a [de.uka.ilkd.key.proof.io.KeYFile].
190+
public Configuration findSettings() {
191+
final var cfg = new ConfigurationBuilder();
192+
if (ctx.preferences() == null || ctx.preferences().cvalue() == null) {
193+
return new Configuration();
194+
}
195+
196+
var c = ctx.preferences().cvalue();
197+
return (Configuration) c.accept(cfg);
198+
}
188199
}
189200

190201
public static class ConfigurationFile extends KeyAst<KeYParser.CfileContext> {

key.core/src/main/java/de/uka/ilkd/key/proof/Node.java

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -11,7 +11,6 @@
1111
import de.uka.ilkd.key.proof.reference.ClosedBy;
1212
import de.uka.ilkd.key.rule.NoPosTacletApp;
1313
import de.uka.ilkd.key.rule.merge.MergeRule;
14-
import de.uka.ilkd.key.util.Pair;
1514

1615
import org.key_project.logic.op.Function;
1716
import org.key_project.prover.rules.RuleApp;

key.core/src/main/java/de/uka/ilkd/key/proof/io/OutputStreamProofSaver.java

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -60,6 +60,8 @@
6060
import org.key_project.util.collection.ImmutableList;
6161
import org.key_project.util.collection.KeYCollections;
6262

63+
import org.jspecify.annotations.NullMarked;
64+
import org.jspecify.annotations.Nullable;
6365
import org.slf4j.Logger;
6466
import org.slf4j.LoggerFactory;
6567

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

Lines changed: 21 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -268,7 +268,7 @@ public List<Object> getList(String name) {
268268

269269
/**
270270
* Returns a list of strings for the given name.
271-
*
271+
* <p>
272272
* In contrast to the other methods, this method does not throw an exception if the entry does
273273
* not
274274
* exist in the configuration. Instead, it returns an empty list.
@@ -464,14 +464,19 @@ public Set<String> keys() {
464464
}
465465

466466
// TODO Add documentation for this.
467+
467468
/**
468469
* POJO for metadata of configuration entries.
469470
*/
470471
public static class ConfigurationMeta {
471-
/** Position of declaration within a file */
472+
/**
473+
* Position of declaration within a file
474+
*/
472475
private Position position;
473476

474-
/** documentation given in the file */
477+
/**
478+
* documentation given in the file
479+
*/
475480
private String documentation;
476481

477482
public Position getPosition() {
@@ -581,6 +586,19 @@ private ConfigurationWriter print(String s) {
581586
return this;
582587
}
583588

589+
private ConfigurationWriter printSeq(int[] values) {
590+
out.format("[");
591+
for (var i = 0; i < values.length; i++) {
592+
int o = values[i];
593+
printValue(o);
594+
if (i + 1 < values.length) {
595+
print(", ");
596+
}
597+
}
598+
out.format("]");
599+
return this;
600+
}
601+
584602
private ConfigurationWriter printSeq(Collection<?> value) {
585603
out.format("[ ");
586604
indent += 4;

key.ui/src/main/java/de/uka/ilkd/key/gui/WindowUserInterfaceControl.java

Lines changed: 8 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -34,6 +34,7 @@
3434
import de.uka.ilkd.key.proof.io.*;
3535
import de.uka.ilkd.key.proof.io.AbstractProblemLoader.ReplayResult;
3636
import de.uka.ilkd.key.rule.IBuiltInRuleApp;
37+
import de.uka.ilkd.key.settings.Configuration;
3738
import de.uka.ilkd.key.settings.ProofIndependentSettings;
3839
import de.uka.ilkd.key.settings.ProofSettings;
3940
import de.uka.ilkd.key.settings.ViewSettings;
@@ -509,8 +510,10 @@ public void loadingStarted(AbstractProblemLoader loader) {
509510

510511
@Override
511512
public void loadingFinished(AbstractProblemLoader loader, LoadedPOContainer poContainer,
512-
ProofAggregate proofList, ReplayResult result) throws ProblemLoaderException {
513-
super.loadingFinished(loader, poContainer, proofList, result);
513+
ProofAggregate proofList, ReplayResult result, Configuration settings)
514+
throws ProblemLoaderException {
515+
516+
super.loadingFinished(loader, poContainer, proofList, result, settings);
514517
if (proofList != null) {
515518
if (result != null) {
516519
if ("".equals(result.getStatus())) {
@@ -532,22 +535,21 @@ public void loadingFinished(AbstractProblemLoader loader, LoadedPOContainer poCo
532535
if (poContainer != null
533536
&& poContainer.getProofOblInput() instanceof KeYUserProblemFile file) {
534537
// TODO weigl not triggered
535-
var settings = file.readSettings();
536538
var addInfo = settings.getSection(ProofSettings.KEY_ADDITIONAL_DATA);
537539
if (addInfo != null) {
538540
var lastSelectedNodePath =
539541
settings.getIntList(OutputStreamProofSaver.KEY_LAST_SELECTED_NODE);
540542
if (lastSelectedNodePath != null && proofList != null) {
541543
var proof = proofList.getFirstProof();
542-
proof.root().traversePath(lastSelectedNodePath.iterator());
544+
var selectedNode = proof.root().traversePath(
545+
lastSelectedNodePath.stream().map(Long::intValue).iterator());
546+
getMediator().getSelectionModel().setSelectedNode(selectedNode);
543547
}
544548
}
545549
file.close();
546550
}
547551
}
548552

549-
550-
551553
/**
552554
* Loads the given location and returns all required references as {@link KeYEnvironment} with
553555
* KeY's {@link MainWindow}.

0 commit comments

Comments
 (0)