From ef77b66780b5b2646f1b099de10d678b74f9b4e1 Mon Sep 17 00:00:00 2001 From: PiisRational Date: Sun, 8 Jun 2025 11:52:42 +0200 Subject: [PATCH 1/7] extend the javac extension --- key.ui/build.gradle | 22 ++++- .../javac/JavaCompilerCheckFacade.java | 11 ++- .../key/gui/plugins/javac/JavacExtension.java | 24 ++++- .../key/gui/plugins/javac/JavacSettings.java | 96 +++++++++++++++++++ .../plugins/javac/JavacSettingsProvider.java | 80 ++++++++++++++++ 5 files changed, 229 insertions(+), 4 deletions(-) create mode 100644 key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/javac/JavacSettings.java create mode 100644 key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/javac/JavacSettingsProvider.java diff --git a/key.ui/build.gradle b/key.ui/build.gradle index 5ec55a4a26b..f5db1e9eb11 100644 --- a/key.ui/build.gradle +++ b/key.ui/build.gradle @@ -69,7 +69,27 @@ run { // this can be used to solve a problem where the OS hangs during debugging of popup menus // (see https://docs.oracle.com/javase/10/troubleshoot/awt.htm#JSTGD425) - jvmArgs += "-Dsun.awt.disablegrab=true" + jvmArgs += [ + "-Dsun.awt.disablegrab=true ", + "--add-exports", + "jdk.compiler/com.sun.tools.javac.api=ALL-UNNAMED", + "--add-exports", + "jdk.compiler/com.sun.tools.javac.code=ALL-UNNAMED", + "--add-exports", + "jdk.compiler/com.sun.tools.javac.file=ALL-UNNAMED", + "--add-exports", + "jdk.compiler/com.sun.tools.javac.main=ALL-UNNAMED", + "--add-exports", + "jdk.compiler/com.sun.tools.javac.model=ALL-UNNAMED", + "--add-exports", + "jdk.compiler/com.sun.tools.javac.processing=ALL-UNNAMED", + "--add-exports", + "jdk.compiler/com.sun.tools.javac.tree=ALL-UNNAMED", + "--add-exports", + "jdk.compiler/com.sun.tools.javac.util=ALL-UNNAMED", + "--add-opens", + "jdk.compiler/com.sun.tools.javac.comp=ALL-UNNAMED" + ] } task runWithProfiler(type: JavaExec) { diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/javac/JavaCompilerCheckFacade.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/javac/JavaCompilerCheckFacade.java index 01759d83660..d93f294efd8 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/javac/JavaCompilerCheckFacade.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/javac/JavaCompilerCheckFacade.java @@ -56,11 +56,13 @@ public class JavaCompilerCheckFacade { * @param classPath the {@link List} of {@link File}s referring to the directory that make up * the target Java programs classpath * @param javaPath the {@link String} with the path to the source of the target Java program + * @param processors the {@link List} of {@link String}s referring to the annotation processors to be run * @return future providing the list of diagnostics */ public static @NonNull CompletableFuture> check( ProblemInitializer.ProblemInitializerListener listener, - File bootClassPath, List classPath, File javaPath) { + File bootClassPath, List classPath, File javaPath, + List processors) { if (Boolean.getBoolean("KEY_JAVAC_DISABLE")) { LOGGER.info("Javac check is disabled by system property -PKEY_JAVAC_DISABLE"); return CompletableFuture.completedFuture(Collections.emptyList()); @@ -86,6 +88,7 @@ public class JavaCompilerCheckFacade { // gather configured bootstrap classpath and regular classpath List options = new ArrayList<>(); + if (bootClassPath != null) { options.add("-Xbootclasspath"); options.add(bootClassPath.getAbsolutePath()); @@ -95,6 +98,12 @@ public class JavaCompilerCheckFacade { options.add( classPath.stream().map(File::getAbsolutePath).collect(Collectors.joining(":"))); } + + if (processors != null && !processors.isEmpty()) { + options.add("-processor"); + options.add(processors.stream().collect(Collectors.joining(","))); + } + ArrayList files = new ArrayList<>(); if (javaPath.isDirectory()) { try (var s = Files.walk(javaPath.toPath())) { diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/javac/JavacExtension.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/javac/JavacExtension.java index c8d62a2e080..38a4937fbd5 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/javac/JavacExtension.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/javac/JavacExtension.java @@ -5,6 +5,9 @@ import java.awt.*; import java.io.File; +import java.util.ArrayList; +import java.util.Arrays; +import java.util.Arrays; import java.util.Collections; import java.util.List; import java.util.TreeSet; @@ -24,6 +27,7 @@ import de.uka.ilkd.key.gui.fonticons.MaterialDesignRegular; import de.uka.ilkd.key.proof.JavaModel; import de.uka.ilkd.key.proof.Proof; +import de.uka.ilkd.key.gui.settings.SettingsProvider; import org.slf4j.Logger; import org.slf4j.LoggerFactory; @@ -42,7 +46,7 @@ experimental = false) public class JavacExtension implements KeYGuiExtension, KeYGuiExtension.StatusLine, KeYGuiExtension.Startup, - KeYSelectionListener { + KeYSelectionListener, KeYGuiExtension.Settings { /** * Color used for the label if javac didn't produce any diagnostics. */ @@ -147,6 +151,18 @@ private void loadProof(Proof selectedProof) throws RuntimeException { File bootClassPath = jm.getBootClassPath() != null ? new File(jm.getBootClassPath()) : null; List classpath = jm.getClassPathEntries(); + JavacSettings settings = JavacSettingsProvider.getJavacSettings(); + + List checkers = null; + if (settings.getUseCheckers()) { + if (classpath == null) classpath = new ArrayList<>(); + + classpath.addAll(Arrays.asList(settings.getCheckerPaths().split(System.lineSeparator())) + .stream().map(p -> new File(p)).toList()); + + checkers = Arrays.asList(settings.getCheckers().split(System.lineSeparator())); + } + File javaPath = new File(jm.getModelDir()); lblStatus.setForeground(Color.black); @@ -154,7 +170,7 @@ private void loadProof(Proof selectedProof) throws RuntimeException { lblStatus.setIcon(ICON_WAIT.get(16)); CompletableFuture> task = - JavaCompilerCheckFacade.check(mediator.getUI(), bootClassPath, classpath, javaPath); + JavaCompilerCheckFacade.check(mediator.getUI(), bootClassPath, classpath, javaPath, checkers); try { task.thenAccept(it -> SwingUtilities.invokeLater(() -> { lblStatus.setText("Javac finished"); @@ -227,6 +243,10 @@ public void selectedNodeChanged(KeYSelectionEvent e) { public void selectedProofChanged(KeYSelectionEvent e) { loadProof(e.getSource().getSelectedProof()); } + + public SettingsProvider getSettings() { + return new JavacSettingsProvider(); + } } diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/javac/JavacSettings.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/javac/JavacSettings.java new file mode 100644 index 00000000000..a68e6070f4d --- /dev/null +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/javac/JavacSettings.java @@ -0,0 +1,96 @@ +/* This file is part of KeY - https://key-project.org + * KeY is licensed under the GNU General Public License Version 2 + * SPDX-License-Identifier: GPL-2.0-only */ +package de.uka.ilkd.key.gui.plugins.javac; +import java.lang.Boolean; + +import de.uka.ilkd.key.settings.AbstractPropertiesSettings; + +/** + * Settings for the javac extention. + * + * @author Daniel Grévent + */ +public class JavacSettings extends AbstractPropertiesSettings { + + public static final String CATEGORY = "Type Checking"; + + /** + * Config key for {@link #checkers}. + */ + private static final String KEY_USE_CHECKERS = "useCheckers"; + + /** + * Config key for {@link #checkers}. + */ + private static final String KEY_CHECKERS = "checkers"; + + /** + * Config key for {@link #checkerPaths}. + */ + private static final String KEY_CHECKER_PATHS = "checkerPaths"; + + /** + * The type checkers (processors) to be run. + */ + private final PropertyEntry useCheckers = + createBooleanProperty(KEY_USE_CHECKERS, false); + + /** + * The type checkers (processors) to be run. + */ + private final PropertyEntry checkers = + createStringProperty(KEY_CHECKERS, ""); + + /** + * The paths needed for the checkers (processors). + */ + private final PropertyEntry checkerPaths = + createStringProperty(KEY_CHECKER_PATHS, ""); + + public JavacSettings() { + super(CATEGORY); + } + + /** + * @param useCheckers if the type checkers should be used + */ + public void setUseCheckers(boolean useCheckers) { + this.useCheckers.set(useCheckers); + } + + /** + * @param checkers the type checkers to use + */ + public void setCheckers(String checkers) { + this.checkers.set(checkers); + } + + /** + * @param paths the paths on which the type checkers are + */ + public void setCheckerPaths(String paths) { + this.checkerPaths.set(paths); + } + + /** + * @return true iff the checkers should be used + */ + public boolean getUseCheckers() { + return useCheckers.get(); + } + + /** + * @return all the checkers in a comma separated string + */ + public String getCheckers() { + return checkers.get(); + } + + /** + * @return all checker paths spearated by a colon + */ + public String getCheckerPaths() { + return checkerPaths.get(); + } +} diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/javac/JavacSettingsProvider.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/javac/JavacSettingsProvider.java new file mode 100644 index 00000000000..dffebd2b728 --- /dev/null +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/javac/JavacSettingsProvider.java @@ -0,0 +1,80 @@ +/* This file is part of KeY - https://key-project.org + * KeY is licensed under the GNU General Public License Version 2 + * SPDX-License-Identifier: GPL-2.0-only */ +package de.uka.ilkd.key.gui.plugins.javac; + +import javax.swing.*; + +import de.uka.ilkd.key.gui.MainWindow; +import de.uka.ilkd.key.gui.settings.SettingsPanel; +import de.uka.ilkd.key.gui.settings.SettingsProvider; +import de.uka.ilkd.key.settings.ProofIndependentSettings; + +/** + * Settings for the javac extension. + * + * @author Daniel Grévent + */ +public class JavacSettingsProvider extends SettingsPanel implements SettingsProvider { + /** + * Singleton instance of the slicing settings. + */ + private static final JavacSettings JAVAC_SETTINGS = new JavacSettings(); + + private static final String USE_CHECKERS_INFO = "If enabled the type checkers will be run in addition to the default java type checker."; + private static final String CHECKERS_INFO = "The list of type checkers to run in addition to the default Java type checker. Each checkers should be written on a new line."; + private static final String CHECKER_PATHS_INFO = "The list of paths to the type checkers and their dependencies. Each path should be absolute and be written on a new line."; + + private final JCheckBox useCheckers; + private final JTextArea checkers; + private final JTextArea paths; + + /** + * Construct a new settings provider. + */ + public JavacSettingsProvider() { + useCheckers = addCheckBox( + "use checkers", USE_CHECKERS_INFO, false, e -> {}); + checkers = addTextArea("checkers", "", CHECKERS_INFO, e -> {}); + paths = addTextArea("checker paths", "", CHECKER_PATHS_INFO, e -> {}); + + setHeaderText("Javac Options"); + } + + @Override + public String getDescription() { + return "Java Type Checking"; + } + + public static JavacSettings getJavacSettings() { + ProofIndependentSettings.DEFAULT_INSTANCE.addSettings(JAVAC_SETTINGS); + return JAVAC_SETTINGS; + } + + + @Override + public JPanel getPanel(MainWindow window) { + JavacSettings settings = getJavacSettings(); + + useCheckers.setSelected(settings.getUseCheckers()); + checkers.setText(settings.getCheckers()); + paths.setText(settings.getCheckerPaths()); + + return this; + } + + @Override + public void applySettings(MainWindow window) { + JavacSettings settings = getJavacSettings(); + + settings.setUseCheckers(useCheckers.isSelected()); + settings.setCheckers(checkers.getText()); + settings.setCheckerPaths(paths.getText()); + } + + + @Override + public int getPriorityOfSettings() { + return 10000; + } +} From 2a5ca567df5feed6878be6204cbf29f77962461c Mon Sep 17 00:00:00 2001 From: PiisRational Date: Mon, 17 Nov 2025 19:20:42 +0100 Subject: [PATCH 2/7] updated the code and text to be clearer --- .../key/gui/plugins/javac/JavacExtension.java | 10 +-- .../key/gui/plugins/javac/JavacSettings.java | 66 +++++++++---------- .../plugins/javac/JavacSettingsProvider.java | 59 ++++++++++++----- 3 files changed, 80 insertions(+), 55 deletions(-) diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/javac/JavacExtension.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/javac/JavacExtension.java index 38a4937fbd5..a98db9c985e 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/javac/JavacExtension.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/javac/JavacExtension.java @@ -153,14 +153,14 @@ private void loadProof(Proof selectedProof) throws RuntimeException { List classpath = jm.getClassPathEntries(); JavacSettings settings = JavacSettingsProvider.getJavacSettings(); - List checkers = null; - if (settings.getUseCheckers()) { + List processors = null; + if (settings.getUseProcessors()) { if (classpath == null) classpath = new ArrayList<>(); - classpath.addAll(Arrays.asList(settings.getCheckerPaths().split(System.lineSeparator())) + classpath.addAll(Arrays.asList(settings.getClassPaths().split(System.lineSeparator())) .stream().map(p -> new File(p)).toList()); - checkers = Arrays.asList(settings.getCheckers().split(System.lineSeparator())); + processors = Arrays.asList(settings.getProcessors().split(System.lineSeparator())); } File javaPath = new File(jm.getModelDir()); @@ -170,7 +170,7 @@ private void loadProof(Proof selectedProof) throws RuntimeException { lblStatus.setIcon(ICON_WAIT.get(16)); CompletableFuture> task = - JavaCompilerCheckFacade.check(mediator.getUI(), bootClassPath, classpath, javaPath, checkers); + JavaCompilerCheckFacade.check(mediator.getUI(), bootClassPath, classpath, javaPath, processors); try { task.thenAccept(it -> SwingUtilities.invokeLater(() -> { lblStatus.setText("Javac finished"); diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/javac/JavacSettings.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/javac/JavacSettings.java index a68e6070f4d..96488e6fa38 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/javac/JavacSettings.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/javac/JavacSettings.java @@ -16,81 +16,81 @@ public class JavacSettings extends AbstractPropertiesSettings { public static final String CATEGORY = "Type Checking"; /** - * Config key for {@link #checkers}. + * Config key for {@link #useProcessors}. */ - private static final String KEY_USE_CHECKERS = "useCheckers"; + private static final String KEY_USE_PROCESSORS = "useProcessors"; /** - * Config key for {@link #checkers}. + * Config key for {@link #processors}. */ - private static final String KEY_CHECKERS = "checkers"; + private static final String KEY_PROCESSORS = "processors"; /** - * Config key for {@link #checkerPaths}. + * Config key for {@link #classPaths}. */ - private static final String KEY_CHECKER_PATHS = "checkerPaths"; + private static final String KEY_CLASS_PATHS = "classPaths"; /** - * The type checkers (processors) to be run. + * The type annotation processors to be run. */ - private final PropertyEntry useCheckers = - createBooleanProperty(KEY_USE_CHECKERS, false); + private final PropertyEntry useProcessors = + createBooleanProperty(KEY_USE_PROCESSORS, false); /** - * The type checkers (processors) to be run. + * The type annotation processors to be run. */ - private final PropertyEntry checkers = - createStringProperty(KEY_CHECKERS, ""); + private final PropertyEntry processors = + createStringProperty(KEY_PROCESSORS, ""); /** - * The paths needed for the checkers (processors). + * Additional class paths, needed for example by annotation processors */ - private final PropertyEntry checkerPaths = - createStringProperty(KEY_CHECKER_PATHS, ""); + private final PropertyEntry classPaths = + createStringProperty(KEY_CLASS_PATHS, ""); public JavacSettings() { super(CATEGORY); } /** - * @param useCheckers if the type checkers should be used + * @param useProcessors if the annotation processors should be run */ - public void setUseCheckers(boolean useCheckers) { - this.useCheckers.set(useCheckers); + public void setUseProcessors(boolean useProcessors) { + this.useProcessors.set(useProcessors); } /** - * @param checkers the type checkers to use + * @param processor the annotation processors to run */ - public void setCheckers(String checkers) { - this.checkers.set(checkers); + public void setProcessors(String processor) { + this.processors.set(processor); } /** - * @param paths the paths on which the type checkers are + * @param paths the additional class paths */ - public void setCheckerPaths(String paths) { - this.checkerPaths.set(paths); + public void setClassPaths(String paths) { + this.classPaths.set(paths); } /** - * @return true iff the checkers should be used + * @return true iff the annotation processors should be used */ - public boolean getUseCheckers() { - return useCheckers.get(); + public boolean getUseProcessors() { + return useProcessors.get(); } /** - * @return all the checkers in a comma separated string + * @return the annotation processors separated by newlines */ - public String getCheckers() { - return checkers.get(); + public String getProcessors() { + return processors.get(); } /** - * @return all checker paths spearated by a colon + * @return the additional class paths separated by newlines */ - public String getCheckerPaths() { - return checkerPaths.get(); + public String getClassPaths() { + return classPaths.get(); } } diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/javac/JavacSettingsProvider.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/javac/JavacSettingsProvider.java index dffebd2b728..6ad05aba32e 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/javac/JavacSettingsProvider.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/javac/JavacSettingsProvider.java @@ -10,6 +10,8 @@ import de.uka.ilkd.key.gui.settings.SettingsProvider; import de.uka.ilkd.key.settings.ProofIndependentSettings; +import net.miginfocom.layout.CC; + /** * Settings for the javac extension. * @@ -17,33 +19,56 @@ */ public class JavacSettingsProvider extends SettingsPanel implements SettingsProvider { /** - * Singleton instance of the slicing settings. + * Singleton instance of the javac settings. */ private static final JavacSettings JAVAC_SETTINGS = new JavacSettings(); - private static final String USE_CHECKERS_INFO = "If enabled the type checkers will be run in addition to the default java type checker."; - private static final String CHECKERS_INFO = "The list of type checkers to run in addition to the default Java type checker. Each checkers should be written on a new line."; - private static final String CHECKER_PATHS_INFO = "The list of paths to the type checkers and their dependencies. Each path should be absolute and be written on a new line."; + /** + * Text for the explanaition. + */ + private static final String INTRO_LABEL = "This allows to run the Java compiler when loading java files with additional processes such as Nulness or Ownership checkers."; + + /** + * Information message for the {@link #useProcessors} checkbox. + */ + private static final String USE_PROCESSORS_INFO = + "If enabled the annotation processors will be run with the java compiler while performing type checking of newly loaded sources."; + + /** + * Information message for the {@link #processors} text area. + */ + private static final String PROCESSORS_INFO = """ + A list of annotation processors to run while type checking with the java compiler. + Each checkers should be written on a new line."""; + + /** + * Information message for the {@link #paths} text area. + */ + private static final String CLASS_PATHS_INFO = """ + A list of additional class paths to be used by the java compiler while type checking. + These could for example be needed for certain annotation processors. + Each path should be absolute and be written on a new line."""; - private final JCheckBox useCheckers; - private final JTextArea checkers; + private final JCheckBox useProcessors; + private final JTextArea processors; private final JTextArea paths; /** * Construct a new settings provider. */ public JavacSettingsProvider() { - useCheckers = addCheckBox( - "use checkers", USE_CHECKERS_INFO, false, e -> {}); - checkers = addTextArea("checkers", "", CHECKERS_INFO, e -> {}); - paths = addTextArea("checker paths", "", CHECKER_PATHS_INFO, e -> {}); + pCenter.add(new JLabel(INTRO_LABEL), new CC().span().alignX("left")); + useProcessors = addCheckBox( + "Enable Annotation Processing", USE_PROCESSORS_INFO, false, e -> {}); + processors = addTextArea("Annotation Processors", "", PROCESSORS_INFO, e -> {}); + paths = addTextArea("Class Paths", "", CLASS_PATHS_INFO, e -> {}); setHeaderText("Javac Options"); } @Override public String getDescription() { - return "Java Type Checking"; + return "Javac Options"; } public static JavacSettings getJavacSettings() { @@ -56,9 +81,9 @@ public static JavacSettings getJavacSettings() { public JPanel getPanel(MainWindow window) { JavacSettings settings = getJavacSettings(); - useCheckers.setSelected(settings.getUseCheckers()); - checkers.setText(settings.getCheckers()); - paths.setText(settings.getCheckerPaths()); + useProcessors.setSelected(settings.getUseProcessors()); + processors.setText(settings.getProcessors()); + paths.setText(settings.getClassPaths()); return this; } @@ -67,9 +92,9 @@ public JPanel getPanel(MainWindow window) { public void applySettings(MainWindow window) { JavacSettings settings = getJavacSettings(); - settings.setUseCheckers(useCheckers.isSelected()); - settings.setCheckers(checkers.getText()); - settings.setCheckerPaths(paths.getText()); + settings.setUseProcessors(useProcessors.isSelected()); + settings.setProcessors(processors.getText()); + settings.setClassPaths(paths.getText()); } From 74af1d7a68d15eb278cad28dc7cb1d2c51225750 Mon Sep 17 00:00:00 2001 From: PiisRational Date: Tue, 18 Nov 2025 20:59:07 +0100 Subject: [PATCH 3/7] save proof independent settings, that are not used by the configuration --- .../uka/ilkd/key/settings/Configuration.java | 4 +-- .../settings/ProofIndependentSettings.java | 27 ++++++++++++------- .../key/gui/plugins/javac/JavacExtension.java | 3 +++ .../key/gui/plugins/javac/JavacSettings.java | 5 +++- 4 files changed, 26 insertions(+), 13 deletions(-) diff --git a/key.core/src/main/java/de/uka/ilkd/key/settings/Configuration.java b/key.core/src/main/java/de/uka/ilkd/key/settings/Configuration.java index 8efef1a3e1b..b6dbb981ecd 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/settings/Configuration.java +++ b/key.core/src/main/java/de/uka/ilkd/key/settings/Configuration.java @@ -525,7 +525,7 @@ private ConfigurationWriter printMap(Map value) { } indent -= 4; newline().printIndent(); - out.format(" }"); + out.format("}"); return this; } @@ -555,7 +555,7 @@ private ConfigurationWriter printSeq(Collection value) { } indent -= 4; newline().printIndent(); - out.format(" ]"); + out.format("]"); return this; } diff --git a/key.core/src/main/java/de/uka/ilkd/key/settings/ProofIndependentSettings.java b/key.core/src/main/java/de/uka/ilkd/key/settings/ProofIndependentSettings.java index 0646074f4af..12b64dadf06 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/settings/ProofIndependentSettings.java +++ b/key.core/src/main/java/de/uka/ilkd/key/settings/ProofIndependentSettings.java @@ -53,8 +53,8 @@ public class ProofIndependentSettings { private final List settings = new LinkedList<>(); private final PropertyChangeListener settingsListener = e -> saveSettings(); - private Properties lastReadedProperties; - private Configuration lastReadedConfiguration; + private Properties lastReadProperties; + private Configuration lastReadConfiguration; private ProofIndependentSettings() { addSettings(smtSettings); @@ -74,11 +74,11 @@ public void addSettings(Settings settings) { if (!this.settings.contains(settings)) { this.settings.add(settings); settings.addPropertyChangeListener(settingsListener); - if (lastReadedProperties != null) { - settings.readSettings(lastReadedProperties); + if (lastReadProperties != null) { + settings.readSettings(lastReadProperties); } - if (lastReadedConfiguration != null) { - settings.readSettings(lastReadedConfiguration); + if (lastReadConfiguration != null) { + settings.readSettings(lastReadConfiguration); } } } @@ -106,19 +106,22 @@ private void load(File file) throws IOException { for (Settings settings : settings) { settings.readSettings(properties); } - lastReadedProperties = properties; + lastReadProperties = properties; } } else { - this.lastReadedConfiguration = Configuration.load(file); + this.lastReadConfiguration = Configuration.load(file); for (Settings settings : settings) { - settings.readSettings(lastReadedConfiguration); + settings.readSettings(lastReadConfiguration); } } } public void saveSettings() { if (!filename.getName().endsWith(".json")) { - Properties result = new Properties(); + Properties result = lastReadProperties == null + ? new Properties() + : new Properties(lastReadProperties); + for (Settings settings : settings) { settings.writeSettings(result); } @@ -135,6 +138,10 @@ public void saveSettings() { } Configuration config = new Configuration(); + if (lastReadConfiguration != null) { + config.overwriteWith(lastReadConfiguration); + } + for (var settings : settings) settings.writeSettings(config); if (!filename.exists()) { diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/javac/JavacExtension.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/javac/JavacExtension.java index a98db9c985e..480eb2e2c8f 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/javac/JavacExtension.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/javac/JavacExtension.java @@ -178,6 +178,9 @@ private void loadProof(Proof selectedProof) throws RuntimeException { updateLabel(data); })).get(); } catch (InterruptedException | ExecutionException ex) { + lblStatus.setForeground(COLOR_ERROR.get()); + lblStatus.setIcon(ICON_ERROR.get(16)); + lblStatus.setText("Javac error"); throw new RuntimeException(ex); } } diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/javac/JavacSettings.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/javac/JavacSettings.java index 96488e6fa38..95827169cba 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/javac/JavacSettings.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/javac/JavacSettings.java @@ -13,7 +13,10 @@ */ public class JavacSettings extends AbstractPropertiesSettings { - public static final String CATEGORY = "Type Checking"; + /** + * The name of the category in the settings. + */ + public static final String CATEGORY = "Javac Extension"; /** * Config key for {@link #useProcessors}. From 0ae4244a00008863c8b28639b1b464b4c1151450 Mon Sep 17 00:00:00 2001 From: PiisRational Date: Mon, 24 Nov 2025 16:37:42 +0100 Subject: [PATCH 4/7] few changes --- key.ui/build.gradle | 5 ++++- .../de/uka/ilkd/key/gui/plugins/javac/JavacExtension.java | 2 +- 2 files changed, 5 insertions(+), 2 deletions(-) diff --git a/key.ui/build.gradle b/key.ui/build.gradle index f5db1e9eb11..6c0f5f87cac 100644 --- a/key.ui/build.gradle +++ b/key.ui/build.gradle @@ -69,8 +69,11 @@ run { // this can be used to solve a problem where the OS hangs during debugging of popup menus // (see https://docs.oracle.com/javase/10/troubleshoot/awt.htm#JSTGD425) + jvmArgs += "-Dsun.awt.disablegrab=true " + + // this is needed to be able to load checker framework checkers in the javac + // extension jvmArgs += [ - "-Dsun.awt.disablegrab=true ", "--add-exports", "jdk.compiler/com.sun.tools.javac.api=ALL-UNNAMED", "--add-exports", diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/javac/JavacExtension.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/javac/JavacExtension.java index 480eb2e2c8f..c66567ec51d 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/javac/JavacExtension.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/javac/JavacExtension.java @@ -33,7 +33,7 @@ import org.slf4j.LoggerFactory; /** - * Extensions provides Javac checks for recent-loaded Java files. + * Extension provides Javac checks for recent-loaded Java files. *

* Provides an entry in the status line for access. * From 0f710eb359420d65fe7307b45f8b59893e8a870c Mon Sep 17 00:00:00 2001 From: PiisRational Date: Mon, 24 Nov 2025 17:08:46 +0100 Subject: [PATCH 5/7] fix mistakes introduced by the merge --- .../uka/ilkd/key/gui/plugins/javac/JavaCompilerCheckFacade.java | 2 +- .../java/de/uka/ilkd/key/gui/plugins/javac/JavacExtension.java | 1 + 2 files changed, 2 insertions(+), 1 deletion(-) diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/javac/JavaCompilerCheckFacade.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/javac/JavaCompilerCheckFacade.java index cccfd859de0..15a19f60fc9 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/javac/JavaCompilerCheckFacade.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/javac/JavaCompilerCheckFacade.java @@ -61,7 +61,7 @@ public class JavaCompilerCheckFacade { */ public static @NonNull CompletableFuture> check( ProblemInitializer.ProblemInitializerListener listener, - Path bootClassPath, List classPath, Path javaPath + Path bootClassPath, List classPath, Path javaPath, List processors) { if (Boolean.getBoolean("KEY_JAVAC_DISABLE")) { LOGGER.info("Javac check is disabled by system property -PKEY_JAVAC_DISABLE"); diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/javac/JavacExtension.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/javac/JavacExtension.java index ede47a3bce8..a36732b5390 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/javac/JavacExtension.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/javac/JavacExtension.java @@ -6,6 +6,7 @@ import java.awt.*; import java.nio.file.Path; +import java.nio.file.Paths; import java.util.ArrayList; import java.util.Arrays; import java.util.Collections; From d84fb9f3c76f404863fdc61e800747dc62915013 Mon Sep 17 00:00:00 2001 From: PiisRational Date: Sat, 6 Dec 2025 18:31:19 +0100 Subject: [PATCH 6/7] Revert "save proof independent settings, that are not used by the configuration" This reverts commit 74af1d7a68d15eb278cad28dc7cb1d2c51225750. --- .../uka/ilkd/key/settings/Configuration.java | 4 +-- .../settings/ProofIndependentSettings.java | 27 +++++++------------ .../key/gui/plugins/javac/JavacExtension.java | 3 --- .../key/gui/plugins/javac/JavacSettings.java | 5 +--- 4 files changed, 13 insertions(+), 26 deletions(-) diff --git a/key.core/src/main/java/de/uka/ilkd/key/settings/Configuration.java b/key.core/src/main/java/de/uka/ilkd/key/settings/Configuration.java index b6dbb981ecd..8efef1a3e1b 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/settings/Configuration.java +++ b/key.core/src/main/java/de/uka/ilkd/key/settings/Configuration.java @@ -525,7 +525,7 @@ private ConfigurationWriter printMap(Map value) { } indent -= 4; newline().printIndent(); - out.format("}"); + out.format(" }"); return this; } @@ -555,7 +555,7 @@ private ConfigurationWriter printSeq(Collection value) { } indent -= 4; newline().printIndent(); - out.format("]"); + out.format(" ]"); return this; } diff --git a/key.core/src/main/java/de/uka/ilkd/key/settings/ProofIndependentSettings.java b/key.core/src/main/java/de/uka/ilkd/key/settings/ProofIndependentSettings.java index 12b64dadf06..0646074f4af 100644 --- a/key.core/src/main/java/de/uka/ilkd/key/settings/ProofIndependentSettings.java +++ b/key.core/src/main/java/de/uka/ilkd/key/settings/ProofIndependentSettings.java @@ -53,8 +53,8 @@ public class ProofIndependentSettings { private final List settings = new LinkedList<>(); private final PropertyChangeListener settingsListener = e -> saveSettings(); - private Properties lastReadProperties; - private Configuration lastReadConfiguration; + private Properties lastReadedProperties; + private Configuration lastReadedConfiguration; private ProofIndependentSettings() { addSettings(smtSettings); @@ -74,11 +74,11 @@ public void addSettings(Settings settings) { if (!this.settings.contains(settings)) { this.settings.add(settings); settings.addPropertyChangeListener(settingsListener); - if (lastReadProperties != null) { - settings.readSettings(lastReadProperties); + if (lastReadedProperties != null) { + settings.readSettings(lastReadedProperties); } - if (lastReadConfiguration != null) { - settings.readSettings(lastReadConfiguration); + if (lastReadedConfiguration != null) { + settings.readSettings(lastReadedConfiguration); } } } @@ -106,22 +106,19 @@ private void load(File file) throws IOException { for (Settings settings : settings) { settings.readSettings(properties); } - lastReadProperties = properties; + lastReadedProperties = properties; } } else { - this.lastReadConfiguration = Configuration.load(file); + this.lastReadedConfiguration = Configuration.load(file); for (Settings settings : settings) { - settings.readSettings(lastReadConfiguration); + settings.readSettings(lastReadedConfiguration); } } } public void saveSettings() { if (!filename.getName().endsWith(".json")) { - Properties result = lastReadProperties == null - ? new Properties() - : new Properties(lastReadProperties); - + Properties result = new Properties(); for (Settings settings : settings) { settings.writeSettings(result); } @@ -138,10 +135,6 @@ public void saveSettings() { } Configuration config = new Configuration(); - if (lastReadConfiguration != null) { - config.overwriteWith(lastReadConfiguration); - } - for (var settings : settings) settings.writeSettings(config); if (!filename.exists()) { diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/javac/JavacExtension.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/javac/JavacExtension.java index a36732b5390..6dbe5220512 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/javac/JavacExtension.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/javac/JavacExtension.java @@ -179,9 +179,6 @@ private void loadProof(Proof selectedProof) throws RuntimeException { updateLabel(data); })).get(); } catch (InterruptedException | ExecutionException ex) { - lblStatus.setForeground(COLOR_ERROR.get()); - lblStatus.setIcon(ICON_ERROR.get(16)); - lblStatus.setText("Javac error"); throw new RuntimeException(ex); } } diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/javac/JavacSettings.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/javac/JavacSettings.java index 95827169cba..96488e6fa38 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/javac/JavacSettings.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/javac/JavacSettings.java @@ -13,10 +13,7 @@ */ public class JavacSettings extends AbstractPropertiesSettings { - /** - * The name of the category in the settings. - */ - public static final String CATEGORY = "Javac Extension"; + public static final String CATEGORY = "Type Checking"; /** * Config key for {@link #useProcessors}. From 7ca22418fc511ee6d7c7c90d513ce26cf77229ea Mon Sep 17 00:00:00 2001 From: PiisRational Date: Sat, 6 Dec 2025 18:34:28 +0100 Subject: [PATCH 7/7] un-revert the name of the Javac Settings --- .../de/uka/ilkd/key/gui/plugins/javac/JavacSettings.java | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/javac/JavacSettings.java b/key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/javac/JavacSettings.java index 96488e6fa38..95827169cba 100644 --- a/key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/javac/JavacSettings.java +++ b/key.ui/src/main/java/de/uka/ilkd/key/gui/plugins/javac/JavacSettings.java @@ -13,7 +13,10 @@ */ public class JavacSettings extends AbstractPropertiesSettings { - public static final String CATEGORY = "Type Checking"; + /** + * The name of the category in the settings. + */ + public static final String CATEGORY = "Javac Extension"; /** * Config key for {@link #useProcessors}.