Skip to content

Commit 0f775b4

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

29 files changed

Lines changed: 623 additions & 268 deletions

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

Lines changed: 29 additions & 34 deletions
Original file line numberDiff line numberDiff line change
@@ -3,17 +3,6 @@
33
* SPDX-License-Identifier: GPL-2.0-only */
44
package de.uka.ilkd.key.core;
55

6-
import java.io.File;
7-
import java.io.IOException;
8-
import java.lang.reflect.InvocationTargetException;
9-
import java.net.URL;
10-
import java.nio.file.Files;
11-
import java.nio.file.Path;
12-
import java.util.List;
13-
import java.util.Locale;
14-
import java.util.concurrent.Callable;
15-
import javax.xml.parsers.ParserConfigurationException;
16-
176
import de.uka.ilkd.key.control.UserInterfaceControl;
187
import de.uka.ilkd.key.gui.ExampleChooser;
198
import de.uka.ilkd.key.gui.MainWindow;
@@ -34,11 +23,9 @@
3423
import de.uka.ilkd.key.util.Debug;
3524
import de.uka.ilkd.key.util.KeYConstants;
3625
import de.uka.ilkd.key.util.rifl.RIFLTransformer;
37-
26+
import org.jspecify.annotations.Nullable;
3827
import org.key_project.util.java.IOUtil;
3928
import org.key_project.util.reflection.ClassLoaderUtil;
40-
41-
import org.jspecify.annotations.Nullable;
4229
import org.slf4j.Logger;
4330
import org.slf4j.LoggerFactory;
4431
import org.xml.sax.SAXException;
@@ -47,6 +34,17 @@
4734
import picocli.CommandLine.Parameters;
4835
import recoder.ParserException;
4936

37+
import javax.xml.parsers.ParserConfigurationException;
38+
import java.io.File;
39+
import java.io.IOException;
40+
import java.lang.reflect.InvocationTargetException;
41+
import java.net.URL;
42+
import java.nio.file.Files;
43+
import java.nio.file.Path;
44+
import java.util.List;
45+
import java.util.Locale;
46+
import java.util.concurrent.Callable;
47+
5048
/**
5149
* The main entry point for KeY
5250
* <p>
@@ -464,25 +462,27 @@ private AbstractMediatorUserInterfaceControl createUserInterface(List<Path> file
464462
}
465463

466464
public static void ensureExamplesAvailable() {
467-
File examplesDir = getExamplesDir() == null ? ExampleChooser.lookForExamples()
468-
: new File(getExamplesDir());
469-
if (!examplesDir.exists()) {
465+
Path examplesDir = getExamplesDir() == null
466+
? ExampleChooser.lookForExamples()
467+
: getExamplesDir();
468+
469+
if (!Files.exists(examplesDir)) {
470470
examplesDir = setupExamples();
471471
}
472-
setExamplesDir(examplesDir.getAbsolutePath());
472+
setExamplesDir(examplesDir.toAbsolutePath());
473473
}
474474

475-
private static File setupExamples() {
475+
private static Path setupExamples() {
476476
try {
477477
URL examplesURL = Main.class.getResource("/examples.zip");
478478
if (examplesURL == null) {
479479
throw new IOException("Missing examples.zip in resources");
480480
}
481481

482-
File tempDir = createTempDirectory();
482+
Path tempDir = createTempDirectory();
483483

484484
if (tempDir != null) {
485-
IOUtil.extractZip(examplesURL.openStream(), tempDir.toPath());
485+
IOUtil.extractZip(examplesURL.openStream(), tempDir);
486486
}
487487
return tempDir;
488488
} catch (IOException e) {
@@ -491,13 +491,9 @@ private static File setupExamples() {
491491
}
492492
}
493493

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)));
494+
private static Path createTempDirectory() throws IOException {
495+
Path tempDir = Files.createTempDirectory("keyheap-examples-");
496+
Runtime.getRuntime().addShutdownHook(new Thread(() -> IOUtil.delete(tempDir.toFile())));
501497
return tempDir;
502498
}
503499

@@ -541,7 +537,7 @@ private void preProcessInput()
541537
}
542538

543539
if (inputFiles != null && !inputFiles.isEmpty()) {
544-
Path f = inputFiles.get(0);
540+
Path f = inputFiles.getFirst();
545541
if (Files.isDirectory(f)) {
546542
workingDir = f;
547543
} else {
@@ -552,20 +548,19 @@ private void preProcessInput()
552548
}
553549
}
554550

555-
private static String EXAMPLE_DIR = null;
556-
557-
public static @Nullable String getExamplesDir() {
551+
private static Path EXAMPLE_DIR = null;
552+
public static @Nullable Path getExamplesDir() {
558553
return EXAMPLE_DIR;
559554
}
560555

561556
/**
562-
* Defines the examples directory. This method is used by the Eclipse
557+
* Defines the examples' directory. This method is used by the Eclipse
563558
* integration (KeY4Eclipse)
564559
* to use the examples extract from the plug-in into the workspace.
565560
*
566561
* @param newExamplesDir The new examples directory to use.
567562
*/
568-
public static void setExamplesDir(String newExamplesDir) {
563+
public static void setExamplesDir(Path newExamplesDir) {
569564
EXAMPLE_DIR = newExamplesDir;
570565
}
571566
}

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

Lines changed: 36 additions & 38 deletions
Original file line numberDiff line numberDiff line change
@@ -3,20 +3,19 @@
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;
6+
import org.slf4j.Logger;
7+
import org.slf4j.LoggerFactory;
8+
9+
import javax.swing.tree.DefaultMutableTreeNode;
10+
import javax.swing.tree.DefaultTreeModel;
911
import java.io.IOException;
1012
import java.nio.charset.StandardCharsets;
13+
import java.nio.file.Files;
14+
import java.nio.file.Path;
1115
import java.util.ArrayList;
1216
import java.util.Enumeration;
1317
import java.util.List;
1418
import java.util.Properties;
15-
import javax.swing.tree.DefaultMutableTreeNode;
16-
import javax.swing.tree.DefaultTreeModel;
17-
18-
import org.slf4j.Logger;
19-
import org.slf4j.LoggerFactory;
2019

2120
/**
2221
* This class wraps a {@link java.io.File} and has a special {@link #toString()} method only using
@@ -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;
@@ -143,12 +142,12 @@ public String toString() {
143142

144143
public void addToTreeModel(DefaultTreeModel model) {
145144
DefaultMutableTreeNode node =
146-
findChild((DefaultMutableTreeNode) model.getRoot(), getPath(), 0);
145+
findChild((DefaultMutableTreeNode) model.getRoot(), getPath(), 0);
147146
node.add(new DefaultMutableTreeNode(this));
148147
}
149148

150149
private DefaultMutableTreeNode findChild(DefaultMutableTreeNode root, String[] path,
151-
int from) {
150+
int from) {
152151
if (from == path.length) {
153152
return root;
154153
}
@@ -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,
173-
Properties properties) {
174-
try (BufferedReader r = new BufferedReader(new FileReader(file, StandardCharsets.UTF_8))) {
175-
String line;
171+
private static StringBuilder extractDescription(Path file, StringBuilder sb,
172+
Properties properties) {
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
}

0 commit comments

Comments
 (0)