|
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 |