lib/browser/GraphBrowser/Console.java
changeset 13968 689868b99bde
child 13970 4aef7117817b
equal deleted inserted replaced
13967:9cdab3186c0b 13968:689868b99bde
       
     1 /***************************************************************************
       
     2   Title:      GraphBrowser/Console.java
       
     3   ID:         $Id$
       
     4   Author:     Stefan Berghofer, TU Muenchen
       
     5   License:    GPL (GNU GENERAL PUBLIC LICENSE)
       
     6 
       
     7   This is the graph browser's main class when run as a console application.
       
     8 
       
     9 ***************************************************************************/
       
    10 
       
    11 package GraphBrowser;
       
    12 
       
    13 import java.io.*;
       
    14 import java.util.*;
       
    15 import java.net.*;
       
    16 import awtUtilities.*;
       
    17 
       
    18 public class Console {
       
    19 	Graph g;
       
    20 	// TreeBrowser tb;
       
    21 	String gfname;
       
    22 
       
    23   public Console(String name) {
       
    24     gfname = name;
       
    25   }
       
    26 
       
    27 	public void PS(String fname,boolean printable) throws IOException {
       
    28     g.layout(null);
       
    29 		g.PS(fname,printable);
       
    30 	}
       
    31 
       
    32 	public void initBrowser(InputStream is) {
       
    33 		try {
       
    34 			TreeNode tn = new TreeNode("Root", "", -1, true);
       
    35       g = new Graph(is, tn);
       
    36       
       
    37 			// gv = new GraphView(new Graph(is, tn), null, null);
       
    38       // tb = new TreeBrowser(tn, gv, font);
       
    39 			// gv.setTreeBrowser(tb);
       
    40 			// Vector v = new Vector(10,10);
       
    41 			// tn.collapsedDirectories(v);
       
    42 			// gv.collapseDir(v);
       
    43 		} catch (IOException exn) {
       
    44 			System.err.println("\nI/O error while reading graph file.");
       
    45 		} catch (ParseError exn) {
       
    46 			System.err.println("\nParse error in graph file:");
       
    47 			System.err.println(exn.getMessage());
       
    48 			System.err.println("\nSyntax:\n<vertexname> <vertexID> <dirname> [ + ] <path> [ < | > ] [ <vertexID> [ ... [ <vertexID> ] ... ] ] ;");
       
    49 		}
       
    50 	}
       
    51 
       
    52 	public static void main(String[] args) {
       
    53 		try {
       
    54       if (args.length <= 1) {
       
    55         System.err.println("Graph and output file expected");
       
    56         return;
       
    57       }
       
    58 			Console console=new Console(args[0]);
       
    59 
       
    60       InputStream is=new FileInputStream(args[0]);
       
    61       console.initBrowser(is);
       
    62       is.close();      
       
    63     
       
    64       try {
       
    65         if (args[1].endsWith(".ps"))
       
    66           console.PS(args[1], true);
       
    67         else if (args[1].endsWith(".eps"))
       
    68           console.PS(args[1], false);
       
    69         else
       
    70           System.err.println("Unknown file type: " + args[1]);
       
    71       } catch (IOException exn) {
       
    72         System.err.println("Unable to write file " + args[1]);
       
    73       }
       
    74 		} catch (IOException exn) {
       
    75 			System.err.println("Can't open graph file "+args[0]);
       
    76 		}
       
    77 	}
       
    78 }
       
    79