Skip to content

Commit 4b1a8ae

Browse files
wadoonwadoon
committed
wip
1 parent 5f036c9 commit 4b1a8ae

7 files changed

Lines changed: 86 additions & 12 deletions

File tree

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -466,7 +466,7 @@ private InitConfig createInitConfigFor(EnvInput envInput) throws ProofInputExcep
466466
// cache the last used init config
467467
BaseConfigCache.setBaseInputConfig(config, inputDigest);
468468
config = config.copy();
469-
profile.prepareInitConfig(config);
469+
profile.prepareInitConfig(config, null);
470470
return config;
471471
}
472472

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

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -12,8 +12,10 @@
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

18+
import org.jspecify.annotations.Nullable;
1719
import org.key_project.logic.Name;
1820
import org.key_project.prover.engine.GoalChooserFactory;
1921
import org.key_project.prover.proof.ProofGoal;
@@ -181,7 +183,7 @@ default UseOperationContractRule getUseOperationContractRule() {
181183
/// established.
182184
///
183185
/// @see ProblemInitializer
184-
default void prepareInitConfig(InitConfig baseConfig) {
186+
default void prepareInitConfig(InitConfig baseConfig, @Nullable Configuration configuration) {
185187

186188
}
187189
}

‎key.core/src/main/java/de/uka/ilkd/key/scripts/ProofScriptEngine.java‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -71,7 +71,7 @@ public ProofScriptEngine(List<ScriptCommandAst> script, Goal initiallySelectedGo
7171
this.script = script;
7272
}
7373

74-
private static Map<String, ProofScriptCommand> loadCommands() {
74+
public static Map<String, ProofScriptCommand> loadCommands() {
7575
Map<String, ProofScriptCommand> result = new HashMap<>();
7676
var loader = ServiceLoader.load(ProofScriptCommand.class);
7777

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

Lines changed: 78 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -16,6 +16,8 @@
1616
import javax.swing.tree.DefaultTreeModel;
1717
import javax.swing.tree.MutableTreeNode;
1818

19+
import com.google.common.collect.Multimap;
20+
import com.google.common.collect.MultimapBuilder;
1921
import de.uka.ilkd.key.core.KeYMediator;
2022
import de.uka.ilkd.key.core.KeYSelectionEvent;
2123
import de.uka.ilkd.key.core.KeYSelectionListener;
@@ -28,6 +30,10 @@
2830
import de.uka.ilkd.key.gui.utilities.LexerHighlighter;
2931
import de.uka.ilkd.key.logic.MetaSpace;
3032
import de.uka.ilkd.key.logic.label.TermLabelManager;
33+
import de.uka.ilkd.key.logic.op.ParametricFunctionDecl;
34+
import de.uka.ilkd.key.logic.sort.ParametricSortDecl;
35+
import de.uka.ilkd.key.logic.sort.SortAlias;
36+
import de.uka.ilkd.key.nparser.KeyAst;
3137
import de.uka.ilkd.key.pp.LogicPrinter;
3238
import de.uka.ilkd.key.pp.NotationInfo;
3339
import de.uka.ilkd.key.proof.Goal;
@@ -41,14 +47,18 @@
4147
import de.uka.ilkd.key.rule.NoPosTacletApp;
4248
import de.uka.ilkd.key.rule.OneStepSimplifier;
4349
import de.uka.ilkd.key.rule.Taclet;
50+
import de.uka.ilkd.key.scripts.ProofScriptCommand;
51+
import de.uka.ilkd.key.scripts.ProofScriptEngine;
4452
import de.uka.ilkd.key.util.MiscTools;
4553

4654
import org.key_project.logic.Choice;
55+
import org.key_project.logic.HasMeta;
4756
import org.key_project.logic.Name;
4857
import org.key_project.logic.Namespace;
4958
import org.key_project.logic.op.Function;
5059
import org.key_project.logic.sort.Sort;
5160
import org.key_project.prover.rules.RuleApp;
61+
import org.key_project.prover.rules.RuleSet;
5262
import org.key_project.util.collection.ImmutableList;
5363

5464
import org.jspecify.annotations.NullMarked;
@@ -271,9 +281,71 @@ private DefaultMutableTreeNode createInfoTreeRoot(Goal g) {
271281
root.add(createNodeTermLabels(docs, g.proof()));
272282
root.add(createNodeFunctions(docs, g.proof().getNamespaces().functions()));
273283
root.add(createNodeTacletOptions(docs, g.proof().getInitConfig()));
284+
root.add(createNodeChoices(docs, g.proof().getNamespaces().choices()));
285+
root.add(createNodeRS("Parametric Funcions", docs, g.proof().getNamespaces().parametricFunctions().allElements()));
286+
root.add(createNodeRS("Parametric Sorts", docs, g.proof().getNamespaces().parametricSorts().allElements()));
287+
root.add(createNodeRS("Rule Sets", docs, g.proof().getNamespaces().ruleSets().allElements()));
288+
root.add(createNodeAliases(docs, g.proof().getNamespaces().sortAliases().allElements()));
289+
root.add(createNodeRS("Variables",docs, g.proof().getNamespaces().variables().allElements()));
290+
root.add(createNodeRS("Program Variables", docs, g.proof().getNamespaces().programVariables().allElements()));
291+
root.add(createNodeScripts(docs));
274292
return root;
275293
}
276294

295+
private MutableTreeNode createNodeAliases(MetaSpace docs, Collection<SortAlias> sortAliases) {
296+
var tlRoot = create("Sort Alias", "");
297+
for (var alias : sortAliases) {
298+
tlRoot.add(new InfoTreeNode(alias.name().toString(),
299+
() -> "Alias of " + alias.aliasedSort() + "\n" + docs.findDocumentation(alias.aliasedSort())));
300+
}
301+
return tlRoot;
302+
}
303+
304+
private MutableTreeNode createNodeRS(String title, MetaSpace docs, Collection<? extends HasMeta> ruleSets) {
305+
var tlRoot = create(title, "");
306+
for (var element : ruleSets) {
307+
tlRoot.add(new InfoTreeNode(element.toString(), () -> docs.findDocumentation(element)));
308+
}
309+
return tlRoot;
310+
}
311+
312+
private MutableTreeNode createNodePS(MetaSpace docs, Namespace<ParametricSortDecl> sorts) {
313+
var tlRoot = create("Parametric Sorts", "");
314+
for (var element : sorts.allElements()) {
315+
tlRoot.add(new InfoTreeNode(element.toString(), () -> docs.findDocumentation(element)));
316+
}
317+
return tlRoot;
318+
}
319+
320+
private MutableTreeNode createNodePF(MetaSpace docs, Namespace<ParametricFunctionDecl> funcs) {
321+
var tlRoot = create("Parametric Functions", "");
322+
for (var element : funcs.allElements()) {
323+
tlRoot.add(new InfoTreeNode(element.toString(), () -> docs.findDocumentation(element)));
324+
}
325+
return tlRoot;
326+
}
327+
328+
private InfoTreeNode createNodeChoices(MetaSpace docs, Namespace<Choice> choices) {
329+
var tlRoot = create("Choices", "Browse descriptions for currently available choices");
330+
Multimap<String, InfoTreeNode> map = MultimapBuilder.hashKeys().arrayListValues(4).build();
331+
choices.allElements().forEach((c) ->
332+
map.put(c.category(), new InfoTreeNode(c.name().toString(), () -> docs.findDocumentation(c))));
333+
for (var s : map.keySet()) {
334+
var cat = new InfoTreeNode(s, () -> docs.findDocumentation(new HasMeta.OptionCategory(s)));
335+
map.get(s).forEach(cat::add);
336+
tlRoot.add(cat);
337+
}
338+
return tlRoot;
339+
}
340+
341+
private InfoTreeNode createNodeScripts(MetaSpace docs) {
342+
var tlRoot = create("Proof Script Commands", "Browse descriptions for currently available proof script commands.");
343+
ProofScriptEngine.loadCommands().forEach((key, value) -> {
344+
tlRoot.add(new InfoTreeNode(key, () -> value.getDocumentation()));
345+
});
346+
return tlRoot;
347+
}
348+
277349
private InfoTreeNode createNodeRules(MetaSpace docs, Goal g) {
278350
var tlRoot = create("Rules", "Browse descriptions for currently available rules.");
279351

@@ -365,7 +437,7 @@ private MutableTreeNode createNodeTermLabels(MetaSpace docs, Proof proof) {
365437
return tlRoot;
366438
}
367439

368-
private InfoTreeNode createNodeFunctions(MetaSpace docs, Namespace<Function> functions) {
440+
private InfoTreeNode createNodeFunctions(MetaSpace docs, Namespace<? extends Function> functions) {
369441
var fnRoot = create("Function Symbols", DEFAULT_FUNCTIONS_LABEL);
370442
var fnByName = create("By Name", DEFAULT_FUNCTIONS_LABEL);
371443
var fnByReturnType = create("By Return Type", DEFAULT_FUNCTIONS_LABEL);
@@ -377,14 +449,14 @@ private InfoTreeNode createNodeFunctions(MetaSpace docs, Namespace<Function> fun
377449
seq.sort(Comparator.comparing(it -> it.name().toString()));
378450

379451
var byReturn = new TreeMap<Sort, List<InfoTreeNode>>(
380-
Comparator.comparing(it -> it.name().toString()));
452+
Comparator.comparing(it -> it.name().toString()));
381453

382454
for (var fn : seq) {
383455
var fnName = "%s(%s) : %s".formatted(
384-
fn.name(),
385-
fn.argSorts().stream().map(it -> it.name().toString())
386-
.collect(Collectors.joining(", ")),
387-
fn.sort().name());
456+
fn.name(),
457+
fn.argSorts().stream().map(it -> it.name().toString())
458+
.collect(Collectors.joining(", ")),
459+
fn.sort().name());
388460
var fnSort = fn.sort();
389461

390462
// flat list:

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -327,7 +327,7 @@ public void actionPerformed(ActionEvent actionEvent) {
327327
mainWindow.loadProblem(file, pl -> {
328328
if (profile != null) {
329329
pl.setProfileOfNewProofs(profile);
330-
pl.setAdditionalProfileOptions(additionalProfileOptions);
330+
//pl.setAdditionalProfileOptions(additionalProfileOptions);
331331
}
332332
pl.setLoadSingleJavaFile(fileEntry.singleJava);
333333
});

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -102,7 +102,7 @@ public void loadProblem(Path file, Consumer<ProblemLoader> configure) {
102102
mainWindow.addRecentFile(file.toAbsolutePath().toString(),
103103
problemLoader.getProfileOfNewProofs(),
104104
problemLoader.isLoadSingleJavaFile(),
105-
problemLoader.getAdditionalProfileOptions());
105+
null);
106106
problemLoader.runAsynchronously();
107107
}
108108

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -69,7 +69,7 @@ public void actionPerformed(ActionEvent e) {
6969
mainWindow.loadProblem(file, pl -> {
7070
if (selectedProfile != null) {
7171
pl.setProfileOfNewProofs(selectedProfile);
72-
pl.setAdditionalProfileOptions(additionalProfileOptions);
72+
//pl.setAdditionalProfileOptions(additionalProfileOptions);
7373
}
7474
pl.setLoadSingleJavaFile(options.isOnlyLoadSingleJavaFile());
7575
});

0 commit comments

Comments
 (0)