src/Tools/GraphBrowser/graphbrowser/Console.java

clarified names;

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