Skip to content

Commit 97a994e

Browse files
wadoonwadoon
committed
file UI
1 parent a8d58af commit 97a994e

File tree

6 files changed

+217
-57
lines changed

6 files changed

+217
-57
lines changed

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

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -7,6 +7,8 @@
77
import javax.swing.Icon;
88
import javax.swing.KeyStroke;
99

10+
import bibliothek.gui.dock.common.action.CAction;
11+
import bibliothek.gui.dock.common.action.CButton;
1012
import de.uka.ilkd.key.gui.keyshortcuts.KeyStrokeManager;
1113

1214
import static de.uka.ilkd.key.gui.keyshortcuts.KeyStrokeManager.SHORTCUT_KEY_MASK;
@@ -155,4 +157,10 @@ public int getPriority() {
155157
protected void setPriority(int priority) {
156158
putValue(PRIORITY, priority);
157159
}
160+
161+
public CAction toCAction() {
162+
final var btn = new CButton(getName(), null);
163+
btn.addActionListener(this);
164+
return btn;
165+
}
158166
}

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

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -40,6 +40,7 @@ private SwingUtil() {
4040
* @param uri the URI to be displayed in the user's default browser
4141
*/
4242
public static void browse(URI uri) throws IOException {
43+
LOGGER.info("Open {}", uri);
4344
try {
4445
Desktop.getDesktop().browse(uri);
4546
} catch (UnsupportedOperationException e) {

‎keyext.llm/src/main/java/org/key_project/key/llm/LlmExtension.java‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -28,7 +28,7 @@
2828
public class LlmExtension implements KeYGuiExtension, KeYGuiExtension.ContextMenu,
2929
KeYGuiExtension.Settings, KeYGuiExtension.Startup, KeYGuiExtension.LeftPanel, KeYGuiExtension.MainMenu {
3030
private KeyAction actionStartLlmPromptForCurrentProof;
31-
private TabPanel uiPrompt = new LlmPrompt();
31+
private TabPanel uiPrompt;
3232

3333
@Override
3434
public @NonNull List<Action> getContextActions(
@@ -54,6 +54,7 @@ public void preInit(MainWindow window, KeYMediator mediator) {
5454

5555
@Override
5656
public @NonNull Collection<TabPanel> getPanels(@NonNull MainWindow window, @NonNull KeYMediator mediator) {
57+
uiPrompt = new LlmPrompt(window,mediator);
5758
return List.of(uiPrompt);
5859
}
5960

‎keyext.llm/src/main/java/org/key_project/key/llm/LlmPrompt.java‎

Lines changed: 145 additions & 52 deletions
Original file line numberDiff line numberDiff line change
@@ -1,10 +1,21 @@
11
package org.key_project.key.llm;
22

3+
import bibliothek.gui.dock.common.action.CAction;
4+
import bibliothek.gui.dock.common.action.CMenu;
5+
import bibliothek.gui.dock.common.action.CRadioButton;
6+
import bibliothek.gui.dock.common.action.CRadioGroup;
37
import com.google.gson.GsonBuilder;
8+
import de.uka.ilkd.key.core.KeYMediator;
9+
import de.uka.ilkd.key.core.KeYSelectionEvent;
10+
import de.uka.ilkd.key.core.KeYSelectionListener;
411
import de.uka.ilkd.key.gui.MainWindow;
512
import de.uka.ilkd.key.gui.actions.KeyAction;
613
import de.uka.ilkd.key.gui.colors.ColorSettings;
14+
import de.uka.ilkd.key.gui.docking.DynamicCMenu;
715
import de.uka.ilkd.key.gui.extension.api.TabPanel;
16+
import de.uka.ilkd.key.gui.fonticons.IconFactory;
17+
import de.uka.ilkd.key.gui.help.HelpFacade;
18+
import de.uka.ilkd.key.proof.Proof;
819
import net.miginfocom.layout.CC;
920
import net.miginfocom.layout.LC;
1021
import net.miginfocom.swing.MigLayout;
@@ -13,13 +24,15 @@
1324
import org.slf4j.LoggerFactory;
1425

1526
import javax.swing.*;
27+
import javax.swing.table.DefaultTableModel;
1628
import java.awt.*;
1729
import java.awt.event.*;
18-
import java.util.Arrays;
19-
import java.util.Collection;
30+
import java.io.IOException;
31+
import java.net.URI;
32+
import java.util.*;
2033
import java.util.List;
21-
import java.util.Map;
2234
import java.util.concurrent.ForkJoinPool;
35+
import java.util.function.Supplier;
2336

2437
/**
2538
*
@@ -35,7 +48,7 @@ public class LlmPrompt extends JPanel implements TabPanel {
3548
public static final ColorSettings.ColorProperty COLOR_BG_ERROR
3649
= ColorSettings.define("llm.output.bg.error", "Background color in chat of LLM answers", new Color(255, 180, 180, 255));
3750

38-
private static final ColorSettings.ColorProperty COLOR_BG_ANSWER
51+
public static final ColorSettings.ColorProperty COLOR_BG_ANSWER
3952
= ColorSettings.define("llm.output.bg.answer", "Background color in chat of LLM answers", Color.LIGHT_GRAY);
4053

4154
private final JSplitPane splitPane = new JSplitPane(JSplitPane.VERTICAL_SPLIT);
@@ -46,20 +59,42 @@ public class LlmPrompt extends JPanel implements TabPanel {
4659

4760
private final KeyAction actionSwitchOrientation = new SwitchOrientationAction();
4861
private final SendPromptAction actionSendPrompt = new SendPromptAction();
62+
private final JPanel tblFiles = new JPanel(new MigLayout(new LC().fillX().wrapAfter(1)));
63+
private final DefaultTableModel modelFiles = new DefaultTableModel();
64+
65+
private final DefaultListModel<LlmPromptModel<?>> model = new DefaultListModel<>();
66+
private final MainWindow mainWindow;
67+
private final KeYMediator mediator;
68+
69+
public LlmPrompt(MainWindow mainWindow, @NonNull KeYMediator mediator) {
70+
this.mainWindow = mainWindow;
71+
this.mediator = mediator;
4972

50-
public LlmPrompt() {
5173
setLayout(new BorderLayout());
5274
add(splitPane, BorderLayout.CENTER);
5375
final var comp = new JScrollPane(pOutput);
5476
comp.getVerticalScrollBar().setUnitIncrement(16);
5577
splitPane.add(comp);
56-
splitPane.add(new JScrollPane(txtInput));
78+
var scrpInput = new JScrollPane(txtInput);
79+
var scrpFiles = new JScrollPane(tblFiles);
80+
var tabInputPanes = new JTabbedPane();
81+
tabInputPanes.addTab("Prompt", scrpInput);
82+
tabInputPanes.addTab("Files", scrpFiles);
83+
splitPane.add(tabInputPanes);
84+
85+
SwingUtilities.invokeLater(this::populateFiles);
86+
mediator.addKeYSelectionListener(new KeYSelectionListener() {
87+
@Override
88+
public void selectedProofChanged(KeYSelectionEvent<Proof> e) {
89+
populateFiles();
90+
}
91+
});
92+
5793

5894
handle(new Exception("Test Exception"));
5995
handle(new GsonBuilder().create().fromJson("{\"id\":\"chatcmpl-CdLvyHhYLoKFk3F28rE6JgNJVGZHU\",\"created\":1763495142,\"model\":\"gpt-4.1-mini-2025-04-14\",\"object\":\"chat.completion\",\"system_fingerprint\":\"fp_3dcd5944f5\",\"choices\":[{\"finish_reason\":\"stop\",\"index\":0,\"message\":{\"content\":\"Die Rayleigh-Streuung beschreibt die Streuung von Licht an kleinen Teilchen, deren Größe viel kleiner ist als die Lichtwellenlänge. Dabei wird kurzwelliges Licht (blaues und violettes) stärker gestreut als langwelliges (rotes), was z.B. den blauen Himmel erklärt. Die Intensität der Streuung ist proportional zur vierten Potenz der Frequenz des Lichts.\",\"role\":\"assistant\",\"annotations\":[]},\"provider_specific_fields\":{\"content_filter_results\":{\"hate\":{\"filtered\":false,\"severity\":\"safe\"},\"protected_material_text\":{\"filtered\":false,\"detected\":false},\"self_harm\":{\"filtered\":false,\"severity\":\"safe\"},\"sexual\":{\"filtered\":false,\"severity\":\"safe\"},\"violence\":{\"filtered\":false,\"severity\":\"safe\"}}}}],\"usage\":{\"completion_tokens\":91,\"prompt_tokens\":36,\"total_tokens\":127,\"completion_tokens_details\":{\"accepted_prediction_tokens\":0,\"audio_tokens\":0,\"reasoning_tokens\":0,\"rejected_prediction_tokens\":0},\"prompt_tokens_details\":{\"audio_tokens\":0,\"cached_tokens\":0}},\"prompt_filter_results\":[{\"prompt_index\":0,\"content_filter_results\":{\"hate\":{\"filtered\":false,\"severity\":\"safe\"},\"jailbreak\":{\"filtered\":false,\"detected\":false},\"self_harm\":{\"filtered\":false,\"severity\":\"safe\"},\"sexual\":{\"filtered\":false,\"severity\":\"safe\"},\"violence\":{\"filtered\":false,\"severity\":\"safe\"}}}]}",
6096
Map.class));
61-
addInput(">>> Input data");
62-
97+
addInput("Input data");
6398

6499
txtInput.addKeyListener(new KeyAdapter() {
65100
@Override
@@ -71,73 +106,68 @@ public void keyTyped(KeyEvent e) {
71106
});
72107
}
73108

74-
public static class OutputBox<T> extends JPanel {
75-
protected final T userData;
76-
protected final JEditorPane output = new JEditorPane();
77-
protected final JPanel buttons = new JPanel();
78-
protected final JPopupMenu menu = new JPopupMenu();
109+
static class AddFileAction extends KeyAction {
110+
private final Set<URI> selectedFiles;
111+
private final URI file;
79112

80-
public OutputBox(T userData) {
81-
this(userData, userData.toString());
82-
output.add(menu);
113+
public AddFileAction(URI file, Set<URI> selectedFiles) {
114+
this.file = file;
115+
this.selectedFiles = selectedFiles;
116+
setName(file.toString());
83117
}
84118

85-
public OutputBox(T userData, String text) {
86-
this.userData = userData;
87-
setLayout(new BorderLayout());
88-
output.setEditable(false);
89-
add(output, 0);
90-
buttons.setVisible(false);
91-
output.addMouseListener(new MouseAdapter() {
92-
@Override
93-
public void mouseEntered(MouseEvent e) {
94-
buttons.setVisible(true);
95-
}
96-
97-
@Override
98-
public void mouseExited(MouseEvent e) {
99-
buttons.setVisible(false);
100-
}
101-
});
102-
output.setText(text);
103-
104-
setBorder(BorderFactory.createEmptyBorder(10, 10, 10, 10));
119+
@Override
120+
public void actionPerformed(ActionEvent e) {
121+
var chk = (JCheckBox) e.getSource();
122+
if (chk.isSelected()) {
123+
selectedFiles.add(file);
124+
} else {
125+
selectedFiles.remove(file);
126+
}
105127
}
128+
}
106129

107-
@Override
108-
public void setBackground(Color bg) {
109-
super.setBackground(bg);
110-
if (output != null) output.setBackground(bg);
130+
private void populateFiles() {
131+
try {
132+
tblFiles.removeAll();
133+
LlmSession session = LlmUtils.getSession(mediator.getSelectedProof());
134+
List<URI> possibleFiles = new ArrayList<>(LlmUtils.getPossibleFiles(mediator.getSelectedProof()));
135+
Set<URI> selectedFiles = session.getSelectedFiles();
136+
possibleFiles.sort(Comparator.comparing(URI::toString));
137+
for (URI file : possibleFiles) {
138+
tblFiles.add(new JCheckBox(new AddFileAction(file, selectedFiles)));
139+
}
140+
tblFiles.invalidate();
141+
} catch (IOException e) {
142+
throw new RuntimeException(e);
111143
}
112144
}
113145

114146
private OutputBox<String> addInput(String text) {
115-
var o = addBox(text, new RepromptAction(text));
147+
var o = addBox(new LlmPromptModel(LlmPromptModel.Kind.INPUT, text, text), new RepromptAction(text));
116148
o.setBackground(COLOR_BG_INPUT.get());
117149
return o;
118150
}
119151

120-
private <T> OutputBox<T> addBox(T data, Action... actions) {
152+
private <T> OutputBox<T> addBox(LlmPromptModel<T> data, Action... actions) {
121153
OutputBox<T> box = new OutputBox<>(data);
122154
for (Action it : actions) {
123155
box.menu.add(it);
124156
}
125157
pOutput.add(box, new CC().growX());
158+
box.setBackground(data.kind().background().get());
126159
return box;
127160
}
128161

129162
private void handle(Map<String, Object> jsonResponse) {
130163
LOGGER.info("LLM prompt {}", jsonResponse);
131-
var o = new OutputBox<>(jsonResponse,
132-
((Map<String, Object>) ((Map<String, Object>) ((List<?>) jsonResponse.get("choices")).get(0)).get("message")).get("content").toString());
133-
pOutput.add(o, new CC().growX());
134-
o.setBackground(COLOR_BG_ANSWER.get());
164+
final var text = ((Map<String, Object>) ((Map<String, Object>) ((List<?>)
165+
jsonResponse.get("choices")).get(0)).get("message")).get("content").toString();
166+
addBox(new LlmPromptModel<>(LlmPromptModel.Kind.OUTPUT, text, jsonResponse));
135167
}
136168

137169
private void handle(Throwable e) {
138-
LOGGER.error("Error during LLM prompt", e);
139-
var box = addBox(e);
140-
box.setBackground(COLOR_BG_ERROR.get());
170+
addBox(new LlmPromptModel<>(LlmPromptModel.Kind.ERROR, e.toString(), e));
141171
}
142172

143173
@Override
@@ -151,8 +181,34 @@ private void handle(Throwable e) {
151181
}
152182

153183
@Override
154-
public @NonNull Collection<Action> getTitleActions() {
155-
return List.of(actionSwitchOrientation);
184+
public @NonNull Collection<CAction> getTitleCActions() {
185+
Supplier<CMenu> supplier = () -> {
186+
CMenu menu = new CMenu();
187+
menu.add(actionSwitchOrientation.toCAction());
188+
189+
CMenu menuModels = new CMenu("Models", null);
190+
menu.add(menuModels);
191+
var groupModels = new CRadioGroup();
192+
var llmSession = LlmUtils.getSession(MainWindow.getInstance().getMediator().getSelectedProof());
193+
194+
for (var m : LlmSettings.INSTANCE.getAvailableModels()) {
195+
var selected = m.equals(llmSession.getModel());
196+
final var action = new CRadioButton(m, null) {
197+
@Override
198+
protected void changed() {
199+
llmSession.setModel(m);
200+
}
201+
};
202+
action.setSelected(selected);
203+
groupModels.add(action);
204+
menuModels.add(action);
205+
}
206+
return menu;
207+
};
208+
209+
var a = new DynamicCMenu("Settings", IconFactory.properties(MainWindow.TOOLBAR_ICON_SIZE), supplier);
210+
var help = HelpFacade.createHelpButton("user/LLM/");
211+
return List.of(help, a);
156212
}
157213

158214
class SwitchOrientationAction extends KeyAction {
@@ -170,7 +226,7 @@ public void actionPerformed(ActionEvent e) {
170226
}
171227
}
172228

173-
class SelectContextAction extends KeyAction {
229+
static class SelectContextAction extends KeyAction {
174230
@Override
175231
public void actionPerformed(ActionEvent e) {
176232

@@ -231,3 +287,40 @@ public void actionPerformed(ActionEvent e) {
231287
}
232288
}
233289
}
290+
291+
class OutputBox<T> extends JPanel {
292+
protected final LlmPromptModel<T> model;
293+
protected final JTextArea output = new JTextArea();
294+
protected final JPanel buttons = new JPanel();
295+
protected final JPopupMenu menu = new JPopupMenu();
296+
297+
public OutputBox(LlmPromptModel<T> userData) {
298+
this.model = userData;
299+
setLayout(new BorderLayout());
300+
output.setEditable(false);
301+
add(output, 0);
302+
buttons.setVisible(false);
303+
output.addMouseListener(new MouseAdapter() {
304+
@Override
305+
public void mouseEntered(MouseEvent e) {
306+
buttons.setVisible(true);
307+
}
308+
309+
@Override
310+
public void mouseExited(MouseEvent e) {
311+
buttons.setVisible(false);
312+
}
313+
});
314+
output.setText(userData.text());
315+
output.setLineWrap(true); //Makes the text wrap to the next line
316+
output.setWrapStyleWord(true); //Makes the text wrap full words, not just letters
317+
output.setComponentPopupMenu(menu);
318+
setBorder(BorderFactory.createEmptyBorder(10, 10, 10, 10));
319+
}
320+
321+
@Override
322+
public void setBackground(Color bg) {
323+
super.setBackground(bg);
324+
if (output != null) output.setBackground(bg);
325+
}
326+
}

‎keyext.llm/src/main/java/org/key_project/key/llm/LlmSession.java‎

Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,9 @@
11
package org.key_project.key.llm;
22

3+
import java.net.URI;
4+
import java.util.Set;
5+
import java.util.TreeSet;
6+
37
/**
48
*
59
* @author Alexander Weigl
@@ -9,6 +13,7 @@ public class LlmSession {
913
private String model = "azure.gpt-4.1-mini";
1014
private String apiEndpoint;
1115
private String authToken;
16+
private Set<URI> selectedFiles = new TreeSet<>();
1217

1318
public LlmSession(String apiEndpoint, String authToken) {
1419
this.apiEndpoint = apiEndpoint;
@@ -38,4 +43,12 @@ public String getModel() {
3843
public void setModel(String model) {
3944
this.model = model;
4045
}
46+
47+
public Set<URI> getSelectedFiles() {
48+
return selectedFiles;
49+
}
50+
51+
public void setSelectedFiles(Set<URI> selectedFiles) {
52+
this.selectedFiles = selectedFiles;
53+
}
4154
}

0 commit comments

Comments
 (0)