Skip to content

Commit ee22098

Browse files
wadoonwadoon
committed
file UI
1 parent 84649fb commit ee22098

6 files changed

Lines changed: 226 additions & 58 deletions

File tree

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

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -9,6 +9,9 @@
99

1010
import de.uka.ilkd.key.gui.keyshortcuts.KeyStrokeManager;
1111

12+
import bibliothek.gui.dock.common.action.CAction;
13+
import bibliothek.gui.dock.common.action.CButton;
14+
1215
import static de.uka.ilkd.key.gui.keyshortcuts.KeyStrokeManager.SHORTCUT_KEY_MASK;
1316

1417
/**
@@ -155,4 +158,10 @@ public int getPriority() {
155158
protected void setPriority(int priority) {
156159
putValue(PRIORITY, priority);
157160
}
161+
162+
public CAction toCAction() {
163+
final var btn = new CButton(getName(), null);
164+
btn.addActionListener(this);
165+
return btn;
166+
}
158167
}

‎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
@@ -33,7 +33,7 @@ public class LlmExtension implements KeYGuiExtension, KeYGuiExtension.ContextMen
3333
KeYGuiExtension.Settings, KeYGuiExtension.Startup, KeYGuiExtension.LeftPanel,
3434
KeYGuiExtension.MainMenu {
3535
private KeyAction actionStartLlmPromptForCurrentProof;
36-
private TabPanel uiPrompt = new LlmPrompt();
36+
private TabPanel uiPrompt;
3737

3838
@Override
3939
public @NonNull List<Action> getContextActions(
@@ -61,6 +61,7 @@ public void preInit(MainWindow window, KeYMediator mediator) {
6161
@Override
6262
public @NonNull Collection<TabPanel> getPanels(@NonNull MainWindow window,
6363
@NonNull KeYMediator mediator) {
64+
uiPrompt = new LlmPrompt(window, mediator);
6465
return List.of(uiPrompt);
6566
}
6667

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

Lines changed: 152 additions & 53 deletions
Original file line numberDiff line numberDiff line change
@@ -5,17 +5,31 @@
55

66
import java.awt.*;
77
import java.awt.event.*;
8-
import java.util.Collection;
8+
import java.io.IOException;
9+
import java.net.URI;
10+
import java.util.*;
911
import java.util.List;
10-
import java.util.Map;
1112
import java.util.concurrent.ForkJoinPool;
13+
import java.util.function.Supplier;
1214
import javax.swing.*;
15+
import javax.swing.table.DefaultTableModel;
1316

17+
import de.uka.ilkd.key.core.KeYMediator;
18+
import de.uka.ilkd.key.core.KeYSelectionEvent;
19+
import de.uka.ilkd.key.core.KeYSelectionListener;
1420
import de.uka.ilkd.key.gui.MainWindow;
1521
import de.uka.ilkd.key.gui.actions.KeyAction;
1622
import de.uka.ilkd.key.gui.colors.ColorSettings;
23+
import de.uka.ilkd.key.gui.docking.DynamicCMenu;
1724
import de.uka.ilkd.key.gui.extension.api.TabPanel;
18-
25+
import de.uka.ilkd.key.gui.fonticons.IconFactory;
26+
import de.uka.ilkd.key.gui.help.HelpFacade;
27+
import de.uka.ilkd.key.proof.Proof;
28+
29+
import bibliothek.gui.dock.common.action.CAction;
30+
import bibliothek.gui.dock.common.action.CMenu;
31+
import bibliothek.gui.dock.common.action.CRadioButton;
32+
import bibliothek.gui.dock.common.action.CRadioGroup;
1933
import com.google.gson.GsonBuilder;
2034
import net.miginfocom.layout.CC;
2135
import net.miginfocom.layout.LC;
@@ -39,7 +53,7 @@ public class LlmPrompt extends JPanel implements TabPanel {
3953
ColorSettings.define("llm.output.bg.error", "Background color in chat of LLM answers",
4054
new Color(255, 180, 180, 255));
4155

42-
private static final ColorSettings.ColorProperty COLOR_BG_ANSWER = ColorSettings.define(
56+
public static final ColorSettings.ColorProperty COLOR_BG_ANSWER = ColorSettings.define(
4357
"llm.output.bg.answer", "Background color in chat of LLM answers", Color.LIGHT_GRAY);
4458

4559
private final JSplitPane splitPane = new JSplitPane(JSplitPane.VERTICAL_SPLIT);
@@ -51,21 +65,43 @@ public class LlmPrompt extends JPanel implements TabPanel {
5165

5266
private final KeyAction actionSwitchOrientation = new SwitchOrientationAction();
5367
private final SendPromptAction actionSendPrompt = new SendPromptAction();
68+
private final JPanel tblFiles = new JPanel(new MigLayout(new LC().fillX().wrapAfter(1)));
69+
private final DefaultTableModel modelFiles = new DefaultTableModel();
70+
71+
private final DefaultListModel<LlmPromptModel<?>> model = new DefaultListModel<>();
72+
private final MainWindow mainWindow;
73+
private final KeYMediator mediator;
74+
75+
public LlmPrompt(MainWindow mainWindow, @NonNull KeYMediator mediator) {
76+
this.mainWindow = mainWindow;
77+
this.mediator = mediator;
5478

55-
public LlmPrompt() {
5679
setLayout(new BorderLayout());
5780
add(splitPane, BorderLayout.CENTER);
5881
final var comp = new JScrollPane(pOutput);
5982
comp.getVerticalScrollBar().setUnitIncrement(16);
6083
splitPane.add(comp);
61-
splitPane.add(new JScrollPane(txtInput));
84+
var scrpInput = new JScrollPane(txtInput);
85+
var scrpFiles = new JScrollPane(tblFiles);
86+
var tabInputPanes = new JTabbedPane();
87+
tabInputPanes.addTab("Prompt", scrpInput);
88+
tabInputPanes.addTab("Files", scrpFiles);
89+
splitPane.add(tabInputPanes);
90+
91+
SwingUtilities.invokeLater(this::populateFiles);
92+
mediator.addKeYSelectionListener(new KeYSelectionListener() {
93+
@Override
94+
public void selectedProofChanged(KeYSelectionEvent<Proof> e) {
95+
populateFiles();
96+
}
97+
});
98+
6299

63100
handle(new Exception("Test Exception"));
64101
handle(new GsonBuilder().create().fromJson(
65102
"{\"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\"}}}]}",
66103
Map.class));
67-
addInput(">>> Input data");
68-
104+
addInput("Input data");
69105

70106
txtInput.addKeyListener(new KeyAdapter() {
71107
@Override
@@ -78,75 +114,71 @@ public void keyTyped(KeyEvent e) {
78114
});
79115
}
80116

81-
public static class OutputBox<T> extends JPanel {
82-
protected final T userData;
83-
protected final JEditorPane output = new JEditorPane();
84-
protected final JPanel buttons = new JPanel();
85-
protected final JPopupMenu menu = new JPopupMenu();
117+
static class AddFileAction extends KeyAction {
118+
private final Set<URI> selectedFiles;
119+
private final URI file;
86120

87-
public OutputBox(T userData) {
88-
this(userData, userData.toString());
89-
output.add(menu);
121+
public AddFileAction(URI file, Set<URI> selectedFiles) {
122+
this.file = file;
123+
this.selectedFiles = selectedFiles;
124+
setName(file.toString());
90125
}
91126

92-
public OutputBox(T userData, String text) {
93-
this.userData = userData;
94-
setLayout(new BorderLayout());
95-
output.setEditable(false);
96-
add(output, 0);
97-
buttons.setVisible(false);
98-
output.addMouseListener(new MouseAdapter() {
99-
@Override
100-
public void mouseEntered(MouseEvent e) {
101-
buttons.setVisible(true);
102-
}
103-
104-
@Override
105-
public void mouseExited(MouseEvent e) {
106-
buttons.setVisible(false);
107-
}
108-
});
109-
output.setText(text);
110-
111-
setBorder(BorderFactory.createEmptyBorder(10, 10, 10, 10));
127+
@Override
128+
public void actionPerformed(ActionEvent e) {
129+
var chk = (JCheckBox) e.getSource();
130+
if (chk.isSelected()) {
131+
selectedFiles.add(file);
132+
} else {
133+
selectedFiles.remove(file);
134+
}
112135
}
136+
}
113137

114-
@Override
115-
public void setBackground(Color bg) {
116-
super.setBackground(bg);
117-
if (output != null)
118-
output.setBackground(bg);
138+
private void populateFiles() {
139+
try {
140+
tblFiles.removeAll();
141+
LlmSession session = LlmUtils.getSession(mediator.getSelectedProof());
142+
List<URI> possibleFiles =
143+
new ArrayList<>(LlmUtils.getPossibleFiles(mediator.getSelectedProof()));
144+
Set<URI> selectedFiles = session.getSelectedFiles();
145+
possibleFiles.sort(Comparator.comparing(URI::toString));
146+
for (URI file : possibleFiles) {
147+
tblFiles.add(new JCheckBox(new AddFileAction(file, selectedFiles)));
148+
}
149+
tblFiles.invalidate();
150+
} catch (IOException e) {
151+
throw new RuntimeException(e);
119152
}
120153
}
121154

122155
private OutputBox<String> addInput(String text) {
123-
var o = addBox(text, new RepromptAction(text));
156+
var o = addBox(new LlmPromptModel(LlmPromptModel.Kind.INPUT, text, text),
157+
new RepromptAction(text));
124158
o.setBackground(COLOR_BG_INPUT.get());
125159
return o;
126160
}
127161

128-
private <T> OutputBox<T> addBox(T data, Action... actions) {
162+
private <T> OutputBox<T> addBox(LlmPromptModel<T> data, Action... actions) {
129163
OutputBox<T> box = new OutputBox<>(data);
130164
for (Action it : actions) {
131165
box.menu.add(it);
132166
}
133167
pOutput.add(box, new CC().growX());
168+
box.setBackground(data.kind().background().get());
134169
return box;
135170
}
136171

137172
private void handle(Map<String, Object> jsonResponse) {
138173
LOGGER.info("LLM prompt {}", jsonResponse);
139-
var o = new OutputBox<>(jsonResponse,
174+
final var text =
140175
((Map<String, Object>) ((Map<String, Object>) ((List<?>) jsonResponse.get("choices"))
141-
.get(0)).get("message")).get("content").toString());
142-
pOutput.add(o, new CC().growX());
143-
o.setBackground(COLOR_BG_ANSWER.get());
176+
.get(0)).get("message")).get("content").toString();
177+
addBox(new LlmPromptModel<>(LlmPromptModel.Kind.OUTPUT, text, jsonResponse));
144178
}
145179

146180
private void handle(Throwable e) {
147-
LOGGER.error("Error during LLM prompt", e);
148-
var box = addBox(e);
149-
box.setBackground(COLOR_BG_ERROR.get());
181+
addBox(new LlmPromptModel<>(LlmPromptModel.Kind.ERROR, e.toString(), e));
150182
}
151183

152184
@Override
@@ -160,8 +192,36 @@ private void handle(Throwable e) {
160192
}
161193

162194
@Override
163-
public @NonNull Collection<Action> getTitleActions() {
164-
return List.of(actionSwitchOrientation);
195+
public @NonNull Collection<CAction> getTitleCActions() {
196+
Supplier<CMenu> supplier = () -> {
197+
CMenu menu = new CMenu();
198+
menu.add(actionSwitchOrientation.toCAction());
199+
200+
CMenu menuModels = new CMenu("Models", null);
201+
menu.add(menuModels);
202+
var groupModels = new CRadioGroup();
203+
var llmSession =
204+
LlmUtils.getSession(MainWindow.getInstance().getMediator().getSelectedProof());
205+
206+
for (var m : LlmSettings.INSTANCE.getAvailableModels()) {
207+
var selected = m.equals(llmSession.getModel());
208+
final var action = new CRadioButton(m, null) {
209+
@Override
210+
protected void changed() {
211+
llmSession.setModel(m);
212+
}
213+
};
214+
action.setSelected(selected);
215+
groupModels.add(action);
216+
menuModels.add(action);
217+
}
218+
return menu;
219+
};
220+
221+
var a = new DynamicCMenu("Settings", IconFactory.properties(MainWindow.TOOLBAR_ICON_SIZE),
222+
supplier);
223+
var help = HelpFacade.createHelpButton("user/LLM/");
224+
return List.of(help, a);
165225
}
166226

167227
class SwitchOrientationAction extends KeyAction {
@@ -179,7 +239,7 @@ public void actionPerformed(ActionEvent e) {
179239
}
180240
}
181241

182-
class SelectContextAction extends KeyAction {
242+
static class SelectContextAction extends KeyAction {
183243
@Override
184244
public void actionPerformed(ActionEvent e) {
185245

@@ -240,3 +300,42 @@ public void actionPerformed(ActionEvent e) {
240300
}
241301
}
242302
}
303+
304+
305+
class OutputBox<T> extends JPanel {
306+
protected final LlmPromptModel<T> model;
307+
protected final JTextArea output = new JTextArea();
308+
protected final JPanel buttons = new JPanel();
309+
protected final JPopupMenu menu = new JPopupMenu();
310+
311+
public OutputBox(LlmPromptModel<T> userData) {
312+
this.model = userData;
313+
setLayout(new BorderLayout());
314+
output.setEditable(false);
315+
add(output, 0);
316+
buttons.setVisible(false);
317+
output.addMouseListener(new MouseAdapter() {
318+
@Override
319+
public void mouseEntered(MouseEvent e) {
320+
buttons.setVisible(true);
321+
}
322+
323+
@Override
324+
public void mouseExited(MouseEvent e) {
325+
buttons.setVisible(false);
326+
}
327+
});
328+
output.setText(userData.text());
329+
output.setLineWrap(true); // Makes the text wrap to the next line
330+
output.setWrapStyleWord(true); // Makes the text wrap full words, not just letters
331+
output.setComponentPopupMenu(menu);
332+
setBorder(BorderFactory.createEmptyBorder(10, 10, 10, 10));
333+
}
334+
335+
@Override
336+
public void setBackground(Color bg) {
337+
super.setBackground(bg);
338+
if (output != null)
339+
output.setBackground(bg);
340+
}
341+
}

‎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
@@ -3,6 +3,10 @@
33
* SPDX-License-Identifier: GPL-2.0-only */
44
package org.key_project.key.llm;
55

6+
import java.net.URI;
7+
import java.util.Set;
8+
import java.util.TreeSet;
9+
610
/**
711
*
812
* @author Alexander Weigl
@@ -12,6 +16,7 @@ public class LlmSession {
1216
private String model = "azure.gpt-4.1-mini";
1317
private String apiEndpoint;
1418
private String authToken;
19+
private Set<URI> selectedFiles = new TreeSet<>();
1520

1621
public LlmSession(String apiEndpoint, String authToken) {
1722
this.apiEndpoint = apiEndpoint;
@@ -41,4 +46,12 @@ public String getModel() {
4146
public void setModel(String model) {
4247
this.model = model;
4348
}
49+
50+
public Set<URI> getSelectedFiles() {
51+
return selectedFiles;
52+
}
53+
54+
public void setSelectedFiles(Set<URI> selectedFiles) {
55+
this.selectedFiles = selectedFiles;
56+
}
4457
}

0 commit comments

Comments
 (0)