LLM support in KeY UI

key.ui/build.gradle

@@ -39,6 +39,8 @@ dependencies {
     runtimeOnly project(":keyext.slicing")
     runtimeOnly project(":keyext.proofmanagement")
     runtimeOnly project(":keyext.isabelletranslation")
+
+    runtimeOnly project(":keyext.llm")
 }
 
 tasks.register('createExamplesZip', Zip) {

key.ui/src/main/java/de/uka/ilkd/key/gui/MainWindow.java

@@ -305,7 +305,9 @@ private MainWindow() {
         proofListener = new MainProofListener();
         userInterface = new WindowUserInterfaceControl(this);
         mediator = getMainWindowMediator(userInterface);
-        KeYGuiExtensionFacade.getStartupExtensions().forEach(it -> it.preInit(this, mediator));
+        KeYGuiExtensionFacade.getStartupExtensions()
+                .stream().filter(Objects::nonNull)
+                .forEach(it -> it.preInit(this, mediator));
 
         Config.DEFAULT.setDefaultFonts();
         ViewSettings vs = ProofIndependentSettings.DEFAULT_INSTANCE.getViewSettings();

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

@@ -7,6 +7,8 @@
 import javax.swing.Icon;
 import javax.swing.KeyStroke;
 
+import bibliothek.gui.dock.common.action.CAction;
+import bibliothek.gui.dock.common.action.CButton;
 import de.uka.ilkd.key.gui.keyshortcuts.KeyStrokeManager;
 
 import static de.uka.ilkd.key.gui.keyshortcuts.KeyStrokeManager.SHORTCUT_KEY_MASK;
@@ -155,4 +157,10 @@ public int getPriority() {
     protected void setPriority(int priority) {
         putValue(PRIORITY, priority);
     }
+
+    public CAction toCAction() {
+        final var btn = new CButton(getName(), null);
+        btn.addActionListener(this);
+        return btn;
+    }
 }

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

@@ -121,7 +121,7 @@ default void preInit(MainWindow window, KeYMediator mediator) {
 
         }
 
-        void init(MainWindow window, KeYMediator mediator);
+        default void init(MainWindow window, KeYMediator mediator) {};
     }
 
     /**

key.ui/src/main/java/de/uka/ilkd/key/gui/settings/SettingsPanel.java

@@ -4,22 +4,25 @@
 package de.uka.ilkd.key.gui.settings;
 
 
-import java.awt.*;
-import java.io.File;
-import java.util.Arrays;
-import java.util.List;
-import javax.swing.*;
-
 import de.uka.ilkd.key.gui.KeYFileChooser;
 import de.uka.ilkd.key.gui.fonticons.FontAwesomeSolid;
+import de.uka.ilkd.key.gui.fonticons.IconFactory;
 import de.uka.ilkd.key.gui.fonticons.IconFontSwing;
-
 import net.miginfocom.layout.AC;
 import net.miginfocom.layout.CC;
 import net.miginfocom.layout.LC;
 import net.miginfocom.swing.MigLayout;
 import org.jspecify.annotations.Nullable;
 
+import javax.swing.*;
+import java.awt.*;
+import java.awt.event.ActionListener;
+import java.io.File;
+import java.util.Arrays;
+import java.util.Collections;
+import java.util.List;
+import java.util.function.Function;
+
 /**
  * Extension of {@link SimpleSettingsPanel} which uses {@link MigLayout} to create a nice
  * three-column view.
@@ -36,19 +39,19 @@ public abstract class SettingsPanel extends SimpleSettingsPanel {
 
     protected SettingsPanel() {
         pCenter.setLayout(new MigLayout(
-            // set up rows:
-            new LC().fillX()
-                    // remove the padding after the help icon
-                    .insets(null, null, null, "0").wrapAfter(3),
-            // set up columns:
-            new AC().count(3).fill(1)
-                    // label column does not grow
-                    .grow(0f, 0)
-                    // input area does grow
-                    .grow(1000f, 1)
-                    // help icon always has the same size
-                    .size("16px", 2)
-                    .align("right", 0)));
+                // set up rows:
+                new LC().fillX()
+                        // remove the padding after the help icon
+                        .insets(null, null, null, "0").wrapAfter(3),
+                // set up columns:
+                new AC().count(3).fill(1)
+                        // label column does not grow
+                        .grow(0f, 0)
+                        // input area does grow
+                        .grow(1000f, 1)
+                        // help icon always has the same size
+                        .size("16px", 2)
+                        .align("right", 0)));
     }
 
     /**
@@ -116,7 +119,7 @@ protected <T> JComboBox<T> createSelection(T[] elements, Validator<T> validator)
      * @return
      */
     protected JCheckBox addCheckBox(String title, String info, boolean value,
-            final Validator<Boolean> validator) {
+                                    final Validator<Boolean> validator) {
         JCheckBox checkBox = createCheckBox(title, value, validator);
         addRowWithHelp(info, new JLabel(), checkBox);
         return checkBox;
@@ -132,7 +135,7 @@ protected JCheckBox addCheckBox(String title, String info, boolean value,
      * @return
      */
     protected JTextField addFileChooserPanel(String title, String file, String info, boolean isSave,
-            final Validator<String> validator) {
+                                             final Validator<String> validator) {
         JTextField textField = new JTextField(file);
         textField.addActionListener(e -> {
             try {
@@ -161,7 +164,7 @@ protected JTextField addFileChooserPanel(String title, String file, String info,
                 fileChooser = KeYFileChooser.getFileChooser("Save file");
                 fileChooser.setFileFilter(fileChooser.getAcceptAllFileFilter());
                 result = fileChooser.showSaveDialog((Component) e.getSource(),
-                    new File(textField.getText()));
+                        new File(textField.getText()));
             } else {
                 fileChooser = KeYFileChooser.getFileChooser("Open file");
                 fileChooser.setFileFilter(fileChooser.getAcceptAllFileFilter());
@@ -181,16 +184,16 @@ protected JTextField addFileChooserPanel(String title, String file, String info,
     /**
      * Adds a new combobox to the panel.
      *
-     * @param title label of the combo box
-     * @param info help text
+     * @param title          label of the combo box
+     * @param info           help text
      * @param selectionIndex which item to initially select
-     * @param validator validator
-     * @param items the items
-     * @param <T> the type of the items
+     * @param validator      validator
+     * @param items          the items
+     * @param <T>            the type of the items
      * @return the combo box
      */
     protected <T> JComboBox<T> addComboBox(String title, String info, int selectionIndex,
-            @Nullable Validator<T> validator, T... items) {
+                                           @Nullable Validator<T> validator, T... items) {
         JComboBox<T> comboBox = new JComboBox<>(items);
         comboBox.setSelectedIndex(selectionIndex);
         comboBox.addActionListener(e -> {
@@ -229,16 +232,75 @@ protected void addTitledComponent(String title, JComponent component, String hel
         addRowWithHelp(helpText, label, component);
     }
 
+    protected <T> JList<T> addListBox(String title, String info,
+                                      final Validator<List<T>> validator,
+                                      List<T> seq, Function<String, T> converter) {
+        var model = new DefaultListModel<T>();
+        model.addAll(seq);
+
+        JList<T> list = new JList<>(model);
+
+        var txtAdd = new JTextField();
+        var btnAdd = new JButton(IconFactory.PLUS_SQUARED.get(16f));
+        var btnRemove = new JButton(IconFactory.MINUS.get(16f));
+
+        JScrollPane field = new JScrollPane(list);
+
+        var panel = new JPanel(new MigLayout(new LC().fillX()));
+        panel.add(field, new CC().span(3).growX().wrap());
+        panel.add(txtAdd, new CC().growX());
+        panel.add(btnAdd, new CC().gapAfter("16px"));
+        panel.add(btnRemove);
+
+        JLabel lblTitle = new JLabel(title);
+        lblTitle.setLabelFor(list);
+        pCenter.add(lblTitle);
+        pCenter.add(new JSeparator(JSeparator.HORIZONTAL));
+        JLabel infoButton = createHelpLabel(info);
+        pCenter.add(infoButton, new CC().wrap());
+        pCenter.add(new JLabel());
+        pCenter.add(panel);
+
+        list.addListSelectionListener(e -> {
+            try {
+                if (validator != null) {
+                    List<T> ary = Collections.list(model.elements());
+                    validator.validate(ary);
+                }
+                demarkComponentAsErrornous(list);
+            } catch (Exception ex) {
+                markComponentAsErrornous(list, ex.getMessage());
+            }
+        });
+
+        final ActionListener addItem = e -> {
+            String value = txtAdd.getText();
+            if (value != null && !value.isEmpty()) {
+                model.addElement(converter.apply(value));
+            }
+        };
+        txtAdd.addActionListener(addItem);
+        btnAdd.addActionListener(addItem);
+
+        ActionListener removeItem = e -> {
+            if(list.getSelectedIndex() != -1) {
+                model.removeElementAt(list.getSelectedIndex());
+            }
+        };
+        btnRemove.addActionListener(removeItem);
+
+        return list;
+    }
 
     protected JTextArea addTextArea(String title, String text, String info,
-            final Validator<String> validator) {
+                                    final Validator<String> validator) {
         JScrollPane field = createTextArea(text, validator);
         addTitledComponent(title, field, info);
         return (JTextArea) field.getViewport().getView();
     }
 
     protected JTextArea addTextAreaWithoutScroll(String title, String text, String info,
-            final Validator<String> validator) {
+                                                 final Validator<String> validator) {
         JTextArea field = createTextAreaWithoutScroll(text, validator);
         addTitledComponent(title, field, info);
         return field;
@@ -253,15 +315,15 @@ protected JTextArea addTextAreaWithoutScroll(String title, String text, String i
      * @return
      */
     protected JTextField addTextField(String title, String text, String info,
-            final Validator<String> validator) {
+                                      final Validator<String> validator) {
         JTextField field = createTextField(text, validator);
         addTitledComponent(title, field, info);
         return field;
     }
 
 
     protected JTextField addTextField(String title, String text, String info,
-            final Validator<String> validator, JComponent additionalActions) {
+                                      final Validator<String> validator, JComponent additionalActions) {
         JTextField field = createTextField(text, validator);
         JLabel label = new JLabel(title);
         label.setLabelFor(field);
@@ -278,24 +340,24 @@ protected JTextField addTextField(String title, String text, String info,
      * also determines how the default {@link javax.swing.text.NumberFormatter} used by the
      * {@link JSpinner} formats entered Strings
      * (see {@link javax.swing.text.NumberFormatter#stringToValue(String)}).
-     *
+     * <p>
      * If there are additional restrictions for the entered values, the passed validator can check
      * those. The entered values have to be of a subclass of {@link Number} (as this is a number
      * text
      * field), otherwise the {@link Validator} will fail.
      *
-     * @param title the title of the text field
-     * @param min the minimum value that can be entered
-     * @param max the maximum value that can be entered
-     * @param step the step size used when changing the entered value using the JSpinner's arrow
-     *        buttons
-     * @param info arbitrary information about the text field
+     * @param title     the title of the text field
+     * @param min       the minimum value that can be entered
+     * @param max       the maximum value that can be entered
+     * @param step      the step size used when changing the entered value using the JSpinner's arrow
+     *                  buttons
+     * @param info      arbitrary information about the text field
      * @param validator a validator for checking the entered values
+     * @param <T>       the class of the minimum value
      * @return the created JSpinner
-     * @param <T> the class of the minimum value
      */
     protected <T extends Number & Comparable<T>> JSpinner addNumberField(String title, T min,
-            Comparable<T> max, Number step, String info, final Validator<Number> validator) {
+                                                                         Comparable<T> max, Number step, String info, final Validator<Number> validator) {
         JSpinner field = createNumberTextField(min, max, step, validator);
         addTitledComponent(title, field, info);
         return field;

key.ui/src/main/java/org/key_project/util/java/SwingUtil.java

@@ -40,6 +40,7 @@ private SwingUtil() {
      * @param uri the URI to be displayed in the user's default browser
      */
     public static void browse(URI uri) throws IOException {
+        LOGGER.info("Open {}", uri);
         try {
             Desktop.getDesktop().browse(uri);
         } catch (UnsupportedOperationException e) {

key.ui/src/main/resources/logback.xml

@@ -46,11 +46,20 @@
             <pattern>[%relative] %highlight(%-5level) %cyan(%logger{0}): %msg %n</pattern>
         </encoder>
         <filter class="ch.qos.logback.classic.filter.ThresholdFilter">
-            <level>TRACE</level>
+            <level>DEBUG</level>
         </filter>
     </appender>
+
     <logger name="key.devel" level="DEBUG">
         <appender-ref ref="STDERR"/>
     </logger>
 
+	<logger name="org.apache.hc.client5.http.headers" level="DEBUG">
+		<appender-ref ref="STDERR"/>
+
+	</logger>
+	<logger name="org.apache.hc.client5.http.wire">
+		<appender-ref ref="STDERR"/>
+
+	</logger>
 </configuration>

keyext.llm/build.gradle

@@ -0,0 +1,10 @@
+description = "LLM UI"
+
+dependencies {
+    implementation project(":key.core")
+    implementation project(":key.ui")
+
+    implementation("org.apache.httpcomponents.client5:httpclient5:5.5.1")
+    implementation("com.google.code.gson:gson:2.13.2")
+    implementation("org.slf4j:jcl-over-slf4j:1.7.5")
+}