Skip to content

Options Panel in Load Dialog. Options in Recent Files#3788

Open
wadoon wants to merge 1 commit intomainfrom
weigl/loadoptionpanel
Open

Options Panel in Load Dialog. Options in Recent Files#3788
wadoon wants to merge 1 commit intomainfrom
weigl/loadoptionpanel

Conversation

@wadoon
Copy link
Copy Markdown
Member

@wadoon wadoon commented Mar 23, 2026

Intended Change

This pull request resolves #3739

Intended Change

Critical things

  • Renovation of InitConfig. Choice selection is now stored as Choice in a Map<String,Choice>. This avoids complicated collision handling. Also default choices, and program/user/file-activated choices are kept separately.

UI

image

I was not able to screenshot the tool-tip.

This PR adds the feature of having Profile-dependent options in the load proof options.

Recent Files are stored along with their options and load settings.

I also decided to use a new file recentFiles_v2.json to avoid loading problems with older versions.

[
    {
        "options" : null,
        "path" : "/home/weigl/work/key/key.ui/examples/standard_key/prop_log/contraposition.key",
        "profile" : null,
        "singleJava" : false
    }, {
        "options" : {
            "wdOperator" : "wdOperator:Y"
        },
        "path" : "/home/weigl/work/key/key.ui/examples/heap/simple/src/MySubclass.java",
        "profile" : "java-wd",
        "singleJava" : false
    }
]

Related Issue

This pull request resolves #3742, #3739.

Plan

  • ConfigurationWriter / Configuration patches are missing

Type of pull request

  • Bug fix (non-breaking change which fixes an issue)
  • New feature (non-breaking change which adds functionality)

Ensuring quality

  • I made sure that introduced/changed code is well documented (javadoc and inline comments).
  • I made sure that new/changed end-user features are well documented (https://github.com/KeYProject/key-docs).
  • I added new test case(s) for new functionality.
  • I have tested the feature as follows: ...
  • I have checked that runtime performance has not deteriorated.
  • For new Gradle modules: I added the Gradle module to the test matrix in
    .github/workflows/tests.yml

Additional information and contact(s)

The contributions within this pull request are licensed under GPLv2 (only) for inclusion in KeY.

@wadoon wadoon force-pushed the weigl/loadoptionpanel branch from ca88ce5 to 3ab1e22 Compare March 23, 2026 22:49
@wadoon wadoon requested a review from unp1 March 23, 2026 23:04
@wadoon wadoon self-assigned this Mar 23, 2026
@wadoon wadoon added the Feature New feature or request label Mar 23, 2026
@wadoon wadoon added this to the v3.0.0 milestone Mar 23, 2026
@wadoon wadoon changed the title fix choices in init config Options Panel in Load Dialog. Options in Recent Files Mar 23, 2026
@wadoon wadoon linked an issue Mar 23, 2026 that may be closed by this pull request
1 task
@wadoon wadoon force-pushed the weigl/loadoptionpanel branch 4 times, most recently from 0697238 to 174683b Compare March 24, 2026 15:32
@wadoon wadoon marked this pull request as ready for review March 24, 2026 20:40
@unp1
Copy link
Copy Markdown
Member

unp1 commented Mar 25, 2026

Just from a brief test:

  1. When loading for example "ReverseArray (directly from the source directory)" selecting the welldefinedness profile.
  2. Selecting a WD PO
  3. Proof > Show All Active Settings shows "wdCheck:Off" and always the "L" operator even if a different operator was chosen in the panel

@wadoon wadoon force-pushed the weigl/loadoptionpanel branch 4 times, most recently from 66c7fac to dbb55a9 Compare March 28, 2026 23:05
# Conflicts:
#	key.ui/src/main/java/de/uka/ilkd/key/gui/RecentFileMenu.java

# Conflicts:
#	key.ui/src/main/java/de/uka/ilkd/key/gui/extension/api/KeYGuiExtension.java

# Conflicts:
#	key.core/src/main/java/de/uka/ilkd/key/proof/init/ProblemInitializer.java
@wadoon wadoon force-pushed the weigl/loadoptionpanel branch from eef92ec to 0ea6348 Compare April 4, 2026 14:54
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

Feature New feature or request

Projects

None yet

Development

Successfully merging this pull request may close these issues.

Who wins: Selected Profile vs. the Profile given by KeY files. Make WD semantics selectable during loading

2 participants