Options Panel in Load Dialog. Options in Recent Files

[wadoon]

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

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.

[unp1]

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

[unp1]

When loading
key.ui/examples/firstTouch/06-BinarySearch/project.key
and selecting
Java Profile + Well....
I get a strange JAR file error (not running from jar but via gradlew :key.ui:run):

Caused by: java.lang.RuntimeException: java.io.FileNotFoundException: JAR entry not found in jar file

[wadoon]

When loading key.ui/examples/firstTouch/06-BinarySearch/project.key and selecting Java Profile + Well.... I get a strange JAR file error (not running from jar but via gradlew :key.ui:run):

Caused by: java.lang.RuntimeException: java.io.FileNotFoundException: JAR entry not found in jar file

Also on main:

The error was in the construction of the FileSystem.

fixed on #3810

[unp1]

Loading a proof with a different file is ignored:

1. Load "examples/heap/removeDups/project.key with "Java Profile + WD"
2. Do proof (WD PO)
3. Save proof
4. Load proof with "Java Profile (Default)" which succeeds and applies WD

I would have expected it to fail.