Skip to content

Commit ca88ce5

Browse files
wadoonwadoon
committed
fix choices in init config
fix null in Configuration forgotten token types in highlighter fixing RecentFileMenu fix get rid of getOrigin() using MetaSpace * overhaul ContextMenu of InfoTree and clean Extension API fix rebasing 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 Test for taclet option * fixed activeTacletOption in InitConfig to forbid multiple choices for the same category * enh Info window to show current taclet options for the active proof * refactor Info window * enh Documentation system: Using now the doc_comments instead of XML files. adding the possibility to have a Profile-dependent option panel # Conflicts: # key.core/src/main/java/de/uka/ilkd/key/logic/NamespaceSet.java
1 parent de96d21 commit ca88ce5

14 files changed

Lines changed: 485 additions & 181 deletions

File tree

‎key.core.symbolic_execution/src/main/java/de/uka/ilkd/key/symbolic_execution/profile/SymbolicExecutionJavaProfile.java‎

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -325,4 +325,9 @@ public static boolean isTruthValueEvaluationEnabled(Profile profile) {
325325
return false;
326326
}
327327
}
328+
329+
@Override
330+
public String displayName() {
331+
return NAME;
332+
}
328333
}

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

Lines changed: 31 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -5,6 +5,7 @@
55

66
import java.net.URL;
77
import java.util.Objects;
8+
import java.util.stream.Collectors;
89

910
import de.uka.ilkd.key.java.Services;
1011
import de.uka.ilkd.key.proof.Proof;
@@ -15,11 +16,15 @@
1516
import de.uka.ilkd.key.proof.io.RuleSourceFactory;
1617
import de.uka.ilkd.key.proof.mgt.SpecificationRepository;
1718
import de.uka.ilkd.key.rule.*;
19+
import de.uka.ilkd.key.settings.Configuration;
1820
import de.uka.ilkd.key.util.KeYResourceManager;
1921

22+
import org.key_project.logic.Choice;
2023
import org.key_project.logic.Name;
2124
import org.key_project.util.collection.ImmutableList;
2225

26+
import org.jspecify.annotations.Nullable;
27+
2328
/**
2429
* @author Alexander Weigl
2530
* @version 1 (7/27/25)
@@ -97,9 +102,34 @@ public RuleCollection getStandardRules() {
97102
return wdStandardRules;
98103
}
99104

105+
/// {@inheritDoc}
106+
///
107+
/// @param additionalProfileOptions a string representing the choice of `wdOperator`
100108
@Override
101-
public void prepareInitConfig(InitConfig baseConfig) {
109+
public void prepareInitConfig(InitConfig baseConfig,
110+
@Nullable Configuration additionalProfileOptions) {
102111
var wdChoice = baseConfig.choiceNS().lookup(new Name("wdChecks:on"));
103112
baseConfig.activateChoice(wdChoice);
113+
114+
if (additionalProfileOptions != null) {
115+
final var selectedWdOperator = additionalProfileOptions.getString("wdOperator");
116+
if (selectedWdOperator == null) {
117+
return;
118+
}
119+
120+
var wdOperator = baseConfig.choiceNS().lookup(selectedWdOperator);
121+
if (wdOperator == null) {
122+
var choices = baseConfig.choiceNS().allElements()
123+
.stream()
124+
.filter(it -> it.category().equals("wdOperator"))
125+
.map(Choice::toString)
126+
.collect(Collectors.joining(", "));
127+
128+
throw new IllegalStateException("Could not find choice for %s. \n Choices known %s."
129+
.formatted(additionalProfileOptions, choices));
130+
} else {
131+
baseConfig.activateChoice(wdOperator);
132+
}
133+
}
104134
}
105135
}

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

Lines changed: 0 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -17,7 +17,6 @@
1717

1818
import org.jspecify.annotations.NonNull;
1919
import org.jspecify.annotations.NullMarked;
20-
import org.jspecify.annotations.Nullable;
2120

2221

2322
@NullMarked
@@ -38,10 +37,6 @@ public Name name() {
3837
return NAME;
3938
}
4039

41-
@Override
42-
public @Nullable String getOrigin() {
43-
return super.getOrigin();
44-
}
4540

4641
protected static class WdWhileInvariantRuleApplier extends WhileInvariantRuleApplier {
4742
public WdWhileInvariantRuleApplier(Goal goal, LoopInvariantBuiltInRuleApp<?> ruleApp) {

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

Lines changed: 60 additions & 23 deletions
Original file line numberDiff line numberDiff line change
@@ -3,21 +3,24 @@
33
* SPDX-License-Identifier: GPL-2.0-only */
44
package de.uka.ilkd.key.gui;
55

6-
import java.util.Arrays;
7-
import java.util.Objects;
6+
import java.util.ArrayList;
7+
import java.util.Map;
88
import java.util.ServiceLoader;
99
import javax.swing.*;
1010

11+
import de.uka.ilkd.key.gui.extension.api.KeYGuiExtension;
12+
import de.uka.ilkd.key.gui.extension.impl.KeYGuiExtensionFacade;
1113
import de.uka.ilkd.key.gui.settings.SettingsPanel;
12-
import de.uka.ilkd.key.proof.init.AbstractProfile;
1314
import de.uka.ilkd.key.proof.init.DefaultProfileResolver;
1415
import de.uka.ilkd.key.proof.init.Profile;
16+
import de.uka.ilkd.key.settings.Configuration;
1517

1618
import net.miginfocom.layout.AC;
1719
import net.miginfocom.layout.CC;
1820
import net.miginfocom.layout.LC;
1921
import net.miginfocom.swing.MigLayout;
2022
import org.checkerframework.checker.nullness.qual.Nullable;
23+
import org.jspecify.annotations.NonNull;
2124

