Skip to content

Commit bc01924

Browse files
wadoonwadoon
committed
store additional loading information for recentFiles
Fix double entry of Java Profile add legacy option for non-setting / non-enforcing a specific profile closes #3742 fix DocSpace parentship fix Taclet options activation spotless fixes after rebase
1 parent 573c60e commit bc01924

14 files changed

Lines changed: 202 additions & 141 deletions

File tree

‎key.core.wd/src/main/java/de/uka/ilkd/key/wd/WdProfile.java‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -15,6 +15,7 @@
1515
import de.uka.ilkd.key.proof.io.RuleSourceFactory;
1616
import de.uka.ilkd.key.proof.mgt.SpecificationRepository;
1717
import de.uka.ilkd.key.rule.*;
18+
import de.uka.ilkd.key.settings.Configuration;
1819
import de.uka.ilkd.key.util.KeYResourceManager;
1920

2021
import org.key_project.logic.Name;
@@ -104,7 +105,7 @@ public RuleCollection getStandardRules() {
104105
/// @param additionalProfileOptions a string representing the choice of `wdOperator`
105106
@Override
106107
public void prepareInitConfig(InitConfig baseConfig,
107-
@Nullable Object additionalProfileOptions) {
108+
@Nullable Configuration additionalProfileOptions) {
108109
var wdChoice = baseConfig.choiceNS().lookup(new Name("wdChecks:on"));
109110
baseConfig.activateChoice(wdChoice);
110111

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

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -191,6 +191,16 @@ public Configuration asConfiguration() {
191191
throw new RuntimeException("Error in configuration. Source: "
192192
+ ctx.start.getTokenSource().getSourceName());
193193
}
194+
195+
public List<Configuration> asConfigurationList() {
196+
final var cfg = new ConfigurationBuilder();
197+
List<Object> res = cfg.visitCfile(ctx);
198+
if (!res.isEmpty())
199+
return (List<Configuration>) res.getFirst();
200+
else
201+
throw new RuntimeException("Error in configuration. Source: "
202+
+ ctx.start.getTokenSource().getSourceName());
203+
}
194204
}
195205

196206
public static class SetStatementContext extends KeyAst<JmlParser.Set_statementContext> {

‎key.core/src/main/java/de/uka/ilkd/key/proof/init/ProblemInitializer.java‎

Lines changed: 5 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -32,6 +32,7 @@
3232
import de.uka.ilkd.key.rule.BuiltInRule;
3333
import de.uka.ilkd.key.rule.Rule;
3434
import de.uka.ilkd.key.rule.Taclet;
35+
import de.uka.ilkd.key.settings.Configuration;
3536
import de.uka.ilkd.key.settings.ProofIndependentSettings;
3637
import de.uka.ilkd.key.settings.ProofSettings;
3738
import de.uka.ilkd.key.speclang.PositionedString;
@@ -69,7 +70,7 @@ public final class ProblemInitializer {
6970
*/
7071
private FileRepo fileRepo;
7172
private ImmutableSet<PositionedString> warnings = DefaultImmutableSet.nil();
72-
private @Nullable Object additionalProfileOptions;
73+
private @Nullable Configuration additionalProfileOptions;
7374

7475
// -------------------------------------------------------------------------
7576
// constructors
@@ -86,18 +87,18 @@ public ProblemInitializer(Profile profile) {
8687
this(null, new Services(Objects.requireNonNull(profile, "Given profile is null")), null);
8788
}
8889

89-
public ProblemInitializer(Profile profile, @Nullable Object additionalProfileOptions) {
90+
public ProblemInitializer(Profile profile, @Nullable Configuration additionalProfileOptions) {
9091
this(profile);
9192
this.additionalProfileOptions = additionalProfileOptions;
9293
}
9394

9495
/// An arbitrary object which is passed to the provided profile, during construction of the
9596
/// `initConfig`.
96-
public @Nullable Object getAdditionalProfileOptions() {
97+
public @Nullable Configuration getAdditionalProfileOptions() {
9798
return additionalProfileOptions;
9899
}
99100

100-
public void setAdditionalProfileOptions(@Nullable Object additionalProfileOptions) {
101+
public void setAdditionalProfileOptions(@Nullable Configuration additionalProfileOptions) {
101102
this.additionalProfileOptions = additionalProfileOptions;
102103
}
103104

‎key.core/src/main/java/de/uka/ilkd/key/proof/init/Profile.java‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -12,6 +12,7 @@
1212
import de.uka.ilkd.key.rule.Rule;
1313
import de.uka.ilkd.key.rule.UseDependencyContractRule;
1414
import de.uka.ilkd.key.rule.UseOperationContractRule;
15+
import de.uka.ilkd.key.settings.Configuration;
1516
import de.uka.ilkd.key.strategy.StrategyFactory;
1617

1718
import org.key_project.logic.Name;
@@ -187,7 +188,7 @@ default UseOperationContractRule getUseOperationContractRule() {
187188
/// command line.
188189
/// @see ProblemInitializer
189190
default void prepareInitConfig(InitConfig baseConfig,
190-
@Nullable Object additionalProfileOptions) {
191+
@Nullable Configuration additionalProfileOptions) {
191192

192193
}
193194
}

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

Lines changed: 7 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -64,7 +64,11 @@ public abstract class AbstractProblemLoader {
6464
* @see EnvInput#isIgnoreOtherJavaFiles()
6565
*/
6666
private boolean loadSingleJavaFile = false;
67-
private Object additionalProfileOptions;
67+
68+
/**
69+
*
70+
*/
71+
private @Nullable Configuration additionalProfileOptions;
6872

6973
/**
7074
* The file or folder to load.
@@ -832,13 +836,13 @@ public void setIgnoreWarnings(boolean ignoreWarnings) {
832836
this.ignoreWarnings = ignoreWarnings;
833837
}
834838

835-
public void setAdditionalProfileOptions(Object additionalProfileOptions) {
839+
public void setAdditionalProfileOptions(@Nullable Configuration additionalProfileOptions) {
836840
this.additionalProfileOptions = additionalProfileOptions;
837841
}
838842

839843
/// An arbitrary object representing additional options for the given profile.
840844
/// @see ProblemInitializer
841-
public Object getAdditionalProfileOptions() {
845+
public Configuration getAdditionalProfileOptions() {
842846
return additionalProfileOptions;
843847
}
844848

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

Lines changed: 11 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -176,7 +176,7 @@ public long getLong(String name, long defaultValue) {
176176
* @throws NullPointerException if no such value entry exists
177177
*/
178178
public boolean getBool(String name) {
179-
return get(name, Boolean.class);
179+
return Boolean.TRUE.equals(get(name, Boolean.class));
180180
}
181181

182182
/**
@@ -350,7 +350,7 @@ private ConfigurationMeta getOrCreateMeta(String name) {
350350
/**
351351
* @see #getTable(String)
352352
*/
353-
public Configuration getSection(String name) {
353+
public @Nullable Configuration getSection(String name) {
354354
return getTable(name);
355355
}
356356

@@ -365,39 +365,39 @@ public Configuration getSection(String name, boolean createIfNotExists) {
365365
return getSection(name);
366366
}
367367

368-
public Object set(String name, Object obj) {
368+
public @Nullable Object set(String name, @Nullable Object obj) {
369369
return data.put(name, obj);
370370
}
371371

372-
public Object set(String name, Boolean obj) {
372+
public @Nullable Object set(String name, @Nullable Boolean obj) {
373373
return set(name, (Object) obj);
374374
}
375375

376-
public Object set(String name, String obj) {
376+
public @Nullable Object set(String name, @Nullable String obj) {
377377
return set(name, (Object) obj);
378378
}
379379

380-
public Object set(String name, Long obj) {
380+
public @Nullable Object set(String name, @Nullable Long obj) {
381381
return set(name, (Object) obj);
382382
}
383383

384-
public Object set(String name, int obj) {
384+
public @Nullable Object set(String name, int obj) {
385385
return set(name, (long) obj);
386386
}
387387

388-
public Object set(String name, Double obj) {
388+
public @Nullable Object set(String name, @Nullable Double obj) {
389389
return set(name, (Object) obj);
390390
}
391391

392-
public Object set(String name, Configuration obj) {
392+
public @Nullable Object set(String name, @Nullable Configuration obj) {
393393
return set(name, (Object) obj);
394394
}
395395

396-
public Object set(String name, List<?> obj) {
396+
public @Nullable Object set(String name, @Nullable List<?> obj) {
397397
return set(name, (Object) obj);
398398
}
399399

400-
public Object set(String name, String[] seq) {
400+
public @Nullable Object set(String name, @Nullable String[] seq) {
401401
return set(name, (Object) Arrays.asList(seq));
402402
}
403403

‎key.core/src/main/java/de/uka/ilkd/key/settings/PathConfig.java‎

Lines changed: 2 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -14,8 +14,8 @@
1414
* Keeps some central paths to files and directories.
1515
* </p>
1616
* <p>
17-
* By default all KeY configurations are stored in a directory named ".key" inside the user's home
18-
* directory. In Microsoft windows operating systems this is directly the hard disc that contains
17+
* By default, all KeY configurations are stored in a directory named ".key" inside the user's home
18+
* directory. In Microsoft Windows operating systems this is directly the hard disc that contains
1919
* the KeY code. But the eclipse integration requires to change the default location. This is
2020
* possible via {@link #setKeyConfigDir(String)} which should be called once before something is
2121
* done with KeY (e.g. before the {@code MainWindow} is opened).
@@ -81,7 +81,6 @@ public static Path getKeyConfigDir() {
8181
*/
8282
public static void setKeyConfigDir(String keyConfigDir) {
8383
PathConfig.keyConfigDir = Paths.get(keyConfigDir);
84-
8584
recentFileStorage = getKeyConfigDir().resolve("recentFiles.json");
8685
proofIndependentSettings = getKeyConfigDir().resolve("proofIndependentSettings.props");
8786
logDirectory = getKeyConfigDir().resolve("logs");

‎key.ui/src/main/java/de/uka/ilkd/key/gui/KeYFileChooserLoadingOptions.java‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -13,6 +13,7 @@
1313
import de.uka.ilkd.key.gui.settings.SettingsPanel;
1414
import de.uka.ilkd.key.proof.init.DefaultProfileResolver;
1515
import de.uka.ilkd.key.proof.init.Profile;
16+
import de.uka.ilkd.key.settings.Configuration;
1617

1718
import net.miginfocom.layout.AC;
1819
import net.miginfocom.layout.CC;
@@ -115,7 +116,7 @@ private void updateProfileInfo(@Nullable ProfileWrapper selectedItem) {
115116
return selected.profile();
116117
}
117118

118-
public @Nullable Object getAdditionalProfileOptions() {
119+
public @Nullable Configuration getAdditionalProfileOptions() {
119120
if (currentOptionPanel == null) {
120121
return null;
121122
}

‎key.ui/src/main/java/de/uka/ilkd/key/gui/MainWindow.java‎

Lines changed: 8 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -56,11 +56,9 @@
5656
import de.uka.ilkd.key.gui.sourceview.SourceViewFrame;
5757
import de.uka.ilkd.key.gui.utilities.LruCached;
5858
import de.uka.ilkd.key.proof.*;
59+
import de.uka.ilkd.key.proof.init.Profile;
5960
import de.uka.ilkd.key.proof.io.ProblemLoader;
60-
import de.uka.ilkd.key.settings.FeatureSettings;
61-
import de.uka.ilkd.key.settings.GeneralSettings;
62-
import de.uka.ilkd.key.settings.ProofIndependentSettings;
63-
import de.uka.ilkd.key.settings.ViewSettings;
61+
import de.uka.ilkd.key.settings.*;
6462
import de.uka.ilkd.key.smt.SolverTypeCollection;
6563
import de.uka.ilkd.key.smt.solvertypes.SolverType;
6664
import de.uka.ilkd.key.ui.AbstractMediatorUserInterfaceControl;
@@ -81,6 +79,7 @@
8179
import com.formdev.flatlaf.FlatLightLaf;
8280
import com.formdev.flatlaf.util.SystemInfo;
8381
import org.jspecify.annotations.NonNull;
82+
import org.jspecify.annotations.Nullable;
8483
import org.slf4j.Logger;
8584
import org.slf4j.LoggerFactory;
8685

@@ -1390,8 +1389,11 @@ public NotificationManager getNotificationManager() {
13901389
*
13911390
* @see RecentFileMenu#addRecentFile(String)
13921391
*/
1393-
public void addRecentFile(@NonNull String absolutePath) {
1394-
recentFileMenu.addRecentFile(absolutePath);
1392+
public void addRecentFile(@NonNull String absolutePath,
1393+
@Nullable Profile profile,
1394+
boolean singleJava,
1395+
@Nullable Configuration additionalOption) {
1396+
recentFileMenu.addRecentFile(absolutePath, profile, singleJava, additionalOption);
13951397
}
13961398

13971399
public void openExamples() {

0 commit comments

Comments
 (0)