# HG changeset patch
# User wenzelm
# Date 1626608480 -7200
# Node ID aa36845ad5ade22ad6cb4d09ddf03d61ef9817e5
# Parent  8c213672f6f3993b8040e2dbe9690b9a228e45bf
discontinued obsolete Apple (deprecated);

diff -r 8c213672f6f3 -r aa36845ad5ad src/Tools/GraphBrowser/graphbrowser/GraphBrowser.java
--- 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 @@
 		}
 	}
 }
-