--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/GraphBrowser/graphbrowser/Console.java Fri Jul 16 12:55:02 2021 +0200
@@ -0,0 +1,89 @@
+/***************************************************************************
+ Title: graphbrowser/Console.java
+ Author: Gerwin Klein, TU Muenchen
+ Options: :tabSize=2:
+
+ This is the graph browser's main class when run as a console application.
+ It duplicates some logic from GraphBrowser and GraphView.
+ It does so to remove dependency on AWT.
+
+***************************************************************************/
+
+package isabelle.graphbrowser;
+
+import java.io.*;
+import java.util.*;
+
+public class Console {
+ Graph g;
+ String gfname;
+
+ public Console(String name) {
+ gfname = name;
+ }
+
+ public void PS(String fname, boolean printable) throws IOException {
+ g.layout(null);
+ g.PS(fname,printable);
+ }
+
+
+ public void collapseNodes(Vector collapsedDir) {
+ Enumeration e1=collapsedDir.elements();
+ Graph gra=(Graph)(g.clone());
+
+ while (e1.hasMoreElements()) {
+ Directory d=(Directory)(e1.nextElement());
+ Vector v=gra.decode(d.getCollapsed());
+ if (!v.isEmpty())
+ gra.collapse(v,"["+d.getName()+"]",d.getCollapsed());
+ }
+
+ g = gra;
+ }
+
+
+ public void initBrowser(InputStream is) {
+ try {
+ TreeNode tn = new TreeNode("Root", "", -1, true);
+ g = new Graph(is, tn);
+ Vector v = new Vector(10,10);
+ tn.collapsedDirectories(v);
+ collapseNodes(v);
+ } catch (IOException exn) {
+ System.err.println("\nI/O error while reading graph file.");
+ } catch (ParseError exn) {
+ System.err.println("\nParse error in graph file:");
+ System.err.println(exn.getMessage());
+ System.err.println("\nSyntax:\n<vertexname> <vertexID> <dirname> [ + ] <path> "+
+ "[ < | > ] [ <vertexID> [ ... [ <vertexID> ] ... ] ] ;");
+ }
+ }
+
+ public static void main(String[] args) {
+ try {
+ if (args.length <= 1) {
+ System.err.println("Graph and output file expected.");
+ return;
+ }
+
+ Console console=new Console(args[0]);
+ InputStream is=new FileInputStream(args[0]);
+ console.initBrowser(is);
+ is.close();
+
+ try {
+ if (args[1].endsWith(".ps"))
+ console.PS(args[1], true);
+ else if (args[1].endsWith(".eps"))
+ console.PS(args[1], false);
+ else
+ System.err.println("Unknown file type: " + args[1]);
+ } catch (IOException exn) {
+ System.err.println("Unable to write file " + args[1]);
+ }
+ } catch (IOException exn) {
+ System.err.println("Can't open graph file "+args[0]);
+ }
+ }
+}