src/Tools/GraphBrowser/graphbrowser/Console.java

+/***************************************************************************
+  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]);
+		}
+	}
+}