2225
public class KeYFileChooserLoadingOptions extends JPanel {
2326
private final JLabel lblProfile = new JLabel("Profile:");
@@ -39,6 +42,11 @@ public class KeYFileChooserLoadingOptions extends JPanel {
3942
Mark this checkbox to only load the selected Java file.
4043
""");
4144

45+
private final Map<Profile, KeYGuiExtension.OptionPanel> additionalOptionPanels =
46+
KeYGuiExtensionFacade.createAdditionalOptionPanels();
47+
48+
49+
private KeYGuiExtension.@Nullable OptionPanel currentOptionPanel = null;
4250

4351
public KeYFileChooserLoadingOptions(KeYFileChooser chooser) {
4452
setLayout(new MigLayout(new LC().fillX().wrapAfter(3).maxWidth("400"),
@@ -48,16 +56,23 @@ public KeYFileChooserLoadingOptions(KeYFileChooser chooser) {
4856
lblProfileInfo.setWrapStyleWord(true);
4957
lblProfileInfo.setLineWrap(true);
5058

51-
var items = ServiceLoader.load(DefaultProfileResolver.class)
52-
.stream().map(it -> it.get().getDefaultProfile())
53-
.map(ProfileWrapper::new)
54-
.toArray(ProfileWrapper[]::new);
59+
var profiles =
60+
new ArrayList<>(ServiceLoader.load(DefaultProfileResolver.class)
61+
.stream().map(it -> it.get().getDefaultProfile())
62+
.map(ProfileWrapper::new)
63+
.toList());
64+
65+
final var legacyMode = new ProfileWrapper("Respect profile given in file", "",
66+
"Usable on KeY file which defines \\profile inside the file. " +
67+
"If no KeY file is loaded, falls back to legacy behavior",
68+
null);
69+
70+
profiles.addFirst(legacyMode);
71+
72+
var items = profiles.toArray(ProfileWrapper[]::new);
73+
5574
cboProfile.setModel(new DefaultComboBoxModel<>(items));
56-
cboProfile.setSelectedItem(
57-
Arrays.stream(items)
58-
.filter(it -> it.profile.equals(AbstractProfile.getDefaultProfile()))
59-
.findFirst()
60-
.orElse(null));
75+
cboProfile.setSelectedItem(legacyMode);
6176

6277
cboProfile.addItemListener(evt -> updateProfileInfo());
6378
updateProfileInfo();
@@ -78,34 +93,56 @@ private void updateProfileInfo() {
7893
}
7994

8095
private void updateProfileInfo(@Nullable ProfileWrapper selectedItem) {
96+
if (currentOptionPanel != null) {
97+
currentOptionPanel.deinstall(this);
98+
}
99+
81100
if (selectedItem == null) {
82101
lblProfileInfo.setText("");
83102
} else {
84-
lblProfileInfo.setText(selectedItem.profile.description());
103+
lblProfileInfo.setText(selectedItem.description());
104+
if (additionalOptionPanels.containsKey(selectedItem.profile)) {
105+
currentOptionPanel = additionalOptionPanels.get(selectedItem.profile);
106+
currentOptionPanel.install(this);
107+
}
85108
}
86109
}
87110

88111
public @Nullable Profile getSelectedProfile() {
89-
var selected = getSelectedProfileName();
90-
var items = ServiceLoader.load(DefaultProfileResolver.class)
91-
.stream().filter(it -> Objects.equals(selected, it.get().getProfileName()))
92-
.findFirst();
93-
return items.map(it -> it.get().getDefaultProfile())
94-
.orElse(null);
112+
var selected = (ProfileWrapper) cboProfile.getSelectedItem();
113+
if (selected == null) {
114+
return null;
115+
}
116+
return selected.profile();
117+
}
118+
119+
public @Nullable Configuration getAdditionalProfileOptions() {
120+
if (currentOptionPanel == null) {
121+
return null;
122+
}
123+
return currentOptionPanel.getResult();
95124
}
96125

97126
public @Nullable String getSelectedProfileName() {
98-
return ((ProfileWrapper) cboProfile.getSelectedItem()).profile().ident();
127+
final var selectedItem = (ProfileWrapper) cboProfile.getSelectedItem();
128+
if (selectedItem == null)
129+
return null;
130+
return selectedItem.ident();
99131
}
100132

101133
public boolean isOnlyLoadSingleJavaFile() {
102134
return lblSingleJava.isSelected();
103135
}
104136

105-
record ProfileWrapper(Profile profile) {
137+
record ProfileWrapper(String name, String ident, String description,
138+
@Nullable Profile profile) {
139+
ProfileWrapper(Profile profile) {
140+
this(profile.displayName(), profile.ident(), profile.description(), profile);
141+
}
142+
106143
@Override
107-
public String toString() {
108-
return profile.displayName();
144+
public @NonNull String toString() {
145+
return name;
109146
}
110147
}
111148
}

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

Lines changed: 10 additions & 8 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

@@ -323,10 +322,10 @@ private MainWindow() {
323322
proofListView = new JScrollPane(proofList);
324323

325324
notificationManager = new NotificationManager(mediator, this);
326-
recentFileMenu = new RecentFileMenu(mediator);
325+
recentFileMenu = new RecentFileMenu(this);
327326

328327
proofTreeView = new ProofTreeView(mediator);
329-
infoView = new InfoView(this, mediator);
328+
infoView = new InfoView(mediator);
330329
strategySelectionView = new StrategySelectionView(this, mediator);
331330
openGoalsView = new GoalList(mediator);
332331

@@ -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)