--- a/src/Tools/GraphBrowser/graphbrowser/GraphBrowser.java Sun Jul 18 13:27:23 2021 +0200
+++ b/src/Tools/GraphBrowser/graphbrowser/GraphBrowser.java Sun Jul 18 13:41:20 2021 +0200
@@ -4,27 +4,23 @@
Options: :tabSize=4:
This is the graph browser's main class. It contains the "main(...)"
- method, which is used for the stand-alone version, as well as
- "init(...)", "start(...)" and "stop(...)" methods which are used for
- the applet version.
+ method, which is used for the stand-alone version.
Note: GraphBrowser is designed for the 1.1.x version of the JDK.
***************************************************************************/
package isabelle.graphbrowser;
import java.awt.*;
-import java.applet.*;
import java.io.*;
import java.util.*;
import java.net.*;
import isabelle.awt.*;
-public class GraphBrowser extends Applet {
+public class GraphBrowser extends Panel {
GraphView gv;
TreeBrowser tb=null;
String gfname;
- static boolean isApplet;
static Frame f;
public GraphBrowser(String name) {
@@ -34,83 +30,71 @@
public GraphBrowser() {}
public void showWaitMessage() {
- if (isApplet)
- getAppletContext().showStatus("calculating layout, please wait ...");
- else {
- f.setCursor(new Cursor(Cursor.WAIT_CURSOR));
- }
+ f.setCursor(new Cursor(Cursor.WAIT_CURSOR));
}
public void showReadyMessage() {
- if (isApplet)
- getAppletContext().showStatus("ready !");
- else {
- f.setCursor(new Cursor(Cursor.DEFAULT_CURSOR));
- }
+ f.setCursor(new Cursor(Cursor.DEFAULT_CURSOR));
}
public void viewFile(String fname) {
try {
- if (isApplet)
- getAppletContext().showDocument(new URL(getDocumentBase(), fname), "_blank");
- else {
- String path = gfname.substring(0, gfname.lastIndexOf('/') + 1);
- Reader rd;
- BufferedReader br;
- String line, text = "";
+ String path = gfname.substring(0, gfname.lastIndexOf('/') + 1);
+ Reader rd;
+ BufferedReader br;
+ String line, text = "";
+
+ try {
+ rd = new BufferedReader(new InputStreamReader((new URL(fname)).openConnection().getInputStream()));
+ } catch (Exception exn) {
+ rd = new FileReader(path + fname);
+ }
+ br = new BufferedReader(rd);
- try {
- rd = new BufferedReader(new InputStreamReader((new URL(fname)).openConnection().getInputStream()));
- } catch (Exception exn) {
- rd = new FileReader(path + fname);
- }
- br = new BufferedReader(rd);
+ while ((line = br.readLine()) != null)
+ text += line + "\n";
+
+ if (fname.endsWith(".html")) {
+ /**** convert HTML to text (just a quick hack) ****/
- while ((line = br.readLine()) != null)
- text += line + "\n";
-
- if (fname.endsWith(".html")) {
- /**** convert HTML to text (just a quick hack) ****/
-
- String buf="";
- char[] text2,text3;
- int i,j=0;
- boolean special=false, html=false;
- char ctrl;
+ String buf="";
+ char[] text2,text3;
+ int i,j=0;
+ boolean special=false, html=false;
+ char ctrl;
- text2 = text.toCharArray();
- text3 = new char[text.length()];
- for (i = 0; i < text.length(); i++) {
- char c = text2[i];
- if (c == '&') {
- special = true;
- buf = "";
- } else if (special) {
- if (c == ';') {
- special = false;
- if (buf.equals("lt"))
- text3[j++] = '<';
- else if (buf.equals("gt"))
- text3[j++] = '>';
- else if (buf.equals("amp"))
- text3[j++] = '&';
- } else
- buf += c;
- } else if (c == '<') {
- html = true;
- ctrl = text2[i+1];
- } else if (c == '>')
- html = false;
- else if (!html)
- text3[j++] = c;
- }
- text = String.valueOf(text3);
- }
-
- Frame f=new TextFrame(fname.substring(fname.lastIndexOf('/')+1),text);
- f.setSize(500,600);
- f.setVisible(true);
- }
+ text2 = text.toCharArray();
+ text3 = new char[text.length()];
+ for (i = 0; i < text.length(); i++) {
+ char c = text2[i];
+ if (c == '&') {
+ special = true;
+ buf = "";
+ } else if (special) {
+ if (c == ';') {
+ special = false;
+ if (buf.equals("lt"))
+ text3[j++] = '<';
+ else if (buf.equals("gt"))
+ text3[j++] = '>';
+ else if (buf.equals("amp"))
+ text3[j++] = '&';
+ } else
+ buf += c;
+ } else if (c == '<') {
+ html = true;
+ ctrl = text2[i+1];
+ } else if (c == '>')
+ html = false;
+ else if (!html)
+ text3[j++] = c;
+ }
+ text = String.valueOf(text3);
+ }
+
+ Frame f=new TextFrame(fname.substring(fname.lastIndexOf('/')+1),text);
+ f.setSize(500,600);
+ f.setVisible(true);
} catch (Exception exn) {
System.err.println("Can't read file "+fname);
}
@@ -168,22 +152,7 @@
}
}
- public void init() {
- isApplet=true;
- gfname=getParameter("graphfile");
- try {
- InputStream is=(new URL(getDocumentBase(), gfname)).openConnection().getInputStream();
- initBrowser(is, false);
- is.close();
- } catch (MalformedURLException exn) {
- System.err.println("Invalid URL: "+gfname);
- } catch (IOException exn) {
- System.err.println("I/O error while reading "+gfname+".");
- }
- }
-
public static void main(String[] args) {
- isApplet=false;
try {
GraphBrowser gb=new GraphBrowser(args.length > 0 ? args[0] : "");
if (args.length > 0) {
@@ -212,4 +181,3 @@
}
}
}
-