lib/browser/GraphBrowser/GraphBrowser.java
changeset 11876 6ac0627167ed
parent 11812 8d191eaf7fc4
child 12411 8a8ea71c79d3
equal deleted inserted replaced
11875:5fcf6b6436af 11876:6ac0627167ed
   125 
   125 
   126 	public boolean isEmpty() {
   126 	public boolean isEmpty() {
   127 		return tb==null;
   127 		return tb==null;
   128 	}
   128 	}
   129 
   129 
   130 	public void initBrowser(InputStream is) {
   130 	public void initBrowser(InputStream is, boolean noAWT) {
   131 		try {
   131 		try {
   132 			TreeNode tn=new TreeNode("Root","",-1,true);
   132 			Font font = noAWT ? null : new Font("Helvetica", Font.PLAIN, 12);
   133 			gv=new GraphView(new Graph(is,tn),this);
   133 			TreeNode tn = new TreeNode("Root", "", -1, true);
   134 			tb=new TreeBrowser(tn,gv);
   134 			gv = new GraphView(new Graph(is, tn), this, font);
       
   135 			tb = new TreeBrowser(tn, gv, font);
   135 			gv.setTreeBrowser(tb);
   136 			gv.setTreeBrowser(tb);
   136 			Vector v = new Vector(10,10);
   137 			Vector v = new Vector(10,10);
   137 			tn.collapsedDirectories(v);
   138 			tn.collapsedDirectories(v);
   138 			gv.collapseDir(v);
   139 			gv.collapseDir(v);
   139 
   140 
   173 	public void init() {
   174 	public void init() {
   174 		isApplet=true;
   175 		isApplet=true;
   175 		gfname=getParameter("graphfile");
   176 		gfname=getParameter("graphfile");
   176 		try {
   177 		try {
   177 			InputStream is=(new URL(getDocumentBase(), gfname)).openConnection().getInputStream();
   178 			InputStream is=(new URL(getDocumentBase(), gfname)).openConnection().getInputStream();
   178 			initBrowser(is);
   179 			initBrowser(is, false);
   179 			is.close();
   180 			is.close();
   180 		} catch (MalformedURLException exn) {
   181 		} catch (MalformedURLException exn) {
   181 			System.err.println("Invalid URL: "+gfname);
   182 			System.err.println("Invalid URL: "+gfname);
   182 		} catch (IOException exn) {
   183 		} catch (IOException exn) {
   183 			System.err.println("I/O error while reading "+gfname+".");
   184 			System.err.println("I/O error while reading "+gfname+".");
   188 		isApplet=false;
   189 		isApplet=false;
   189 		try {
   190 		try {
   190 			GraphBrowser gb=new GraphBrowser(args.length > 0 ? args[0] : "");
   191 			GraphBrowser gb=new GraphBrowser(args.length > 0 ? args[0] : "");
   191 			if (args.length > 0) {
   192 			if (args.length > 0) {
   192 				InputStream is=new FileInputStream(args[0]);
   193 				InputStream is=new FileInputStream(args[0]);
   193 				gb.initBrowser(is);
   194 				gb.initBrowser(is, args.length > 1);
   194 				is.close();
   195 				is.close();
   195 			}
   196 			}
   196 			if (args.length > 1) {
   197 			if (args.length > 1) {
   197                             try {
   198                             try {
   198 			      if (args[1].endsWith(".ps")) {
   199 			      if (args[1].endsWith(".ps"))
   199                                 gb.gv.PS(args[1], true);
   200                                 gb.gv.PS(args[1], true);
   200                               } else if (args[1].endsWith(".eps")) {
   201                               else if (args[1].endsWith(".eps"))
   201                                 gb.gv.PS(args[1], false);
   202                                 gb.gv.PS(args[1], false);
   202                               } else {
   203                               else
   203                                 System.err.println("Unknown file type: " + args[1]);
   204                                 System.err.println("Unknown file type: " + args[1]);
   204                               }
       
   205                             } catch (IOException exn) {
   205                             } catch (IOException exn) {
   206                               System.err.println("Unable to write file " + args[1]);
   206                               System.err.println("Unable to write file " + args[1]);
   207                             }
   207                             }
   208 			    System.exit(0);
       
   209                         } else {
   208                         } else {
   210 			    f=new GraphBrowserFrame(gb);
   209 			    f=new GraphBrowserFrame(gb);
   211 			    f.setSize(700,500);
   210 			    f.setSize(700,500);
   212 			    f.show();
   211 			    f.show();
   213                         }
   212                         }