Skip to content

Commit d238fbc

Browse files
committed
working on documentation, now with json examples
1 parent 0f23b99 commit d238fbc

46 files changed

Lines changed: 733 additions & 290 deletions

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

key.ui/src/main/java/de/uka/ilkd/key/core/Main.java

Lines changed: 17 additions & 19 deletions
Original file line numberDiff line numberDiff line change
@@ -464,25 +464,27 @@ private AbstractMediatorUserInterfaceControl createUserInterface(List<Path> file
464464
}
465465

466466
public static void ensureExamplesAvailable() {
467-
File examplesDir = getExamplesDir() == null ? ExampleChooser.lookForExamples()
468-
: new File(getExamplesDir());
469-
if (!examplesDir.exists()) {
467+
Path examplesDir = getExamplesDir() == null
468+
? ExampleChooser.lookForExamples()
469+
: getExamplesDir();
470+
471+
if (!Files.exists(examplesDir)) {
470472
examplesDir = setupExamples();
471473
}
472-
setExamplesDir(examplesDir.getAbsolutePath());
474+
setExamplesDir(examplesDir.toAbsolutePath());
473475
}
474476

475-
private static File setupExamples() {
477+
private static Path setupExamples() {
476478
try {
477479
URL examplesURL = Main.class.getResource("/examples.zip");
478480
if (examplesURL == null) {
479481
throw new IOException("Missing examples.zip in resources");
480482
}
481483

482-
File tempDir = createTempDirectory();
484+
Path tempDir = createTempDirectory();
483485

484486
if (tempDir != null) {
485-
IOUtil.extractZip(examplesURL.openStream(), tempDir.toPath());
487+
IOUtil.extractZip(examplesURL.openStream(), tempDir);
486488
}
487489
return tempDir;
488490
} catch (IOException e) {
@@ -491,13 +493,9 @@ private static File setupExamples() {
491493
}
492494
}
493495

494-
private static File createTempDirectory() throws IOException {
495-
final File tempDir = File.createTempFile("keyheap-examples-", null);
496-
tempDir.delete();
497-
if (!tempDir.mkdir()) {
498-
return null;
499-
}
500-
Runtime.getRuntime().addShutdownHook(new Thread(() -> IOUtil.delete(tempDir)));
496+
private static Path createTempDirectory() throws IOException {
497+
Path tempDir = Files.createTempDirectory("keyheap-examples-");
498+
Runtime.getRuntime().addShutdownHook(new Thread(() -> IOUtil.delete(tempDir.toFile())));
501499
return tempDir;
502500
}
503501

@@ -541,7 +539,7 @@ private void preProcessInput()
541539
}
542540

543541
if (inputFiles != null && !inputFiles.isEmpty()) {
544-
Path f = inputFiles.get(0);
542+
Path f = inputFiles.getFirst();
545543
if (Files.isDirectory(f)) {
546544
workingDir = f;
547545
} else {
@@ -552,20 +550,20 @@ private void preProcessInput()
552550
}
553551
}
554552

555-
private static String EXAMPLE_DIR = null;
553+
private static Path EXAMPLE_DIR = null;
556554

557-
public static @Nullable String getExamplesDir() {
555+
public static @Nullable Path getExamplesDir() {
558556
return EXAMPLE_DIR;
559557
}
560558

561559
/**
562-
* Defines the examples directory. This method is used by the Eclipse
560+
* Defines the examples' directory. This method is used by the Eclipse
563561
* integration (KeY4Eclipse)
564562
* to use the examples extract from the plug-in into the workspace.
565563
*
566564
* @param newExamplesDir The new examples directory to use.
567565
*/
568-
public static void setExamplesDir(String newExamplesDir) {
566+
public static void setExamplesDir(Path newExamplesDir) {
569567
EXAMPLE_DIR = newExamplesDir;
570568
}
571569
}

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

Lines changed: 28 additions & 30 deletions
Original file line numberDiff line numberDiff line change
@@ -3,11 +3,10 @@
33
* SPDX-License-Identifier: GPL-2.0-only */
44
package de.uka.ilkd.key.gui;
55

6-
import java.io.BufferedReader;
7-
import java.io.File;
8-
import java.io.FileReader;
96
import java.io.IOException;
107
import java.nio.charset.StandardCharsets;
8+
import java.nio.file.Files;
9+
import java.nio.file.Path;
1110
import java.util.ArrayList;
1211
import java.util.Enumeration;
1312
import java.util.List;
@@ -74,59 +73,59 @@ public class Example {
7473
*/
7574
public static final String EXPORT_FILE_PREFIX = "example.exportFile.";
7675

77-
public final File exampleFile;
78-
public final File directory;
76+
public final Path exampleFile;
77+
public final Path directory;
7978
public final String description;
8079
public final Properties properties;
8180

82-
public Example(File file) throws IOException {
81+
public Example(Path file) throws IOException {
8382
this.exampleFile = file;
84-
this.directory = file.getParentFile();
83+
this.directory = file.getParent();
8584
this.properties = new Properties();
8685
StringBuilder sb = new StringBuilder();
8786
extractDescription(file, sb, properties);
8887
this.description = sb.toString();
8988
}
9089

91-
public File getDirectory() {
90+
public Path getDirectory() {
9291
return directory;
9392
}
9493

95-
public File getProofFile() {
96-
return new File(directory, properties.getProperty(KEY_PROOF_FILE, PROOF_FILE_NAME));
94+
public Path getProofFile() {
95+
return directory.resolve(properties.getProperty(KEY_PROOF_FILE, PROOF_FILE_NAME));
9796
}
9897

99-
public File getObligationFile() {
100-
return new File(directory, properties.getProperty(KEY_FILE, KEY_FILE_NAME));
98+
public Path getObligationFile() {
99+
return directory.resolve(properties.getProperty(KEY_FILE, KEY_FILE_NAME));
101100
}
102101

103102
public String getName() {
104-
return properties.getProperty(KEY_NAME, directory.getName());
103+
return properties.getProperty(KEY_NAME, directory.getFileName().toString());
105104
}
106105

107106
public String getDescription() {
108107
return description;
109108
}
110109

111-
public File getExampleFile() {
110+
public Path getExampleFile() {
112111
return exampleFile;
113112
}
114113

115-
public List<File> getAdditionalFiles() {
116-
var result = new ArrayList<File>();
114+
public List<Path> getAdditionalFiles() {
115+
var result = new ArrayList<Path>();
117116
int i = 1;
118117
while (properties.containsKey(ADDITIONAL_FILE_PREFIX + i)) {
119-
result.add(new File(directory, properties.getProperty(ADDITIONAL_FILE_PREFIX + i)));
118+
result.add(directory.resolve(properties.getProperty(ADDITIONAL_FILE_PREFIX + i)));
120119
i++;
121120
}
122121
return result;
123122
}
124123

125-
public List<File> getExportFiles() {
126-
ArrayList<File> result = new ArrayList<>();
124+
public List<Path> getExportFiles() {
125+
var result = new ArrayList<Path>();
127126
int i = 1;
128127
while (properties.containsKey(EXPORT_FILE_PREFIX + i)) {
129-
result.add(new File(directory, properties.getProperty(EXPORT_FILE_PREFIX + i)));
128+
result.add(directory.resolve(properties.getProperty(EXPORT_FILE_PREFIX + i)));
130129
i++;
131130
}
132131
return result;
@@ -169,24 +168,23 @@ public boolean hasProof() {
169168
return properties.containsKey(KEY_PROOF_FILE);
170169
}
171170

172-
private static StringBuilder extractDescription(File file, StringBuilder sb,
171+
private static StringBuilder extractDescription(Path file, StringBuilder sb,
173172
Properties properties) {
174-
try (BufferedReader r = new BufferedReader(new FileReader(file, StandardCharsets.UTF_8))) {
175-
String line;
173+
try {
176174
boolean emptyLineSeen = false;
177-
while ((line = r.readLine()) != null) {
175+
for (var line : Files.readAllLines(file, StandardCharsets.UTF_8)) {
178176
if (emptyLineSeen) {
179177
sb.append(line).append("\n");
180178
} else {
181179
String trimmed = line.trim();
182-
if (trimmed.length() == 0) {
180+
if (trimmed.isEmpty()) {
183181
emptyLineSeen = true;
184-
} else if (trimmed.startsWith("#")) {
185-
// ignore
186182
} else {
187-
String[] entry = trimmed.split(" *[:=] *", 2);
188-
if (entry.length > 1) {
189-
properties.put(entry[0], entry[1]);
183+
if (!trimmed.startsWith("#")) {
184+
String[] entry = trimmed.split(" *[:=] *", 2);
185+
if (entry.length > 1) {
186+
properties.put(entry[0], entry[1]);
187+
}
190188
}
191189
}
192190
}

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

Lines changed: 25 additions & 29 deletions
Original file line numberDiff line numberDiff line change
@@ -6,12 +6,12 @@
66
import java.awt.*;
77
import java.awt.event.MouseAdapter;
88
import java.awt.event.MouseEvent;
9-
import java.io.BufferedReader;
109
import java.io.File;
11-
import java.io.FileReader;
1210
import java.io.IOException;
13-
import java.nio.charset.StandardCharsets;
14-
import java.util.*;
11+
import java.nio.file.Files;
12+
import java.nio.file.Path;
13+
import java.nio.file.Paths;
14+
import java.util.ArrayList;
1515
import java.util.List;
1616
import javax.swing.*;
1717
import javax.swing.border.TitledBorder;
@@ -26,6 +26,7 @@
2626

2727
import org.key_project.util.java.IOUtil;
2828

29+
import org.jspecify.annotations.Nullable;
2930
import org.slf4j.Logger;
3031
import org.slf4j.LoggerFactory;
3132

@@ -61,23 +62,21 @@ public final class ExampleChooser extends JDialog {
6162
/**
6263
* The result value of the dialog. <code>null</code> if nothing to be loaded
6364
*/
64-
private File fileToLoad = null;
65+
private Path fileToLoad = null;
6566

6667
/**
6768
* The currently selected example. <code>null</code> if none selected
6869
*/
6970
private Example selectedExample;
7071

7172

72-
7373
// -------------------------------------------------------------------------
7474
// constructors
7575
// -------------------------------------------------------------------------
7676

77-
private ExampleChooser(File examplesDir) {
77+
private ExampleChooser(Path examplesDir) {
7878
super(MainWindow.getInstance(), "Load Example", true);
7979
assert examplesDir != null;
80-
assert examplesDir.isDirectory();
8180

8281
// create list panel
8382
final JPanel listPanel = new JPanel();
@@ -190,31 +189,30 @@ public void mouseClicked(MouseEvent e) {
190189
// internal methods
191190
// -------------------------------------------------------------------------
192191

193-
public static File lookForExamples() {
192+
public static Path lookForExamples() {
194193
// weigl: using java properties: -Dkey.examples.dir="..."
195194
if (System.getProperty(KEY_EXAMPLE_DIR) != null) {
196-
return new File(System.getProperty(KEY_EXAMPLE_DIR));
195+
return Paths.get(System.getProperty(KEY_EXAMPLE_DIR));
197196
}
198197

199198
// greatly simplified version without parent path lookup.
200199
File folder = new File(IOUtil.getProjectRoot(ExampleChooser.class), EXAMPLES_PATH);
201200
if (!folder.exists()) {
202201
folder = new File(IOUtil.getClassLocation(ExampleChooser.class), EXAMPLES_PATH);
203202
}
204-
return folder;
203+
return folder.toPath();
205204
}
206205

207-
private static String fileAsString(File f) {
206+
private static String fileAsString(Path f) {
208207
try {
209-
return IOUtil.readFrom(f);
208+
return Files.readString(f);
210209
} catch (IOException e) {
211210
LOGGER.error("Could not read file '{}'", f, e);
212211
return "<Error reading file: " + f + ">";
213212
}
214213
}
215214

216215

217-
218216
private void updateDescription() {
219217

220218
TreePath selectionPath = exampleList.getSelectionModel().getSelectionPath();
@@ -235,8 +233,8 @@ private void updateDescription() {
235233
if (p >= 0) {
236234
addTab(fileAsString.substring(p), "Proof Obligation", false);
237235
}
238-
for (File file : example.getAdditionalFiles()) {
239-
addTab(fileAsString(file), file.getName(), false);
236+
for (Path file : example.getAdditionalFiles()) {
237+
addTab(fileAsString(file), file.getFileName().toString(), false);
240238
}
241239
loadButton.setEnabled(true);
242240
loadProofButton.setEnabled(example.hasProof());
@@ -268,16 +266,16 @@ private void addTab(String string, String name, boolean wrap) {
268266
* Shows the dialog, using the passed examples directory. If null is passed, tries to find
269267
* examples directory on its own.
270268
*/
271-
public static File showInstance(String examplesDirString) {
269+
public static @Nullable Path showInstance(Path examplesDirString) {
272270
// get examples directory
273-
File examplesDir;
271+
Path examplesDir;
274272
if (examplesDirString == null) {
275273
examplesDir = lookForExamples();
276274
} else {
277-
examplesDir = new File(examplesDirString);
275+
examplesDir = examplesDirString;
278276
}
279277

280-
if (!examplesDir.isDirectory()) {
278+
if (!Files.isDirectory(examplesDir)) {
281279
JOptionPane.showMessageDialog(MainWindow.getInstance(),
282280
"The examples directory cannot be found.\n" + "Please install them at "
283281
+ (examplesDirString == null ? IOUtil.getProjectRoot(ExampleChooser.class) + "/"
@@ -304,19 +302,17 @@ public static File showInstance(String examplesDirString) {
304302
* @param examplesDir The examples directory to list examples in.
305303
* @return The found examples.
306304
*/
307-
public static List<Example> listExamples(File examplesDir) {
308-
List<Example> result = new LinkedList<>();
309-
310-
String line;
311-
final File index = new File(new File(examplesDir, "index"), "samplesIndex.txt");
312-
try (BufferedReader br =
313-
new BufferedReader(new FileReader(index, StandardCharsets.UTF_8))) {
314-
while ((line = br.readLine()) != null) {
305+
public static List<Example> listExamples(Path examplesDir) {
306+
List<Example> result = new ArrayList<>(64);
307+
308+
final Path index = examplesDir.resolve("index").resolve("samplesIndex.txt");
309+
try {
310+
for (var line : Files.readAllLines(index)) {
315311
line = line.trim();
316312
if (line.startsWith("#") || line.isEmpty()) {
317313
continue;
318314
}
319-
File f = new File(examplesDir, line);
315+
Path f = examplesDir.resolve(line);
320316
try {
321317
result.add(new Example(f));
322318
} catch (IOException e) {

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

Lines changed: 4 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,7 @@
44
package de.uka.ilkd.key.gui.actions;
55

66
import java.awt.event.ActionEvent;
7-
import java.io.File;
7+
import java.nio.file.Path;
88

99
import de.uka.ilkd.key.core.Main;
1010
import de.uka.ilkd.key.gui.ExampleChooser;
@@ -16,12 +16,6 @@
1616
* Opens a file dialog allowing to select the example to be loaded
1717
*/
1818
public final class OpenExampleAction extends MainWindowAction {
19-
20-
/**
21-
*
22-
*/
23-
private static final long serialVersionUID = -7703620988220254791L;
24-
2519
public OpenExampleAction(MainWindow mainWindow) {
2620
super(mainWindow);
2721
setName("Load Example...");
@@ -30,10 +24,10 @@ public OpenExampleAction(MainWindow mainWindow) {
3024
}
3125

3226
public void actionPerformed(ActionEvent e) {
33-
File file = ExampleChooser.showInstance(Main.getExamplesDir());
27+
Path file = ExampleChooser.showInstance(Main.getExamplesDir());
3428
if (file != null) {
35-
KeYFileChooser.getFileChooser("Select file to load").setSelectedFile(file);
36-
mainWindow.loadProblem(file.toPath());
29+
KeYFileChooser.getFileChooser("Select file to load").setSelectedFile(file.toFile());
30+
mainWindow.loadProblem(file);
3731
}
3832
}
3933
}

0 commit comments

Comments
 (0)