diff --git a/.github/workflows/code_quality.yml b/.github/workflows/code_quality.yml index db2bb557f8b..0a322f8c350 100644 --- a/.github/workflows/code_quality.yml +++ b/.github/workflows/code_quality.yml @@ -13,10 +13,10 @@ jobs: runs-on: ubuntu-latest steps: - uses: actions/checkout@v7 - - name: Set up JDK 21 + - name: Set up JDK 25 uses: actions/setup-java@v6.0.1 with: - java-version: 21 + java-version: 25 distribution: 'corretto' cache: 'gradle' - name: Setup Gradle @@ -31,7 +31,7 @@ jobs: - uses: actions/setup-java@v6.0.1 with: distribution: 'corretto' - java-version: '21' + java-version: 25 cache: 'gradle' - name: Build with Gradle run: ./gradlew --parallel --continue spotlessCheck diff --git a/.github/workflows/nightlydeploy.yml b/.github/workflows/nightlydeploy.yml index 953ee83037a..1c0abb27674 100644 --- a/.github/workflows/nightlydeploy.yml +++ b/.github/workflows/nightlydeploy.yml @@ -10,7 +10,7 @@ permissions: id-token: write env: - JAVA_VERSION: 21 + JAVA_VERSION: 25 jobs: diff --git a/.github/workflows/release-tests.yml b/.github/workflows/release-tests.yml index 94ee5dfbcd2..e5ba0eb7259 100644 --- a/.github/workflows/release-tests.yml +++ b/.github/workflows/release-tests.yml @@ -15,7 +15,7 @@ jobs: fail-fast: false matrix: os: [ macos-latest, ubuntu-latest, windows-latest ] - java: [ 21, 25 ] + java: [ 25 ] continue-on-error: false runs-on: ${{ matrix.os }} env: @@ -72,7 +72,7 @@ jobs: matrix: test: [ testProveRules, testRunAllFunProofs, testRunAllInfProofs, testRunAllWdProofs, testProveSMTLemmas ] os: [ macos-latest, ubuntu-latest, windows-latest ] - java: [ 21, 25 ] + java: [ 25 ] z3: [ '4.15.4' ] cvc5: [ '1.3.2' ] @@ -119,7 +119,7 @@ jobs: matrix: test: [ testProveSMTLemmas, testStrictSMT ] os: [ macos-latest, ubuntu-latest, windows-latest ] - java: [ 21 ] + java: [ 25 ] z3: [ '4.13.4', '4.14.1', '4.15.4' ] cvc5: [ '1.3.2', '1.2.1' ] runs-on: ${{ matrix.os }} diff --git a/.github/workflows/tests.yml b/.github/workflows/tests.yml index afe4cef54c5..a4f44a81dea 100644 --- a/.github/workflows/tests.yml +++ b/.github/workflows/tests.yml @@ -24,12 +24,17 @@ jobs: fail-fast: false matrix: os: [ ubuntu-latest, windows-latest ] - java: [ 21 ] + java: [ 25 ] modules: [ keyext.exploration, keyext.slicing, key.ncore, key.ui, key.core, key.core.testgen, keyext.isabelletranslation, keyext.ui.testgen, key.ncore.calculus, key.util, key.core.example, keyext.caching, key.core.wd, key.core.infflow, - keyext.proofmanagement] + keyext.proofmanagement, + # JavaFX UI module and its six keyext ports (MP9.x): the unit tests are toolkit-free + # and headless-safe (the one panel test that needs the FX toolkit skips on + # display-less runners), see the per-module READMEs. + key.ui.fx, keyext.caching.fx, keyext.exploration.fx, keyext.isabelletranslation.fx, + keyext.slicing.fx, keyext.ui.testgen.fx, keyext.proofmanagement.fx] continue-on-error: true runs-on: ${{ matrix.os }} env: @@ -51,7 +56,7 @@ jobs: - name: cvc5 version run: cvc5 --version - - name: Set up JDK 21 + - name: Set up JDK 25 uses: actions/setup-java@v6.0.1 with: java-version: ${{ matrix.java }} @@ -86,11 +91,11 @@ jobs: matrix: test: [ testProveRules, testRunAllFunProofs, testRunAllInfProofs, testRunAllWdProofs, testMtStress, testMt2w, testMt4w ] os: [ ubuntu-latest ] - java: [ 21 ] + java: [ 25 ] runs-on: ${{ matrix.os }} steps: - uses: actions/checkout@v7 - - name: Set up JDK 21 + - name: Set up JDK 25 uses: actions/setup-java@v6.0.1 with: java-version: ${{ matrix.java }} diff --git a/.github/workflows/ui-verify.yml b/.github/workflows/ui-verify.yml new file mode 100644 index 00000000000..429ae58df22 --- /dev/null +++ b/.github/workflows/ui-verify.yml @@ -0,0 +1,76 @@ +name: UI verify sweep (key.ui.fx) + +# Full per-flag regression sweep of the JavaFX UI (WP-11 deliverable): every +# -Dkey.fx.verify.* hook of key.ui.fx runs headlessly against real example proofs inside an +# Xvfb display (software rendering). Maximum parallelization: ONE matrix job per flag +# (recipes in key.ui.fx/ci/verify-sweep.sh); the themepersist save+restore pair and the +# special runs (xdotool key dismissal, real-z3 SMT, natural-exit loadingexit) are single +# matrix entries with multiple runs inside. Logs are uploaded per flag. +on: + push: + branches: [ "main", "weigl/ocfx", "weigl/ocfx-wp11-endgame" ] + paths: + - "key.ui.fx/**" + - "keyext.caching.fx/**" + - "keyext.exploration.fx/**" + - "keyext.isabelletranslation.fx/**" + - "keyext.proofmanagement.fx/**" + - "keyext.slicing.fx/**" + - "keyext.ui.testgen.fx/**" + - ".github/workflows/ui-verify.yml" + workflow_dispatch: + +permissions: + contents: read + +jobs: + sweep: + runs-on: ubuntu-latest + timeout-minutes: 45 + strategy: + fail-fast: false + matrix: + flag: [ sequent, tree, goallist, notifications, docking, help, soundiness, + profileloading, javacsettings, termmenu, colors, shortcuts, sequentmenu, + dialogs, search, sequentsearch, sequentsearchmodes, treefilters, + tacletmatch, inputfreeze, updatehighlight, lemmaorigin, joinmerge, + joinmerge-gcd, proofmgmt-all, extensions, exploration, caching, prooftree, + slicing, testgen, heatmap, isabelle, sourceconsistency, autosave, + minimizeinteraction, themepersist, profileloadingdialog, smt, loadingexit, + proofdiff, drawer, drawerlayout, rightclickmacro ] + steps: + - uses: actions/checkout@v7 + + - name: Setup SMT solvers + uses: keyproject/setup-smt@v0 + with: + z3Version: 4.13.0 + + - name: Set up JDK 25 + uses: actions/setup-java@v6.0.1 + with: + java-version: 25 + distribution: 'corretto' + cache: 'gradle' + + - name: Setup Gradle + uses: gradle/actions/setup-gradle@v6 + + - name: Install Xvfb, xdotool (key dismissal), graphviz (slicing DOT render) + run: | + sudo apt-get update + sudo apt-get install -y --no-install-recommends xvfb xdotool graphviz + + - name: Run the UI verify sweep (${{ matrix.flag }}) + run: bash key.ui.fx/ci/verify-sweep.sh ${{ matrix.flag }} + + - name: Upload sweep logs (${{ matrix.flag }}) + uses: actions/upload-artifact@v7 + if: always() + with: + name: ui-verify-${{ matrix.flag }} + path: | + build/ui-verify/*.log + build/ui-verify/RESULTS.md + build/ui-verify/failed-flags.txt + if-no-files-found: error diff --git a/.gitignore b/.gitignore index b54d0ca8b9c..05a52134ad4 100644 --- a/.gitignore +++ b/.gitignore @@ -78,3 +78,6 @@ checkstyle-diff.txt # Java Flight Recorder output (e.g. runJfrProbe default mt-jfr-probe.jfr) *.jfr + +# Hermes tool cache (agent/tooling state; never version-controlled) +.hermes/ diff --git a/README.md b/README.md index f5718ef1522..bdd37b8e0b0 100644 --- a/README.md +++ b/README.md @@ -47,15 +47,35 @@ Additional and optional components are in `keyext.*/` folders. The file `build.g describing the dependencies and common build tasks for all subprojects. `key.util`, `key.core` and `key.ui` are the base for the product "KeY Prover". Special care is needed -if you plan to make changes here. +if you plan to make changes here. `key.ui.fx` is the JavaFX re-implementation of the user +interface and the **default entry point** of the application +(see [key.ui.fx/README.md](key.ui.fx/README.md)); the legacy Swing UI in `key.ui` stays +available until its retirement decision ([key.ui.fx/SWING-RETIREMENT.md](key.ui.fx/SWING-RETIREMENT.md)). ## Compile and Run KeY Assuming you are in the directory of this README file, you can create a runnable and deployable version with one of these commands: -1. With `./gradlew key.ui:run` you can run the user interface of KeY directly from the repository. - Use `./gradlew key.ui:run --args='--experimental'` to enable experimental features. +1. The JavaFX UI is the default way to run KeY's user interface directly from the repository: + ```sh + ./gradlew :key.ui.fx:run + ``` + This starts `de.uka.ilkd.key.core.fx.MainEx`. Use `./gradlew :key.ui.fx:runExperimental` + to enable experimental features. The `key.fx.*` demo/verification system properties, + the headless run recipe and the full documentation of the FX UI are in + [key.ui.fx/README.md](key.ui.fx/README.md). + + The legacy Swing UI remains available (documented as *legacy*) until its retirement + decision ([key.ui.fx/SWING-RETIREMENT.md](key.ui.fx/SWING-RETIREMENT.md)): + ```sh + ./gradlew key.ui:run --args='--experimental' + ``` + Generic `-DmainClass` ergonomics: the root project's `execute`/`executeInTests` tasks run + any main class, e.g. `-DmainClass=de.uka.ilkd.key.core.fx.MainEx ./gradlew :key.ui.fx:execute` + (FX) or `-DmainClass=de.uka.ilkd.key.core.Main ./gradlew :key.ui:execute` (legacy Swing). + The dedicated `run` tasks are preferred: they set `key.examples.dir` and (for `key.ui.fx`) + forward the whitelisted `key.fx.*` properties. 2. Use `./gradlew classes` to compile KeY, which includes running JavaCC and Antlr. Likewise, use `./gradlew testClasses` if you also want to compile the JUnit test classes. @@ -81,6 +101,9 @@ Assuming you are in the directory of this README file, you can create a runnable ``` The file is generated in `key.ui/build/libs/key-*-slim-exe.jar`. Both jars are also built as part of `./gradlew assemble`. + Note: these tasks package the **legacy Swing** product. The JavaFX UI currently runs via + `./gradlew :key.ui.fx:run`; its jlink/jpackage packaging is a later milestone (see the + packaging note in [key.ui.fx/README.md](key.ui.fx/README.md)). 5. A distribution is build with ```sh diff --git a/build.gradle b/build.gradle index 93b792ef77c..d2b6425d58f 100644 --- a/build.gradle +++ b/build.gradle @@ -69,8 +69,8 @@ subprojects { version = rootProject.version java { - sourceCompatibility = 21 - targetCompatibility = 21 + sourceCompatibility = 25 + targetCompatibility = 25 } repositories { @@ -109,8 +109,9 @@ subprojects { tasks.withType(JavaCompile).configureEach { // Setting UTF-8 as the java source encoding. options.encoding = "UTF-8" - // Setting the release to Java 21 - options.release = 21 + // Setting the release to Java 25 (also required by the JavaFX 25 jars, which are + // class-file version 67 = JDK 23+) + options.release = 25 } tasks.withType(Javadoc).configureEach { @@ -379,9 +380,9 @@ subprojects { tasks.register('start'){ - description = "Use :key.ui:run instead" + description = "Use :key.ui.fx:run (JavaFX UI, default) or :key.ui:run (legacy Swing UI) instead" doFirst { - println "Use :key.ui:run instead" + println "Use :key.ui.fx:run (JavaFX UI, default) or :key.ui:run (legacy Swing UI) instead" } } diff --git a/gradle/libs.versions.toml b/gradle/libs.versions.toml index 7ddff7e2730..096c10f233d 100644 --- a/gradle/libs.versions.toml +++ b/gradle/libs.versions.toml @@ -32,6 +32,14 @@ miglayout = "11.4.3" picocli = "4.7.7" docking-frames = "1.1.3p1" +# JavaFX user interface (key.ui.fx) +javafx = "25.0.4" +richtextfx = "0.11.7" +openjfx-plugin = "0.1.0" + +# Icon fonts (ikonli, kordamp.org/ikonli) — FontAwesome glyphs for the keyext FX ports +ikonli = "12.4.0" + # External tools scala-isabelle = "0.4.5" @@ -80,6 +88,17 @@ miglayout-swing = { module = "com.miglayout:miglayout-swing", version.ref = "mig docking-frames-common = { module = "org.key-project:docking-frames-common", version.ref = "docking-frames" } docking-frames-core = { module = "org.key-project:docking-frames-core", version.ref = "docking-frames" } +# JavaFX UI components (key.ui.fx) +richtextfx = { module = "org.fxmisc.richtext:richtextfx", version.ref = "richtextfx" } +javafx-base = { module = "org.openjfx:javafx-base", version.ref = "javafx" } +javafx-controls = { module = "org.openjfx:javafx-controls", version.ref = "javafx" } +javafx-graphics = { module = "org.openjfx:javafx-graphics", version.ref = "javafx" } +javafx-web = { module = "org.openjfx:javafx-web", version.ref = "javafx" } + +# ikonli — FontAwesome icon fonts (see kordamp.org/ikonli), used by the keyext FX ports +ikonli-javafx = { module = "org.kordamp.ikonli:ikonli-javafx", version.ref = "ikonli" } +ikonli-fontawesome6 = { module = "org.kordamp.ikonli:ikonli-fontawesome6-pack", version.ref = "ikonli" } + # CLI picocli = { module = "info.picocli:picocli", version.ref = "picocli" } @@ -98,4 +117,5 @@ spotless = { id = "com.diffplug.spotless", version.ref = "spotless" } checkerframework = { id = "org.checkerframework", version.ref = "checkerframework-gradle" } maven-publish = { id = "com.vanniktech.maven.publish", version.ref = "maven-publish" } shadow = { id = "com.gradleup.shadow", version.ref = "shadow" } -license-report = { id = "com.github.jk1.dependency-license-report", version = "3.1.4" } \ No newline at end of file +license-report = { id = "com.github.jk1.dependency-license-report", version = "3.1.4" } +openjfx = { id = "org.openjfx.javafxplugin", version.ref = "openjfx-plugin" } \ No newline at end of file diff --git a/key.ui.fx/KNOWN-SIMPLIFIED.md b/key.ui.fx/KNOWN-SIMPLIFIED.md new file mode 100644 index 00000000000..1929efcb487 --- /dev/null +++ b/key.ui.fx/KNOWN-SIMPLIFIED.md @@ -0,0 +1,154 @@ +# Consolidated ledger of KNOWN-SIMPLIFIED deviations + +Every deliberate deviation of the JavaFX UI from its Swing original is marked at the source site +with a `KNOWN-SIMPLIFIED` comment or `KNOWN-SIMPLIFIED:` javadoc block. This file is the +single consolidated ledger: one row per marker, for `key.ui.fx` and all six keyext ports +(MP9.1–9.6). Row references are `Class.java:line` and point at the marker itself, which carries +the full sentence. + +Marker counts per module: + +| Module | Markers | +|---|---| +| `key.ui.fx` (contrib extensions + SMT run UI + exit flow + input freeze) | 7 | +| `keyext.caching.fx` | 10 | +| `keyext.exploration.fx` | 9 | +| `keyext.isabelletranslation.fx` | 4 | +| `keyext.slicing.fx` | 16 | +| `keyext.ui.testgen.fx` | 18 | +| `keyext.proofmanagement.fx` | 4 | +| **Total** | **68** | + +To re-derive this table at any point: `grep -rn 'KNOWN-SIMPLIFIED' */src/main */src/test`. + +The status column is for the close-out tracking: **OPEN** items are candidates for a later +milestone, **FIXED-UPSTREAM** items differ from a Swing bug that the port deliberately corrects, +**WONT-REPLICATE** items depend on Swing-only machinery with no FX counterpart. + +**Ledger status (WP-11 close-out, 2026-10-12):** no row is OPEN. Every row ends RESOLVED (with +its batch/WP reference), WONT-REPLICATE or FIXED-UPSTREAM; the rows marked "—" record deliberate +simplifications that never needed close-out tracking (faithful-port notes, test-design notes, +site-specific decisions like the owner-less file chooser). The marker-count table above reflects +the original audit inventory; as rows were resolved during the P-batches and WP-1…WP-10, some +per-site markers were consolidated into summary javadoc blocks (e.g. `ExplorationExtensionF`), +so a raw `grep` count today is lower than the original 68. The behaviour-level counterpart of +this ledger is `PARITY-SIGNOFF.md` (closed, incl. the deliberate per-feature deferrals such as +the SMT select menu, WP-7); the module-level removal plan for the Swing side is +`SWING-RETIREMENT.md`. + +--- + +## `key.ui.fx` — built-in contrib extensions (3) + +| Site | Swing original | FX port | Status | +|---|---|---|---| +| `extension/contrib/HeatmapF.java:28` | `HeatmapExt` renders the heat highlight into the sequent views (`SequentView.updateHeatMapHighlights`, called from `CurrentGoalView:197`/`InnerNodeView:241` — the proof tree is NOT touched, the ledger's earlier "proof tree / sequent" wording was imprecise) | RESOLVED (WP-2): the age-heatmap renderer is ported onto `SequentViewF` (`rebuildHeatmapOverlays` + `updateHeatmapSFHighlights`/`updateHeatmapTermHighlights` parity — formula ages up the ancestor chain, `SequentChangeInfo`-based term ages, `computeColorForAge` opacity interpolation from `[Heatmap]basecolor` via `ColorPaletteF.HEATMAP_BASE_COLOR`); the menu/toolbar toggle re-prints the sequent like Swing `HeatmapToggleAction.actionPerformed`; `key.fx.verify.heatmap` PASS on `strassen.auto.0.proof` (sfAge=1 sfNewest=5 termsAge=6 termsNewest=3 off=0) | RESOLVED (WP-2) | +| `extension/contrib/HeatmapF.java:37` | — (doubles the `@Info` description) | same surface as the row above — the extension dialog description no longer documents a deferral | RESOLVED (WP-2) | +| `extension/contrib/ParallelProverStatusIndicatorF.java:27` | toggle button "SC" / "MT N×" with left-click toggle and right-click worker-count menu | RESOLVED (WP-3): `Button` with the Swing "SC"/"MT Nx" text format, left-click toggles through the real `onAction` handler (Swing `ParallelProverStatusIndicator` action), right-click opens a `ContextMenu` with the Single-core radio + "Multi-core, N workers" items for the `TreeSet{2, 4, 8, cores}` counts (Swing ParallelProverStatusIndicator.java:92-121); the FX auto-mode state is folded into the tooltip ("Auto mode running."/"Idle." prefixes) | RESOLVED (WP-3) | + +## `key.ui.fx` — SMT run UI + exit flow + input freeze (4) + +| Site | Swing original | FX port | Status | +|---|---|---|---| +| `SolverListenerF.java:81` | results applied via `SMTProofApplyUserAction` (undoable history entry) with the `stopInterface` input freeze around it | RESOLVED (WP-7): `SolverListenerF.applyResults` runs `SMTProofApplyUserActionF.actionPerformed()` — the `UserActionF` port (name "Close: %d goals by SMT", undo = prune to the original nodes + default selection, canUndo = all applied nodes still findable) executed inside the mediator auto-mode context with `stopInterface` freeze around it (Swing SolverListener.java:209-221 parity); the `UserActionListenerF` seam (`KeYMediatorF.addUserActionListener/fireActionPerformed`) is asserted by the undoable-apply extension of `key.fx.verify.smt` (freeze events, undo re-opens a goal) | RESOLVED (WP-7) | +| `InformationWindowF.java:24` | counterexample model tree (`CETree`) with line numbers (`TextLineNumber`) and the counterexample help tab | RESOLVED (WP-7): the counterexample tabs are ported — the `CETreeF` model tree (double-click expansion of `#o`/`#l`/`#s` reference leaves, `IGNORECASE_COMPARATOR` rows), the Help tab (`CE_HELP` text) and a simple line-number gutter for the information tabs (FX has no `TextLineNumber`); the window retitles to "Counterexample ..." for the Z3 CE solver with a model (Swing InformationWindow.initModel, :88-101); asserted by `key.fx.verify.testgen` | RESOLVED (WP-7) | +| `MainWindowF.java:3721` | exit fires the mediator shutdown event (`fireShutDown` → `GUIListener.shutDown`) | RESOLVED (WP-1): `KeYMediatorF` has the GUI-listener registry (`GUIListenerF`, `addGUIListener`/`removeGUIListener`, Swing `KeYMediator.java:306-410`) and the exit flow fires the event (`mediator.fireShutDown(new EventObject(this))`); the Swing listener's window-hiding is the `Platform.exit` of the flow | RESOLVED (WP-1) | +| `MainWindowF.java:2659` | the glass pane covered the whole content pane and re-delivered events only to components marked `isAutoButton` (automation/stop buttons + status-line abort button) | WONT-REPLICATE (WP-1 decision): the overlay keeps covering only the views area (workspace + drawers). The menu bar/toolbar proof actions are disabled during auto mode anyway (enablement binds to `mediator.autoModeRunningProperty()`), so blocking clicks on inert controls adds no protection; the automation macro items are enabled during auto mode by Swing parity so a click stops the run (MacroAutomationAction.java:48-61) and blocking them would regress that intent; the status bar must stay live for the progress display; and the stop controls the Swing glass pane kept live are the same controls the FX toolbar keeps live | WONT-REPLICATE (WP-1) | + +## `keyext.caching.fx` (10) + +| Site | Swing original | FX port | Status | +|---|---|---|---| +| `CachingExtensionF.java:95` | `CachingSettingsProvider.getCachingSettings()` on the keyext compile path | the FX module owns the `ProofCachingSettings` singleton via `CachingSettingsProviderF.getCachingSettings()` (Swing provider not loadable on the FX compile path) | FIXED-UPSTREAM | +| `CachingExtensionF.java:129` | menu checkbox instantiated eagerly | created lazily on first use (constructing controls needs the FX toolkit; the SPI may instantiate the provider headless) | — | +| `CachingExtensionF.java:735` | opens the interactive `ReferenceSearchDialog` (per-goal table + "Apply") | RESOLVED (WP-4): the dialog is ported as `ReferenceSearchDialogF` (per-goal `TableView` snapshot like Swing `ReferenceSearchTable`, "Close"/"Apply" button row, progress label/bar) and opened by the status-button click; the "Apply" action copies the referenced steps via `DefaultReferenceSearchDialogListenerF` (core `CopyReferenceResolver` inside the mediator auto-mode context + statistics window); asserted by `key.fx.verify.caching` | RESOLVED (WP-4) | +| `CachingExtensionF.java:778` | feeds `mediator.getCurrentlyOpenedProofs()` to the reference search | RESOLVED (WP-4): `openedProofs()` returns the live WP-1 seam list (`KeYMediatorF.getCurrentlyOpenedProofs()`, kept live by the `ProofManagerF` sync in `MainWindowF`); the extension's tracked proofs remain only the toolkit-free fallback | RESOLVED (WP-4) | +| `CachingPruneHandlerF.java:26` | iterates `mediator.getCurrentlyOpenedProofs()` | RESOLVED (WP-4): iterates `CachingExtensionF.openedProofs()` (the WP-1 seam list) like Swing `CachingPruneHandler.java:51` | RESOLVED (WP-4) | +| `CachingSettingsProviderF.java:37` | keyext registers the caching settings into `ProofIndependentSettings` | the FX module owns and registers the same singleton itself (shared persisted object with the Swing keyext via the registry) | — | +| `CachingSettingsProviderF.java:109` | writes `strategySearch.isEnabled()` (latent Swing bug — `JCheckBox#isEnabled` always true, persisted `true`) | writes the checkbox *selection* — the behaviour the panel visibly offers | FIXED-UPSTREAM | +| `CopyBeforeDisposeF.java:25` | wraps the copy into `mediator.initiateAutoMode(...)`/`finishAutoMode(...)` | RESOLVED (WP-4): the copy is wrapped into the WP-1 auto-mode context API (`initiateAutoMode(newProof, true, false)` around the copy, `finishAutoMode(newProof, true, true, () -> {})` in the finally, Swing CachingExtension.java:312-319 parity); the direct resolver call remains only the null-mediator (toolkit-free) fallback | RESOLVED (WP-4) | +| `CachingExtensionFTest.java:27` | — (test design) | unit tests are toolkit-free; control-level SPI contracts are verified by the in-app `key.fx.verify.extensions` hook | — | +| `CachingExtensionFTest.java:69` | — (test design) | asserts the FX-module-owned singleton identity and registry idempotence | — | + +## `keyext.exploration.fx` (9) + +| Site | Swing original | FX port | Status | +|---|---|---|---| +| `ExplorationExtensionF.java:54` | registers `ExplorationModeModel` in the mediator registry and an `ExplorationRenderer` (purple border) into the proof tree | RESOLVED (WP-5): the provider registers the model through the WP-1 seam (`mediator.register(model, ExplorationModeModel.class)`, consumers look it up; the provider-held singleton stays as the fallback for consumers without a mediator) and registers the `ExplorationRendererF` cell styler (the purple border/background + "Exploration Action Performed" tooltip title on nodes carrying `ExplorationNodeData`) through the new `ProofTreeViewF` renderer-styling hook (`CellStyler`/`Style`, Swing `Styler` parity) | RESOLVED (WP-5) | +| `ExplorationExtensionF.java:76` | — (extension description) | RESOLVED (WP-5): the restated decision is superseded — proof-tree styling is the `ProofTreeViewF.CellStyler` hook and the hidden second-branch filter routes through the (P3a-implemented) `HIDE_INTERACTIVE_GOALS` filter; the extension description states the parity | RESOLVED (WP-5) | +| `ExplorationExtensionF.java:280` | `mediator.register(model, ExplorationModeModel.class)` | RESOLVED (WP-5): the `init` hook registers the model through the WP-1 `KeYMediatorF.register/lookup` seam; the provider keeps holding the singleton as the lookup fallback (verified by `key.fx.verify.exploration` + the toolkit-free `initRegistersModelInMediatorRegistry` test) | RESOLVED (WP-5) | +| `ExplorationExtensionF.java:363` | "Hide justification" routes through the proof-tree filter `HIDE_INTERACTIVE_GOALS` | RESOLVED (WP-5): the toggle routes through `ProofTreeViewF.applyHideInteractiveGoals` — the same persisted `ViewSettings#setHideInteractiveGoals` flag the FX `HIDE_INTERACTIVE_GOALS` filter honours (P3a) plus the tree rebuild (Swing `ExplorationModeModel.setShowInteractiveBranches` → `GUIProofTreeModel.setFilter` parity) | RESOLVED (WP-5) | +| `ExplorationSequentMenuF.java:48` | `promptForTerm` modal retry-loop until the term is well-typed | RESOLVED (WP-5): faithful port of the Swing retry-loop (ExplorationAction.java:35-65) — the input dialog re-opens until a well-typed term of the required sort is entered; the dialog/error surface sits behind the `PromptHandler` seam for headless unit tests | RESOLVED (WP-5) | +| `ExplorationSequentMenuF.java:173` | sort-mismatch dialog, then re-opens the input dialog | RESOLVED (WP-5): the loop shows the "Sort mismatch" error and re-prompts (unit test `retryAfterSortMismatch`, in-app `key.fx.verify.exploration` accepts bad-then-good input) | RESOLVED (WP-5) | +| `ExplorationSequentMenuF.java:182` | malformed input re-prompts | RESOLVED (WP-5): the loop shows the "Malformed input" error and re-prompts (unit test `retryAcceptsBadThenGoodInput`) | RESOLVED (WP-5) | +| `ExplorationStepsPanelF.java:56` | `Icons` (AWT/Swing) tab help button; icon images | help button not ported; status indicator uses ikonli FontAwesome solid/regular compass; pruning via `MainWindowF.getUserInterfaceControl().getProofControl()` | — | +| `ExplorationStepsPanelF.java:326` | prunes via `mediator.getUI().getProofControl()` | FX counterpart via the window's user-interface control; headless runs no-op | — | + +## `keyext.isabelletranslation.fx` (4) + +| Site | Swing original | FX port | Status | +|---|---|---|---| +| `IsabelleTranslationExtensionF.java:37` | `IsabelleTranslationAction.solveGoals` hands the generated theory to the external Isabelle solver (`IsabelleLauncher`) with a progress/model dialog | theories handed to the `IsabelleLauncher` on a background thread with the JavaFX progress dialog port (`IsabelleSolverProgressDialogF` + `IsabelleLauncherProgressDialogMediatorF`); launch failures show a "Launch failed!" alert and keep the theories accessible in the translation dialog | RESOLVED (WP-8): solver launch + JavaFX progress dialog port added; verify = `key.fx.verify.isabelle` DRY-RUN (fake solvers, no real Isabelle installation, scala-isabelle backend stays unloaded) | +| `IsabelleTranslationExtensionF.java:48` | — (extension description) | extension description now states the solver launch + progress dialog | RESOLVED (WP-8): restated row, see `IsabelleTranslationExtensionF.java:37` | +| `IsabelleTranslationRunnerF.java:28` | solver run + progress/model dialog | the runner translates on the background thread and then calls `IsabelleLauncher.launch(problems, timeout, 1)` like Swing; `IsabelleLauncher` is plain Java (only `IsabelleResourceController`/`IsabelleSledgehammerSolver` bodies touch `de.unruh.isabelle`, loaded lazily at launch execution) | RESOLVED (WP-8): solver run + progress/model dialog ported; sub-simplification: Apply closes solved goals directly without the undoable Swing `UserAction` wrapper (at WP-8 time the FX mediator API had no user-action seam; WP-7 added the `UserActionF` seam afterwards — see `SolverListenerF.java:81`) | +| `IsabelleSettingsProviderF.java:191` | reads the keyext configuration constants | the constants (`isabellePathKey`/`translationPathKey`/`timeoutKey`) are package-protected in keyext; their stable string values are mirrored here | — | + +## `keyext.slicing.fx` (16) + +| Site | Swing original | FX port | Status | +|---|---|---|---| +| `SlicingExtensionF.java:49` | registers a proof-load listener through the Swing mediator | ported the same `this::createTrackerForProof` registration through the WP-1 `KeYMediatorF.registerProofLoadListener`/`fireProofLoaded` registry (fired from `WindowUserInterfaceControlF.registerProofAggregate` like Swing WindowUserInterfaceControl.java:522); the `KeYSelectionListener` stays for the "selected proof switched" case, like Swing | — | +| `SlicingExtensionF.java:249` | "Show dependency graph around this formula" renders the DOT excerpt through `PreviewDialog`/graphviz | RESOLVED (WP-6): the DOT excerpt is rendered by the graphviz `dot` binary (non-Swing `GraphvizDotExecutorF`, PNG into the FX `PreviewDialogF` image dialog); on render failure the DOT-source text dialog remains as the documented fallback | RESOLVED (WP-6) | +| `SlicingSettingsProviderF.java:29` | `SlicingSettings.setAggressiveDeduplicate` callable (same package) | WONT-REPLICATE (WP-6): the setter is package-private in `org.key_project.slicing` and this module may not modify keyext.slicing (no reflection hacks); the toggle reflects but does not persist the flag — resolving it needs an upstream keyext change (make the setter public) | WONT-REPLICATE (WP-6) | +| `SlicingSettingsProviderF.java:144` | writes the aggressive-deduplicate flag | WONT-REPLICATE (WP-6): same package-private-setter constraint as row `:29`; the other two options persist normally | WONT-REPLICATE (WP-6) | +| `SlicingLeftPanelF.java:59` | panel summary: graphviz rendering, iterative fixed point, HTML statistics/timings | RESOLVED (WP-6): graphviz image rendering (with DOT-text fallback), iterative fixed-point dialog, HTML statistics dialog with four sort orders and the HtmlFactory timings table are all ported (remaining simplifications are documented in the panel javadoc) | RESOLVED (WP-6) | +| `SlicingLeftPanelF.java:222` | "Slice proof to fixed point" opens the iterative `SliceToFixedPointDialog` | RESOLVED (WP-6): opens the FX port `SliceToFixedPointDialogF`, which iterates analyze/slice/load until no more steps can be removed (Swing worker/selection-listener choreography) | RESOLVED (WP-6) | +| `SlicingLeftPanelF.java:228` | — (tooltip for the fixed-point button) | RESOLVED (WP-6): tooltip now describes the real iterative behavior | RESOLVED (WP-6) | +| `SlicingLeftPanelF.java:270` | file chooser with parent component | owner-less `FileChooser` (the drawer panel has no dedicated window) | — | +| `SlicingLeftPanelF.java:295` | rule statistics as HTML table with four sort buttons | RESOLVED (WP-6): the HTML table (reused `HtmlFactory.generateTable`) renders in the `RuleStatisticsDialogF` WebView seam with the four Swing sort buttons (name / total / useless / initial useless) | RESOLVED (WP-6) | +| `SlicingLeftPanelF.java:322` | renders the DOT to a PNG via the Swing graphviz executor and shows an image dialog | RESOLVED (WP-6): non-Swing `GraphvizDotExecutorF` runs the configured `dot` binary and the PNG shows in the FX `PreviewDialogF` (ImageView/ScrollPane; the pan-zoom view is simplified); render failure falls back to the DOT-source text dialog; the button is disabled without graphviz like in Swing | RESOLVED (WP-6) | +| `SlicingLeftPanelF.java:377` | passes a headless `DefaultUserInterfaceControl` to the slicer | uses the FX window's own user-interface control (`ProblemLoaderControl`) so the loader callbacks stay FX-safe | — | +| `SlicingLeftPanelF.java:415` | loads the slice through the problem loader directly (keeps it out of the recent-files list) | RESOLVED (WP-6): the slice load goes through the new `MainWindowF.loadProofFileDirect` (the direct loader pipeline without the recent-files registration of `openProofFile`, Swing parity of the `UI.loadProblem` bypass); asserted by the `key.fx.verify.slicing` hook | RESOLVED (WP-6) | +| `SlicingLeftPanelF.java:464` | execution timings as HTML table via `HtmlFactory` | RESOLVED (WP-6): the timings render as an `HtmlFactory` "Algorithm/Time" table in a WebView inside the timings pane (one reused WebView, the Swing `JEditorPane` counterpart) | RESOLVED (WP-6) | +| `SlicingLeftPanelF.java:541` | panel grey-out via the Swing-only `SingleCoreFeatureGate` | checks the parallel-prover setting directly and disables the panel recursively | — | +| `SlicingLeftPanelF.java:618` | `HtmlDialog`/`PreviewDialog` | RESOLVED (WP-6): the Swing `HtmlDialog` and `PreviewDialog` have FX ports (`HtmlDialogF` WebView seam, `PreviewDialogF` image dialog); the text dialog remains only as the documented graphviz-failure fallback | RESOLVED (WP-6) | +| `SlicingExtensionFTest.java:27` | — (test design) | unit tests are toolkit-free; the provider's JavaFX widget contributions are verified in-app | — | + +## `keyext.ui.testgen.fx` (18) + +| Site | Swing original | FX port | Status | +|---|---|---|---| +| `TestgenExtensionF.java:59` | implements `Toolbar` and `Startup` in addition to the menu | RESOLVED (WP-7): the extension implements `KeYGuiExtensionF.ToolbarF` + `StartupF` like Swing — the two actions are the plain `Button`s contributed through `getToolbarControls` and the window is captured at startup; the status-line `MenuButton` stand-in is dropped; asserted by the toolkit-free `capabilitySurface` test and `key.fx.verify.testgen` | RESOLVED (WP-7) | +| `TestgenExtensionF.java:72` | window arrives via `Startup`/toolbar | RESOLVED (WP-7): the `StartupF.init(window, mediator)` hook (plus the toolbar hook) hands the window to the extension at app startup, so the enablement listeners wire from the start; the settings panel remains the toolkit-free fallback capture | RESOLVED (WP-7) | +| `TestgenExtensionF.java:133` | — (field doc) | the window field stays a plain `Object` (`MainWindowF` is not nameable in this module); it is captured at startup through the `StartupF`/`ToolbarF` hooks (WP-7) | — | +| `TestgenExtensionF.java:155` | toolbar in the JToolBar | RESOLVED (WP-7): the two plain buttons of the Swing JToolBar, contributed through the `ToolbarF` hook; the status-line `MenuButton` stand-in is dropped | — | +| `TestgenExtensionF.java:193` | `SHORTCUT+T` bound via `KeyStrokeSettings` on the TestGen strategy macro (term context menu) | RESOLVED (WP-7): the `TestGenMacro` default (real FQN `de.uka.ilkd.key.testgen.macros.TestGenMacro`, Ctrl+Shift+T) is registered in the shared `KeyStrokeManagerF` (`defineDefault`) and drives the generate item's accelerator (`manager.binding(...).ifPresent(setAccelerator)` + `manager.register(item, id)`); asserted by `testGenMacroShortcutBinding` and `key.fx.verify.testgen` | RESOLVED (WP-7) | +| `TestgenExtensionF.java:344` | enabled-state updates via the Swing action infrastructure | RESOLVED (WP-7): with the startup capture the enablement listeners (selection, auto mode, SMT settings) wire from the start — the controls disable during runs (auto mode) and enable for a loaded proof with an installed z3 CE solver | RESOLVED (WP-7) | +| `TestgenSettingsProviderF.java:40` | settings provider with a named `MainWindowF` | `SettingsProviderF.getPanel/apply` declare `MainWindowF`, and naming it forces javac to complete `KeYEnvironment`'s class file, which fails on this module's classpath — the provider is a `java.lang.reflect.Proxy` that forwards the window as plain `Object` | — | +| `TestgenSettingsProviderF.java:50` | panel subclasses the Swing `SettingsPanel` base (row/validator/chooser helpers, working-copy change listeners) | plain `GridPane` of label/input rows (host wraps it in a `ScrollPane`) | — | +| `TestgenReflectionF.java:160` | `TGWorker` wraps the run in the mediator's auto-mode machinery with an immediate `StopRequest`/`SolverLauncher` stop | RESOLVED (WP-7): `generateTestcases` builds its own `SolverLauncher` and hands the handle to the caller via `launcherRef` (the Swing `stopSMTLauncher` parity, the facade hid its launcher) and every phase is guarded by a `shouldStop` flag (the cooperative `StopRequest` parity); the auto-mode shell lives in `TestGenerationTaskF` | RESOLVED (WP-7) | +| `TestgenReflectionF.java:220` | `SolverListener` opens a modal progress dialog and a results dialog showing the counterexample model | RESOLVED (WP-7): the CE search routes its `SolverLauncherListener` through the `SolverListenerFactoryF` hook answered by `CounterExampleTaskF` with a `SolverListenerF` — the modal progress dialog and the results/counterexample-model dialogs like Swing `SolverListener`; the reflective log-only listener is deleted | RESOLVED (WP-7) | +| `TestGenerationTaskF.java:19` | worker puts the original proof into auto-mode machinery and stops cooperatively | RESOLVED (WP-7): typed `Proof`/`KeYMediatorF` auto-mode shell (`initiateAutoMode` in `call`, `finishAutoMode` in the terminal-state hooks, the Swing `TGWorker.start/done` parity) and cooperative stop (`shouldStop` between the phases, `SolverLauncher` stop + worker-interrupt backup, the `interruptionPerformed` parity) | RESOLVED (WP-7) | +| `TestGenResultsDialogF.java:43` | dialog embeds a live `TestgenOptionsPanel` on its eastern edge | RESOLVED (WP-7): the dialog embeds the `TestgenOptionsPanelF` on its right edge (`root.setRight`, TGInfoDialog.java:126 parity) — KNOWN-SIMPLIFIED: the embedded panel writes into the global settings live (the Swing working copy was never applied from the run dialog, so its edits were lost — deliberate FX change); "Close" is disabled during the run like Swing; the generated-files list is a recursive listing of the output folder (Swing only logs "Writing test file") | RESOLVED (WP-7) | +| `TestGenResultsDialogF.java:154` | window available from the start | RESOLVED (WP-7): the window arrives at startup through the `StartupF` hook, so the run starts normally; the null-window hint remains the toolkit-free fallback path | RESOLVED (WP-7) | +| `CounterExampleTaskF.java:21` | `SolverListener` modal progress + results dialogs with the counterexample model; auto-mode shell | RESOLVED (WP-7): the auto-mode shell is restored (the Swing `CEWorker.start/done` parity: `initiateAutoMode` in `call`, `finishAutoMode` in the terminal hooks) and the listener route answers a `SolverListenerF` (the modal progress dialog + CE model dialogs) | RESOLVED (WP-7) | +| `CounterExampleResultsDialogF.java:35` | counterexample model shown in modal result dialogs | RESOLVED (WP-7): the counterexample model is shown in the `SolverListenerF` result dialogs (`InformationWindowF` with the `CETreeF` model tree); the run dialog keeps the pipeline log (side proof, semantics blasting) as documented | RESOLVED (WP-7) | +| `CounterExampleResultsDialogF.java:131` | window available from the start | RESOLVED (WP-7): the window is available from startup through the `StartupF` hook; the validated-on-click path remains the toolkit-free fallback | RESOLVED (WP-7) | +| `TestgenExtensionFTest.java:24` | — (test design) | unit tests are toolkit-free; control trees are asserted in-app only | — | +| `TestgenExtensionFTest.java:52` | — (test design) | asserts that `ToolbarF`/`StartupF` are implemented (WP-7) | — | + +## `keyext.proofmanagement.fx` (4) + +| Site | Swing original | FX port | Status | +|---|---|---|---| +| `CheckConfigDialogF.java:45` | `BlockingGlassPane` blocks input while the check runs (Stop-only pass-through) | explicitly disables the input controls while the check runs; "Run checkers" becomes "Stop" (the only enabled control); cancelling may leave partial output like the original | — | +| `CheckConfigDialogF.java:50` | bundle/report choosers via AWT `KeYFileChooser` with `.zproof`/`.html` filters | `FileChooser` with equivalent extension filters; file-only selection matches the Swing dialog | — | +| `CheckConfigDialogF.java:55` | opens the generated report via `Desktop.getDesktop().open` | opens it through the `HelpFacadeF` browser seam (`openExternal`, host services with a desktop fallback) — no AWT/Swing | — | +| `CheckConfigDialogF.java:212` | in-dialog browser/help | `HelpFacadeF` browser seam — see the class javadoc | — | + +--- + +**What this ledger does not track:** ordinary porting work that is *faithful* to the Swing +original (the vast majority of the ~490 audited behaviors) and the deliberate feature additions +of the FX port (e.g. working search, editable dark theme column, extension status indicators). +Those are covered by `PARITY-SIGNOFF.md` and the per-module READMEs. diff --git a/key.ui.fx/PARITY-SIGNOFF.md b/key.ui.fx/PARITY-SIGNOFF.md new file mode 100644 index 00000000000..65ab3f28b95 --- /dev/null +++ b/key.ui.fx/PARITY-SIGNOFF.md @@ -0,0 +1,431 @@ +# Parity sign-off — Swing→JavaFX audit (2026-10-08) vs. delivered application + +This document signs off the parity audit that was carried out on 2026-10-08 against the +in-development JavaFX UI. The audit inventoried ~490 behaviors across nine components +(report index: `/tmp/opencode/parity-*.md`, synthesis in the appended table). + +**Warning:** the audit predates milestones MP7–MP10 and the MP9.x keyext ports, so a large share +of the "MISSING" entries have since been delivered. This sign-off re-states each gap against the +delivered application and the `key.fx.verify.*` regression hooks, and carries forward everything +still open into the close-out list at the end. + +Evidence used: the MP9 combined regression run (16/16 PASS), menuparity 5/5, termmenu 25, +tacletmatch 9/9, uicontrol 4/4, the six MP9.x module ports, and the consolidated +[KNOWN-SIMPLIFIED ledger](KNOWN-SIMPLIFIED.md). Items without an app-level regression hook are +marked `OPEN (unverified)` rather than assumed fixed. + +## Component verdicts + +| Component (audit report) | Behaviors | Audit verdict | Resolution since | Current status | +|---|---|---|---|---| +| mainwindow | 62 | 13 PORTED / 24 PARTIAL / **17 MISSING** / 6 KNOWN-DEF | window shell, menu/toolbar/status parity, docking, drawers (MP1–MP10) | mostly resolved; open items below | +| prooftree | 53 | 20 / 8 / **13 MISSING** / 5 KNOWN-DEF | core tree faithful; P3a sweep items, WP-10 click-target + Apply-Strategy, WP-2 heatmap/NodeInfoVisualizer/branch editing | RESOLVED (remaining gaps documented in KNOWN-SIMPLIFIED) | +| sequent | 45 | 14 / 10 / **15 MISSING** / 4 KNOWN-DEF | term context menu + taclet application + search (MP8); multi-selection highlight + reprint persistence (WP-3) | context menu RESOLVED; user-selection highlight + reprint persistence RESOLVED (WP-3 `key.fx.verify.sequent`); remaining items below | +| interactive-completion | 25 | 0 / 0 / **20 MISSING** | `WindowUserInterfaceControlF` seam + tacletmatch + join/merge | RESOLVED (was the top P0; evidence uicontrol + tacletmatch 9/9) | +| goallist-strategy-info | 37 | goal list at parity; strategy preset UI missing; info view re-designed | strategy preset combo / stash UI ported (WP-3: the Swing `StrategySelectionView.createDefaultPanel` [⚙][combo][Apply] row with Defaults + built-ins + user presets, save/stash/rename/delete over `StrategyPresetsSettings`, Apply writes maxSteps + properties like Swing :572-585; `key.fx.verify.goallist` preset round trip PASS) | stats staleness KNOWN-DEFERRED (deliberate): `InfoViewF` observes `selectedProofChanged` only (`InfoViewF.java:94-99`) — the statistics go stale after interactive rule applications until the next proof change/auto-mode stop (Swing `InfoView.java:83-111` refreshes on node changes too); per-feature deferral, outside the WP-1…WP-10 scope | +| source-search-filechooser | 74 | 30 / 5 / **28 MISSING** | search bars + loading-options dialog ported | source-view interaction (symbex highlights, cross-highlight) KNOWN-DEFERRED (deliberate, documented at `SourceViewF.java:64-66/:110/:237` — the tab-per-file UI, the proof-node ↔ source-line symbex highlights and the sequent-hover origin cross-highlight stay deferred; per-feature deferral, outside the WP-1…WP-10 scope) | +| menus-actions | 57 leaves | ~25 MISSING | menu parity 5/5 (File 16 / Proof 24 / Options 12 / View 7 / About 5) plus automation submenu | RESOLVED at surface level; a few behaviours below | +| settings-config | 117 | 83 / 8 / 11 MISSING / 13 KNOWN-DEF | settings framework + providers + colors mechanics + search; theme persistence (WP-3: `ThemeManager` persists the choice to the user preference node, restore at startup, `key.fx.theme` stays the one-off override; `key.fx.verify.themepersist` save/restore round trip PASS) | color definitions + SMT run UI RESOLVED (P1); theme persistence RESOLVED (WP-3) | +| unported-dialogs | 18 | 13 MISSING / 2 PARTIAL | proofmgmt, tacletmatch, IssueDialog, notification, Loaded Proofs | RESOLVED where noted below; join/mergerule/lemmatagenerator/etc. track their MP9.x modules | + +## P0 sign-off (the audit's "prover workflow critical" list) + +| Audit item | Delivered in | Evidence | Status | +|---|---|---|---| +| `UserInterfaceControlF` seam (status/progress/task/exception callbacks, `RuleCompletionHandler`) | `WindowUserInterfaceControlF` + diamond issue/LogView/AutoDismiss | `key.fx.verify.uicontrol` 4/4 (`wasShown=true` for the exception dialog) | **RESOLVED** | +| Sequent term context menu (`CurrentGoalViewMenu` ~900 LOC) | `SequentTermContextMenuF` + `SequentMenuModelF` | `key.fx.verify.termmenu` 25 checks; interactive rule apps in-app | **RESOLVED** | +| TacletMatch suite (gates interactive rule application) | `TacletMatchDialogF` + panels | `key.fx.verify.tacletmatch` 9/9 | **RESOLVED** | +| Abandon Proof | Proof menu (24 items) | `key.fx.verify.menuparity` Proof 24 | **RESOLVED** | +| ProofManagementDialog + TaskTree / Loaded Proofs dockable | `keyext.proofmanagement.fx` (MP9.6) + Loaded Proofs view | `key.fx.verify.proofmgmt` 1/2 | **RESOLVED** | +| IssueDialog / error reporting | `IssueDialogF` (toasts + dialog) | `key.fx.verify.uicontrol` (exception leg) | **RESOLVED** | +| Goal Back / Prune disable bindings; input freeze during auto mode | **RESOLVED** (P1: the auto mode blocking overlay — main area covered, mouse input blocked, keys swallowed except Escape, wait cursor; wired to the auto mode listener incl. the demo-live stop path; `key.fx.verify.inputfreeze` PASS) | — | **RESOLVED** | +| Apply Strategy on node + Prune-at-node in the tree popup | **RESOLVED** (WP-10: the popup's Apply Strategy / Prune actions run on the clicked node — the popup context is built from the clicked row like Swing `ProofTreeView.mousePressed` (`getPathForLocation` + `setSelectionPath`), not from the selection; `key.fx.verify.prooftree` asserts the real handlers: popup on the clicked node with the selection parked elsewhere, a capped strategy run grows the clicked node's subtree (nodes 1->21) and the prune removes it again (20->1) — "PASS - popup on clicked node … prune 20->1") | — | **RESOLVED** | + +P0 bugs from the audit: + +| Bug | Status | +|---|---| +| FX search stale on node switch | **RESOLVED** (search re-runs on reprint; sequent-leftovers milestone `18df960b35`) | +| Proof-tree context menu acts on the selection, not the clicked node | **RESOLVED** (WP-10: the context-request handler resolves the clicked row from the event-target `TreeCell` — the FX counterpart of Swing's `JTree.getPathForLocation` — and selects it like Swing `setSelectionPath`; the clicked node, not the previous selection, becomes `ProofTreeContext.invokedNode`; `key.fx.verify.prooftree` PASS "popup on clicked node, parkedSelection=true") | +| View-menu Pretty Print / Unicode inert placeholders | **RESOLVED** (WP-3: the items were already wired to the ViewSettings + NotationInfo statics + `refreshPrettyViews` since MP3a — the real gap found and fixed was the *initial* sequent printer, built from a bare `new NotationInfo()` that printed plain syntax regardless of the settings; the shared `createPrinter` now refreshes from the ViewSettings like Swing's mediator-owned NotationInfo; `key.fx.verify.menuparity` PrettyUnicode leg fires the real CheckMenuItems and asserts the settings mirroring, the Unicode disable binding and the visible effect — `PASS - pretty[true->true] unicodeEffect=true`; the demo sequent has no arithmetic, so its pretty/default notation is identical and the visible effect is asserted through the state-aware unicode toggle) | +| Recent-file clicks drop stored profile / single-java options | **RESOLVED** (P1: `openProofFile` registers the loading options with the entry like Swing `WindowUserInterfaceControl.loadProblem`; the recent-files menu restores profile (resolved via `DefaultProfileResolver`) / additional options / single-java like Swing `RecentFileAction`, `key.fx.verify.loadingexit` round trip PASS) | +| Shortcut-default mismatches (`KeyStrokeManagerF`: tree search, sequent search, macro defaults) | **RESOLVED** (P1: the defaults match the Swing table now — macros and PrettyPrint/Unicode/ProofManagement/tree-search on Ctrl+Shift, sequent search on Ctrl+F instead of the bare F that hijacked typing; stale persisted old defaults heal on load; `key.fx.verify.shortcuts` PASS) | +| Dead registered bindings (Ctrl+C term copy, F3/Shift+F3, Ctrl+K/Ctrl+J, Goal Back/Prune) | **RESOLVED** (P1: Ctrl+C copies the term under the mouse via the sequent view handler + the term-menu copy item carries the accelerator; term-menu global macro items carry their accelerators and the view-level macro keys run at the last clicked position (Swing `MacroKeyBinding`); F3/Shift+F3, Ctrl+K/Ctrl+J, Goal Back/Prune wired and covered by `key.fx.verify.shortcuts`) | +| Colors: 12 mapped CSS variables ineffective (47 property definitions missing) | **RESOLVED** (P1: `ColorPaletteF` defines all 51 Swing-parity properties — the true count incl. the two multi-line `define(` keys; the 9 previously-undeclared mapped CSS vars are declared in both themes and consumed by the re-wired `.sequent-hl-*`/`.source-*` rules; `key.fx.verify.colors` PASS) | +| UPSTREAM (Swing, not FX): `LoopApplyHeadCompletion` + `LoopContract*` dead code; seed-clobber `overwriteWith` | **Not our defect** — flags for upstream `key.ui`/`key.core` cleanup | + +## P1 sign-off + +| Audit item | Status | +|---|---| +| Loading options (profile / ignore other Java files) | **RESOLVED** — load-options dialog ported (`key.fx.verify.profileloading` + `profileloadingdialog` PASS) | +| Select Goal Above / Below + menu set (View 7) | **RESOLVED** (WP-10: Selection Back/Forward verified — `key.fx.verify.selectionhistory` PASS: the View menu's Back/Forward items carry the KeyStrokeManagerF accelerators (Ctrl+Alt+Left/Right), follow the history-driven enablement and firing them moves the mediator selection back/forward over the `SelectionHistoryF` — "PASS (navigation: moved 0->148)"; the View-menu surface itself was already `key.fx.verify.menuparity` View 7 PASS) | +| Automation submenu + macro invocation | **RESOLVED** (automation submenu MP2, macro menu in term menu); global toolbar dropdown KNOWN-DEFERRED (deliberate): with B14 the FX keeps ONE merged extension toolbar and the Swing `DropdownSelectionButton` macro-dropdown has no dedicated slot — macros run from the Automation submenu and the sequent/tree macro menus (B12); a toolbar dropdown control remains a possible small follow-up | +| Join / merge dialogs | **RESOLVED** for the merge/join flow (`key.fx.verify.joinmerge` PASS on gcd 32/0); `keyext.slicing.fx` SMT routing partial | +| Strategy preset combo / stash UI | **RESOLVED** (WP-3: the Swing `StrategySelectionView.createDefaultPanel` [⚙][combo][Apply] row ported — Defaults first, then the built-in presets, then the stored user presets with the "✕" delete affordance; save/stash/rename via the gear menu's parameterized core methods over `StrategyPresetsSettings` (Swing :663-750), Apply writes maxSteps + properties into the proof's live settings and gates on `predefChanged` like Swing `applySelectedPreset` :572-585; `key.fx.verify.goallist` asserts the entry list + stash/save/rename/delete round trip + write-through + Apply gating — "PASS - entries=3 stash/save/rename/delete=ok maxSteps=10000->10000") | +| SMT settings + run UI | **RESOLVED** (P1: settings providers ported in MP4; the run UI — `SolverListenerF` + `ProgressDialogF` progress table + `InformationWindowF` + result application via the SMT rule — ported, `key.fx.verify.smt` PASS: Z3 closes the Agatha goal; the Swing toolbar `DropdownSelectionButton` remains tracked under the toolbar item (KNOWN-DEFERRED, see the P1 automation row); WP-7: the per-solver command/parameters/timeout/support panels are ported as `SolverOptionsF` child providers of the SMT settings entry (Swing `SolverOptions` parity, KNOWN-DEFERRED — deliberate per-feature deferral of WP-7, sites `SolverOptionsF.java:35/:130`: `updateSMTSelectMenu` refresh + progress mode/global timeout/bounds/store path, the FX main window has no SMT select-menu counterpart yet) and the result application is the undoable `SMTProofApplyUserActionF` with the undoable-apply assert in `key.fx.verify.smt`) | +| Exit flow (close-request, `confirmExit`, layout save) | **RESOLVED** (P1: the window close button and the Exit menu item run the Swing `ExitMainAction` flow — `confirmExit` dialog, recent-files save, `System.exit(0)` which runs the docking/colors/keystrokes shutdown hooks; WP-1: the Swing mediator `fireShutDown` is now ported — `KeYMediatorF` GUI-listener registry + the exit flow fires the event, KNOWN-SIMPLIFIED row RESOLVED; `key.fx.verify.loadingexit` PASS: recent-files round trip + profile resolution, then the close-request path terminates with exit code 0 and the docking layout is saved) | +| Term labels; Pretty Print / Unicode wiring | **RESOLVED** for the wiring (WP-3: the View-menu toggles drive the ViewSettings + NotationInfo statics + the `refreshPrettyViews` re-render, and the initial printer honors the settings like Swing — see the P0 row; visible effect via `key.fx.verify.menuparity` PrettyUnicode PASS). Term labels stay covered mechanically by the `key.fx.verify.lemmaorigin` hook | +| User-selection highlight + Ctrl+C copy | **RESOLVED** (term-menu copy item in the skeleton); multi-selection highlight + reprint persistence **RESOLVED** (WP-3: sticky Ctrl+click / middle-click toggle in the `userSelectionOverlay` pane with the Swing `PERMANENT_HIGHLIGHT_COLOR` colors (light rgba(110,85,181,0.3), dark rgba(210,185,201,0.78), SequentViewInputListener.java:135-145); the highlight survives plain reprints and settings-change re-renders via `recalculateUserSelectionRange` over `table.pathForPosition`/`rangeForPath` (Swing SequentView.java:585-660, without the Swing +1 offset — the FX position table indexes match the printed text); cleared on node switch (documented deviation — Swing keeps the stored position across node switches but also loses it visually when the view instance swaps); `key.fx.verify.sequent` PASS — reprint=true settings=true toggle=true) | +| Symbex source line highlights + sequent-hover origin cross-highlight | KNOWN-DEFERRED (deliberate, per-feature deferral documented at the source sites: `SourceViewF.java:64-66` — "the tab-per-file UI … deliberately deferred", `:110` — "deferred: the Swing view updates the symbolic execution highlights here", `:237`; outside the WP-1…WP-10 scope) | +| KeyStroke default wiring next to the registry | **RESOLVED** (P1: `key.fx.verify.shortcuts` PASS — Swing-parity defaults, no binding collisions, an override round trip and the sequent-view Ctrl+F key path; the defaults table lives inside the FX registry `KeyStrokeManagerF` (`defineDefault`), so "wiring next to the registry" is exactly what the hook asserts) | + +## P2 sign-off + +Heatmap overlay (RESOLVED via WP-2 — the heat overlay is ported onto `SequentViewF` in the +Swing-faithful scope: the Swing original `SequentView.updateHeatMapHighlights` renders into the +sequent views only, never the proof tree), NodeInfoVisualizer + the proof-tree renderer surface +and branch-label F2 editing (RESOLVED via WP-2, see carried-forward item 2), +info-view node-change refresh, notification framework depth, docking title +actions/layout slots/maximize (partially done — `key.fx.verify.docking` PASS; title actions +exist as `DockTitleActionF`), join+mergerule dialogs (track MP9.x modules), lemmatagenerator +(`key.fx.verify.lemmaorigin` PASS for the generator path), soundiness (`key.fx.verify.soundiness` +PASS), originlabels (lemmaorigin), plugins, profileloading (RESOLVED), help windows +(`key.fx.verify.help` PASS), theme persistence (color definitions RESOLVED via P1 +`key.fx.verify.colors`; the persistence itself RESOLVED via WP-3, item 9 below), feature +flags + parallel prover (`ParallelProverStatusIndicatorF` RESOLVED via WP-3 — the SC/MT toggle +button with the worker-count context menu, `key.fx.verify.extensions` proverMode leg PASS; +KNOWN-SIMPLIFIED row RESOLVED), settings dump, modal +grey-out, proof-disposal clearing (auto saver handles the disposal part), tab icons/titles, +file-chooser bookmarks. Each is either documented in the KNOWN-SIMPLIFIED ledger or listed above +as open. + +## Still-open work list (carried forward) + +1. Input freeze during auto mode (blocking glass pane port) — RESOLVED via P1 + `key.fx.verify.inputfreeze`; glass-pane scope decided in WP-1: WONT-REPLICATE — the FX + overlay keeps covering only the views area (the menu/toolbar proof actions are disabled + during auto mode anyway, the automation macro items must stay clickable to stop a run, and + the status bar must stay live for the progress display) — KNOWN-SIMPLIFIED. +2. Proof-tree: Apply Strategy on clicked node, Prune-at-node in the popup (both RESOLVED via + WP-10 `key.fx.verify.prooftree`), renderer surface, NodeInfoVisualizer, branch-label F2 + editing — RESOLVED (WP-2): the renderer surface is ported (leaf goal icons — closed goal, + cached-closed, linked, interactive, open — as FontAwesome glyph stand-ins for the Swing + key-hole gifs, non-leaf marker icons in the Swing priority window/notes/useless/interactive/ + script, the branch linked-folder icon, tooltip notes + useless-analysis lines, and the + `NodeInfoVisualizerListenerF` attachment that re-renders on register/unregister like Swing's + `nodeInfoVisListener`); branch-label F2 editing is ported with the Swing + `DefaultTreeCellEditor.isCellEditable` gate (only branch entries whose node has a parent — + the root branch is denied) and the commit seam mirroring + `GUIProofTreeModel.valueForPathChanged → GUIBranchNode.setLabel → NodeInfo.setBranchLabel` + plus the full rebuild; the heatmap heat overlay renders into the sequent view (the Swing + original touches the sequent views only). Documented deviations: the Swing key-hole gif + images have no FontAwesome glyph equivalents (state colors stay on the text classes, icons + use the neutral `key-icon` fill), and `key.fx.verify.prooftree` asserts the surface — + `branchEdit rootEditable=false labelEdit=PASS leafIcons=3 nodeInfoVisualizer=PASS PASS` + (`/tmp/opencode/wp2/prooftree-agatha3.log`) and the heatmap leg + `sfAge=1 sfNewest=5 termsAge=6 termsNewest=3 off=0 PASS` (`/tmp/opencode/wp2/heatmap1.log`). +3. Sequent: multi-select highlight + reprint persistence (RESOLVED via WP-3 + `key.fx.verify.sequent`), drag & drop, inner-node highlights + + taclet info pane, source cross-highlight. +4. Source view: symbex line highlights, click-to-jump into the proof tree, hover + cursor/line highlight, multi-file tabs, branch status bar. +5. Menus/actions: Pretty Print / Unicode wiring (RESOLVED via WP-3 — see the P0 row; + `key.fx.verify.menuparity` PrettyUnicode PASS), term labels, tooltip toggles, selection + Back/Forward bindings (RESOLVED via WP-10 `key.fx.verify.selectionhistory`), Edit Last File, + Load User Taclets + Prove submenu, Run All Proofs + (dialogs exist for several), EnableWhenProofLoaded analogue, toolbars 9 remaining buttons. +6. Keyboard: shortcut-default regressions; dead bindings audit (RESOLVED via P1 + `key.fx.verify.shortcuts`; the Swing-persisted `keystrokes.json` stays the source of truth + for user overrides). +7. Options dialogs: strategy preset UI (RESOLVED via WP-3 — the strategy tab's [⚙][combo][Apply] + row + `key.fx.verify.goallist` PASS), HeatmapOptionsDialog (SMT run UI RESOLVED via P1 + `key.fx.verify.smt`). +8. Exit flow: close-request + confirmExit + layout persistence on close (RESOLVED via P1 + `key.fx.verify.loadingexit`; the Swing `fireShutDown` event now fires through the WP-1 + `GUIListenerF` registry seam — `MainWindowF.java:3721` RESOLVED). +9. Colors/theme: all 51 Swing-parity color property definitions RESOLVED (P1 `key.fx.verify.colors` PASS); theme persistence RESOLVED (WP-3: `ThemeManager` persists to the user preference node, `key.fx.verify.themepersist` save/restore round trip PASS — save `applied=DARK persisted=DARK`, restore `restored=DARK persisted=DARK reset=LIGHT`). +10. Notification framework depth: proof-closed/exception dialogs beyond toasts are in + (`IssueDialogF`); the `NotificationTask`/action framework remains partial. +11. Docking: remaining title actions, layout-slot keys F10–F12 (named slots exist). +12. Upstream (Swing) flags: `LoopApplyHeadCompletion`/`LoopContract*` dead code, seed-clobber. + +### Close-out status (WP-11, 2026-10-12) + +Of the carried-forward list above, items 1, 2, 6, 7, 8 and 9 are RESOLVED with the evidence +cited inline (P1…P4 batches and the WP-1…WP-10 merges; per-WP evidence logs under +`/tmp/opencode/wp*/`). Item 5 is resolved in its main parts: term labels (`key.fx.verify.lemmaorigin`), +the Load-User-Taclets dialog (P2b `LoadUserTacletsDialogF`), the Prove submenu +(`buildProveSubmenu`, `MainWindowF.java:482`) and Run All Proofs (`RunAllProofsF`, behind the +Swing-parity feature flag, `MainWindowF.java:241`) are ported; the remainder of item 5 and the +other per-feature tails are deliberate KNOWN-DEFERRED deferrals of the FX port, each documented +at its source site or in the tables above: the sequent drag & drop and inner-node +highlights/taclet info pane (item 3), the source-view family (item 4, +`SourceViewF.java:64-66/:110/:237`), Edit Last File, tooltip toggles, the +EnableWhenProofLoaded analogue and the toolbar buttons beyond the merged bar (item 5), the +global toolbar macro dropdown (P1 automation row), the info-view node-change statistics +refresh (`InfoViewF.java:94-99`), the notification `NotificationTask`/action-framework depth +(item 10) and the docking title-action/layout-slot remainder (item 11, named slots F10–F12 +exist). Item 12 flags upstream Swing defects ("Not our defect" — `key.ui`/`key.core` cleanup, +unchanged by this migration). + +**No row of this sign-off remains OPEN or unmarked.** Every entry ends RESOLVED, +WONT-REPLICATE (with its reason) or a clearly marked deliberate KNOWN-DEFERRED per-feature +deferral with its batch/WP reference and source site. The module-removal counterpart of this +close-out is `SWING-RETIREMENT.md`. + +The KNOWN-SIMPLIFIED ledger mirrors the module-level subset of this list with per-site +file:line markers and statuses (`OPEN` / `FIXED-UPSTREAM` / `WONT-REPLICATE`). This sign-off is +re-run after each milestone batch that closes any of the items above. + +# Difference audit — Swing↔JavaFX (2026-10-10) + +The 2026-10-08 sign-off covered the documented deviations (the 68 KNOWN-SIMPLIFIED markers plus +the still-open list above). This section records the **new, previously undocumented** +differences found by a second Swing↔JavaFX sweep, with stable IDs used by the P2/P3/P4 batches +(`weigl/ocfx-p2-*`, `weigl/ocfx-p3-*`, `weigl/ocfx-p4-*`). Statuses: OPEN / RESOLVED (batch) +/ WONT-REPLICATE. + +## A. Dialogs missing or reduced + +| ID | Finding (Swing reference) | Status | +|----|---------------------------|--------| +| A1 | Contract/invariant configurator dialogs: the Swing registration `WindowUserInterfaceControl.java:74-82` (FunctionalOperationContract/DependencyContract/LoopInvariantRule/BlockContractInternal/BlockContractExternal completions + `ContractConfigurator.java`) — the FX registry (`WindowUserInterfaceControlF.java:126-135`) holds only `MergeRuleCompletionF` | RESOLVED (P2b) | +| A2 | `LemmaSelectionDialog` (lemmatagenerator, 161 lines) not ported | RESOLVED (P2b) | +| A3 | `LoadUserTacletsDialog` reduced (Swing 499 lines) | RESOLVED (P2b) | +| A4 | Proof Statistics: no export (Swing exports HTML/text) | RESOLVED (P3c) | +| A5 | About/License reduced to toasts instead of dialogs | RESOLVED (P3c) | +| A6 | GitHub-issue prefill dropped (bug-reporting URL parameters) | RESOLVED (P3c) | +| A7 | Feedback: no zip archive of logs | RESOLVED (P3c) | +| A8 | ToolTip options: "Save as Default" behaviour | RESOLVED (P3c) | +| A9 | `EnsureSourceConsistency` info dialog | RESOLVED (P2b) | +| A10 | Dialog triage remainder of the sweep | RESOLVED (P4, triage) | + +## B. Menus / actions / toolbar + +| ID | Finding (Swing reference) | Status | +|----|---------------------------|--------| +| B11 | Dynamic "Goal Back" label (`GoalBackAction.java:113-125`) vs. static `MainWindowF.java:3325-3327` | RESOLVED (P3b) | +| B12 | Macro superset + category submenus + ProofScript actions vs. the 4-macro `AUTOMATION_MACROS` | RESOLVED (P3b) | +| B13 | Extension PATH nesting (extension menus cannot nest) | RESOLVED (P4) | +| B14 | Per-extension toolbars merged into one | RESOLVED (P4, decided) | +| B15 | Toolbar GoalBack/Prune have no enablement | RESOLVED (P3b) | +| B16 | Popup dialogs replaced by toasts (per site) | RESOLVED (P4, decided) | +| B17 | TermLabelMenu persistence/styling | RESOLVED (P3b) | +| B18 | Recent-Files empty menu not disabled + font-size item order | RESOLVED (P3b) | + +## C. Proof tree + +| ID | Finding (Swing reference) | Status | +|----|---------------------------|--------| +| C19 | Per-proof view state cache (expansion/selection per proof) | RESOLVED (P3a) | +| C20 | Linearized (flat) proof view mode | RESOLVED (P3a) | +| C21 | OSS child nodes in the tree | RESOLVED (P3a) | +| C22 | Whole-tree actions (expand all/collapse all/...) | RESOLVED (P3a) | +| C23 | Popup items incl. SubtreeStatistics | RESOLVED (P3a) | +| C24 | `PROOF_TREE` extension seam (tree popup contributions) | RESOLVED (P4) | +| C25 | Node-filter counting rule | RESOLVED (P3a) | +| C26 | Hidden-tab passivation (Swing docking detail) | WONT-REPLICATE (P4, decided) | +| C27 | Auto-mode partial subtree updates | RESOLVED (P3a) | + +## D. Sequent / strategy / goal list / status bar + +| ID | Finding (Swing reference) | Status | +|----|---------------------------|--------| +| D28 | Left-click taclet menu + `POPUP_DELAY` guard (`CurrentGoalViewListener.java:48-95`, `SequentViewListener.java:29`) | RESOLVED (P2a) | +| D29 | Shift+click focussed auto mode (`CurrentGoalViewListener.java:56-58`) | RESOLVED (P2a) | +| D30 | Extension tooltip strings unwired | RESOLVED (P4) | +| D31 | Sequent line width computed from the viewport | RESOLVED (P3c) | +| D32 | Sequent search prefill from the hovered term (`SearchInSequentAction.java:32-37`) | RESOLVED (P2a) | +| D33 | Fonts vs. `KEY_FONT_*` settings | RESOLVED (P3c) | +| D34 | `SequentViewDock` missing | RESOLVED (P3c) | +| D35 | Strategy tab Go button + parallel-prover merge-point lock (`StrategySelectionView.java:157-208/869-895`) | RESOLVED (P2a) | +| D36 | `KeyboardShortcuts` extension seams absent | RESOLVED (P4) | +| D37 | Status-line task progress bar (log-only stubs, `WindowUserInterfaceControlF.java:317-327`) | RESOLVED (P3c) | + +P2a (`weigl/ocfx-p2-sequent`, merged 2026-10-10) resolved D28/D29/D32/D35 — +`key.fx.verify.sequentmenu` PASS (term menu 31 entries, POPUP_DELAY guard, search prefill, +focussed auto mode) on Xvnc :99. + +P2b (`weigl/ocfx-p2-dialogs`, merged 2026-10-10) resolved A1/A2/A3/A9 — the five contract +completions (`FunctionalOperationContractCompletionF`, `DependencyContractCompletionF`, +`LoopInvariantRuleCompletionF`, `BlockContractInternalCompletionF`, +`BlockContractExternalCompletionF`) are registered in the FX control next to +`MergeRuleCompletionF` (Swing parity WindowUserInterfaceControl.java:74-82); the dialogs +(`ContractConfiguratorF`, `AuxiliaryContractConfiguratorF`, `BlockContractSelectionPanelF`, +`ContractSelectionPanelF`, `InvariantConfiguratorF`, `LemmaSelectionDialogF` + `ItemChooserF`, +`LoadUserTacletsDialogF` axiom panel/warning/help, `EnsureSourceConsistency` info dialog) are +ported; `key.fx.verify.dialogs` PASS (registry + dialog skeletons) on Xvnc :99. + +Interactive end-to-end contract application is RESOLVED (WP-9, `weigl/ocfx-wp9-integration`): +the sixth leg of `key.fx.verify.dialogs` loads a real spec-bearing example off the main window +(`heap/model_methods/CellTest_callSet.key`, override `key.fx.verify.dialogs.contract`), builds a +`UseOperationContractRule` app on a succedent top-level goal position, completes it through the +REAL `WindowUserInterfaceControlF.completeBuiltInRuleApp` dispatch (the modal +`ContractConfiguratorF` is driven by a background watcher via the new `lastInstance` seam: +select contract + OK) and applies the completed app via `ProofControl.applyInteractive`, +growing the proof by exactly one node. HTML-styled contract cells of the Swing configurator +remain plain text in the FX port (KNOWN-SIMPLIFIED, see the class javadocs). + +P3a (`weigl/ocfx-p3a-prooftree`, merged 2026-10-10) resolved C19/C20/C21/C22/C23/C25/C27 — +`ProofTreeViewF`: the per-proof view-state cache (WeakHashMap, saved and +restored in the proof switch, C19); the linearized mode with the "main"-tagged taclet splice +(C20); the OneStepSimplifier protocol child rows with an "expand OSS nodes" toggle that gates +the whole-tree expand (C21); the whole-tree expand-all/collapse-all actions (C22); the popup +additions Apply Strategy / Prune Proof / Edit Notes / Show Subtree Statistics (C23, Swing +`ProofTreePopupFactory`); the node-filter counting rule incl. the "inlined due to hidden +subtree" case (C25); and the auto-mode partial subtree updates (C27, `modifiedSubtrees`, +`MAX_PARTIAL_TREE_UPDATES=16`). `key.fx.verify.prooftree` PASS (semantics self test + notes +dialog + subtree statistics dialog) on Xvnc :99, plus a live-autoprove run +(`key.fx.verify.prooftree` + `key.fx.demo.autoprove.live`) that exercised the partial subtree +updates (`autoModePartialUpdates=1`) and a post-autoprove run (`+ key.fx.demo.autoprove`) +covering the OSS rows on a strategy-proved proof. The view filters and the tree controls live +in the tree context menu because the FX docking framework has no tab-title gear menu (documented +in `ProofTreeViewF`); the subtree statistics report is a plain-text window rather than the Swing +HTML one (export is A4/P3c). C24 (the `PROOF_TREE` extension seam) stays open for P4. + +P3b (`weigl/ocfx-p3b-menus`, see the branch report) resolved B11/B12/B15/B17/B18 — menu/toolbar +parity items: + +- B11/B15 — the Proof-menu item and toolbar buttons now follow Swing enablement and labels: + "Undo Last Rule Application" shows the applied rule name dynamically (`KeYMediatorF + .`goalBackRuleName`), and Goal Back / Prune are enabled per the selected node and auto mode + (`key.fx.verify.menuparity` legs). +- B12 — the macro surfaces (sequent right-click popup, term-menu "Strategy Macros", proof-tree + context-menu "Strategy Macros") now show the registered-`ProofMacro` superset + (`ProofMacroMenuF`), category-grouped like Swing, plus the PROOF_SCRIPTS menu (file chooser / + input dialog) executed by a new `ProofScriptWorkerF`; the proof-tree macro submenu is + persistent with a live PROOF_SCRIPTS feature listener. +- B17 — `TermLabelMenuF` items are `CustomMenuItem(HBox(CheckBox+Label))` rows that persist + their state to `Preferences.userNodeForPackage(MainWindowF.class)` under the exact Swing + `AbstractButtonSaver` keys (`DisplayLabelsCheckBox.DisplayLabelsCheckBox.selected` / + `TermLabelCheckBox.