finish getting reference.zip to work with Java Mode

This commit is contained in:
Ben Fry
2021-08-08 10:47:14 -04:00
parent ed5b9c0a83
commit 6dad06d6c4
4 changed files with 59 additions and 138 deletions

View File

@@ -74,7 +74,6 @@ public class JavaEditor extends Editor {
JMenu modeMenu;
// protected JMenuItem inspectorItem;
// static final int ERROR_TAB_INDEX = 0;
protected PreprocService preprocService;
@@ -90,6 +89,11 @@ public class JavaEditor extends Editor {
static private final boolean SHOW_AST_VIEWER = false;
private ASTViewer astViewer;
/** P5 in decimal; if there are complaints, move to preferences.txt */
static final int REFERENCE_PORT = 8053;
Boolean useReferenceServer;
WebServer referenceServer;
protected JavaEditor(Base base, String path, EditorState state,
Mode mode) throws EditorException {
@@ -1199,6 +1203,34 @@ public class JavaEditor extends Editor {
}
public void showReference(String filename) {
if (useReferenceServer == null) {
File referenceZip = new File(mode.getFolder(), "reference.zip");
if (referenceZip.exists()) {
try {
referenceServer = new WebServer(referenceZip, REFERENCE_PORT);
useReferenceServer = true;
} catch (IOException e) {
Messages.showWarning("Reference Server Problem", "Error while starting the documentation server.");
}
} else {
useReferenceServer = false;
}
}
if (useReferenceServer) {
String url = referenceServer.getPrefix() + "reference/" + filename;
Platform.openURL(url);
} else {
File file = new File(mode.getReferenceFolder(), filename);
showReferenceFile(file);
}
}
public void statusError(String what) {
super.statusError(what);
// new Exception("deactivating RUN").printStackTrace();