Skip to content

Commit 6b1f07a

Browse files
kovzolkovzol
committed
Fix running from EXE on Windows, center app on CheerpJ, optimize window size
1 parent 5da3120 commit 6b1f07a

2 files changed

Lines changed: 138 additions & 113 deletions

File tree

‎src/index.html‎

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -6,6 +6,14 @@
66
<title>Java Geometry Expert CheerpJ version</title>
77
<script src="https://cjrtnc.leaningtech.com/4.1/loader.js"></script>
88
</head>
9+
10+
<style>
11+
div {
12+
margin: auto;
13+
text-align: center;
14+
}
15+
</style>
16+
917
<body>
1018
<script>
1119
function execCb(cmdPath, argsArray) {

‎src/main/java/wprover/GExpert.java‎

Lines changed: 130 additions & 113 deletions
Original file line numberDiff line numberDiff line change
@@ -817,11 +817,13 @@ void addAllExamples(JMenu menu) {
817817
void addDirectory(JMenu menu, String resourceDir) {
818818
try {
819819
ClassLoader cl = Thread.currentThread().getContextClassLoader();
820-
URL dirUrl = cl.getResource(resourceDir + "/");
821-
if (dirUrl == null) return;
820+
try {
821+
URL dirUrl = cl.getResource(resourceDir + "/");
822+
if (dirUrl == null) return;
822823

823-
if (dirUrl.getProtocol().equals("file")) {
824+
// 1. Assume first that we are
824825
// running in IDE/Gradle on disk
826+
// if (dirUrl.getProtocol().equals("file")) ...
825827
File folder = new File(dirUrl.toURI());
826828
File[] files = folder.listFiles();
827829
// Sort files using custom comparator
@@ -863,134 +865,147 @@ else if (name2.matches("^\\d+.*")) {
863865
for (File f : files) {
864866
handleEntry(menu, resourceDir, f.getName(), f.isDirectory());
865867
}
866-
} else {
867-
// running from JAR(specifically for CheerpJ)
868-
String path = resourceDir + "/";
868+
if (files.length > 0) {
869+
// we assume that at least one file was found
870+
return; // so no further work is needed
871+
}
872+
} catch (Exception ex) {
873+
// Problem when getting URL.
874+
}
875+
876+
// 2. assume that running from JAR (specifically for CheerpJ)
877+
String path = resourceDir + "/";
878+
try {
879+
// Use JarFile approach to get all entries
869880
try {
870-
// Use JarFile approach to get all entries
871-
URL jarUrl = cl.getResource(path);
872-
if (jarUrl != null) {
873-
String jarPath = jarUrl.toString();
874-
if (jarPath.startsWith("jar:file:")) {
875-
jarPath = jarPath.substring(9, jarPath.indexOf("!"));
876-
try (JarFile jar = new JarFile(jarPath)) {
877-
Enumeration<JarEntry> entries = jar.entries();
878-
// first collect all entries to process
879-
java.util.Map<String, Boolean> processedDirs = new java.util.HashMap<>();
880-
java.util.List<String> filesToProcess = new java.util.ArrayList<String>();
881-
882-
while (entries.hasMoreElements()) {
883-
JarEntry entry = entries.nextElement();
884-
String entryName = entry.getName();
885-
886-
if (entryName.startsWith(path)) {
887-
String relativePath = entryName.substring(path.length());
888-
if (relativePath.isEmpty()) continue;
889-
890-
int slashIndex = relativePath.indexOf('/');
891-
if (slashIndex == -1) {
892-
filesToProcess.add(relativePath);
893-
} else {
894-
// subdirectory
895-
String dirName = relativePath.substring(0, slashIndex);
896-
if (!processedDirs.containsKey(dirName)) {
897-
processedDirs.put(dirName, true);
881+
URL jarUrl = cl.getResource(path);
882+
if (jarUrl != null) {
883+
String jarPath = jarUrl.toString();
884+
if (jarPath.startsWith("jar:file:")) {
885+
jarPath = jarPath.substring(9, jarPath.indexOf("!"));
886+
jarPath = jarPath.replace("%20", " "); // fix path
887+
try (JarFile jar = new JarFile(jarPath)) {
888+
Enumeration<JarEntry> entries = jar.entries();
889+
// first collect all entries to process
890+
java.util.Map<String, Boolean> processedDirs = new java.util.HashMap<>();
891+
java.util.List<String> filesToProcess = new java.util.ArrayList<String>();
892+
893+
while (entries.hasMoreElements()) {
894+
JarEntry entry = entries.nextElement();
895+
String entryName = entry.getName();
896+
897+
if (entryName.startsWith(path)) {
898+
String relativePath = entryName.substring(path.length());
899+
if (relativePath.isEmpty()) continue;
900+
901+
int slashIndex = relativePath.indexOf('/');
902+
if (slashIndex == -1) {
903+
filesToProcess.add(relativePath);
904+
} else {
905+
// subdirectory
906+
String dirName = relativePath.substring(0, slashIndex);
907+
if (!processedDirs.containsKey(dirName)) {
908+
processedDirs.put(dirName, true);
909+
}
898910
}
899911
}
900912
}
901-
}
902913

903-
// Sort directories using custom comparator
904-
java.util.List<String> dirNames = new java.util.ArrayList<>(processedDirs.keySet());
905-
Collections.sort(dirNames, new Comparator<String>() {
906-
@Override
907-
public int compare(String name1, String name2) {
908-
// Check if both names start with numbers
909-
if (name1.matches("^\\d+.*") && name2.matches("^\\d+.*")) {
910-
// Extract the numeric prefix
911-
String num1 = name1.replaceAll("^(\\d+).*", "$1");
912-
String num2 = name2.replaceAll("^(\\d+).*", "$1");
913-
914-
// If numeric parts are different, compare them numerically
915-
if (!num1.equals(num2)) {
916-
return Integer.compare(Integer.parseInt(num1), Integer.parseInt(num2));
914+
// Sort directories using custom comparator
915+
java.util.List<String> dirNames = new java.util.ArrayList<>(processedDirs.keySet());
916+
Collections.sort(dirNames, new Comparator<String>() {
917+
@Override
918+
public int compare(String name1, String name2) {
919+
// Check if both names start with numbers
920+
if (name1.matches("^\\d+.*") && name2.matches("^\\d+.*")) {
921+
// Extract the numeric prefix
922+
String num1 = name1.replaceAll("^(\\d+).*", "$1");
923+
String num2 = name2.replaceAll("^(\\d+).*", "$1");
924+
925+
// If numeric parts are different, compare them numerically
926+
if (!num1.equals(num2)) {
927+
return Integer.compare(Integer.parseInt(num1), Integer.parseInt(num2));
928+
}
917929
}
930+
// If one name starts with a number and the other doesn't, prioritize the one with number
931+
else if (name1.matches("^\\d+.*")) {
932+
return -1;
933+
}
934+
else if (name2.matches("^\\d+.*")) {
935+
return 1;
936+
}
937+
938+
// Otherwise, use alphabetical order
939+
return name1.compareTo(name2);
918940
}
919-
// If one name starts with a number and the other doesn't, prioritize the one with number
920-
else if (name1.matches("^\\d+.*")) {
921-
return -1;
922-
}
923-
else if (name2.matches("^\\d+.*")) {
924-
return 1;
925-
}
941+
});
926942

927-
// Otherwise, use alphabetical order
928-
return name1.compareTo(name2);
943+
// Process directories in sorted order
944+
for (String dirName : dirNames) {
945+
handleEntry(menu, resourceDir, dirName, true);
929946
}
930-
});
931947

932-
// Process directories in sorted order
933-
for (String dirName : dirNames) {
934-
handleEntry(menu, resourceDir, dirName, true);
935-
}
936-
937-
// Sort files using custom comparator
938-
Collections.sort(filesToProcess, new Comparator<String>() {
939-
@Override
940-
public int compare(String name1, String name2) {
941-
// Check if both names start with numbers
942-
if (name1.matches("^\\d+.*") && name2.matches("^\\d+.*")) {
943-
// Extract the numeric prefix
944-
String num1 = name1.replaceAll("^(\\d+).*", "$1");
945-
String num2 = name2.replaceAll("^(\\d+).*", "$1");
946-
947-
// If numeric parts are different, compare them numerically
948-
if (!num1.equals(num2)) {
949-
return Integer.compare(Integer.parseInt(num1), Integer.parseInt(num2));
948+
// Sort files using custom comparator
949+
Collections.sort(filesToProcess, new Comparator<String>() {
950+
@Override
951+
public int compare(String name1, String name2) {
952+
// Check if both names start with numbers
953+
if (name1.matches("^\\d+.*") && name2.matches("^\\d+.*")) {
954+
// Extract the numeric prefix
955+
String num1 = name1.replaceAll("^(\\d+).*", "$1");
956+
String num2 = name2.replaceAll("^(\\d+).*", "$1");
957+
958+
// If numeric parts are different, compare them numerically
959+
if (!num1.equals(num2)) {
960+
return Integer.compare(Integer.parseInt(num1), Integer.parseInt(num2));
961+
}
950962
}
963+
// If one name starts with a number and the other doesn't, prioritize the one with number
964+
else if (name1.matches("^\\d+.*")) {
965+
return -1;
966+
}
967+
else if (name2.matches("^\\d+.*")) {
968+
return 1;
969+
}
970+
971+
// Otherwise, use alphabetical order
972+
return name1.compareTo(name2);
951973
}
952-
// If one name starts with a number and the other doesn't, prioritize the one with number
953-
else if (name1.matches("^\\d+.*")) {
954-
return -1;
955-
}
956-
else if (name2.matches("^\\d+.*")) {
957-
return 1;
958-
}
974+
});
959975

960-
// Otherwise, use alphabetical order
961-
return name1.compareTo(name2);
976+
// process all files in this directory
977+
for (String fileName : filesToProcess) {
978+
handleEntry(menu, resourceDir, fileName, false);
962979
}
963-
});
964-
965-
// process all files in this directory
966-
for (String fileName : filesToProcess) {
967-
handleEntry(menu, resourceDir, fileName, false);
968980
}
969981
}
970-
} else {
971-
// fallback to JarInputStream if jar-file protocol not available
972-
try (InputStream is = cl.getResourceAsStream(path);
973-
JarInputStream jin = new JarInputStream(is)) {
974-
JarEntry e;
975-
while ((e = jin.getNextJarEntry()) != null) {
976-
String name = e.getName();
977-
if (name.startsWith(path)) {
978-
String entry = name.substring(path.length());
979-
if (!entry.isEmpty() && !entry.contains("/")) {
980-
handleEntry(menu, resourceDir, entry, false);
981-
}
982-
}
983-
}
982+
return; // success
983+
}
984+
985+
} catch (Exception ex) {
986+
// Error with file handling.
987+
}
988+
// 3. fallback to JarInputStream if jar-file protocol not available
989+
try (InputStream is = cl.getResourceAsStream(path);
990+
JarInputStream jin = new JarInputStream(is)) {
991+
JarEntry e;
992+
while ((e = jin.getNextJarEntry()) != null) {
993+
String name = e.getName();
994+
if (name.startsWith(path)) {
995+
String entry = name.substring(path.length());
996+
if (!entry.isEmpty() && !entry.contains("/")) {
997+
handleEntry(menu, resourceDir, entry, false);
984998
}
985999
}
9861000
}
987-
} catch (Exception e) {
988-
// log the exception but continue processing
989-
e.printStackTrace();
9901001
}
1002+
} catch (Exception e) {
1003+
// log the exception but continue processing
1004+
e.printStackTrace();
9911005
}
992-
} catch (Exception ex) {
993-
ex.printStackTrace();
1006+
} catch (Exception e) {
1007+
// log the exception but continue processing
1008+
e.printStackTrace();
9941009
}
9951010
}
9961011

@@ -3695,10 +3710,12 @@ private static void createAndShowGUI() {
36953710
frame.pack();
36963711

36973712
Dimension screenSize = Toolkit.getDefaultToolkit().getScreenSize();
3698-
frame.setSize(1200, 900);
3713+
int frameWidth = 1000;
3714+
int frameHeight = 700;
3715+
frame.setSize(frameWidth, frameHeight);
36993716

3700-
frame.setLocation((int) (screenSize.getWidth() - 1200) / 2,
3701-
(int) (screenSize.getHeight() - 900) / 2); //center
3717+
frame.setLocation((int) (screenSize.getWidth() - frameWidth) / 2,
3718+
(int) (screenSize.getHeight() - frameHeight) / 2); //center
37023719
frame.setVisible(true);
37033720

37043721
// In case there were command line requests, let us do them:

0 commit comments

Comments
 (0)