equal
deleted
inserted
replaced
54 try { |
54 try { |
55 if (isApplet) |
55 if (isApplet) |
56 getAppletContext().showDocument(new URL(getDocumentBase(), fname), "_blank"); |
56 getAppletContext().showDocument(new URL(getDocumentBase(), fname), "_blank"); |
57 else { |
57 else { |
58 String path = gfname.substring(0, gfname.lastIndexOf('/') + 1); |
58 String path = gfname.substring(0, gfname.lastIndexOf('/') + 1); |
|
59 Reader rd; |
59 BufferedReader br; |
60 BufferedReader br; |
60 String line, text = ""; |
61 String line, text = ""; |
61 |
62 |
62 br = new BufferedReader(new FileReader(path + fname)); |
63 try { |
|
64 rd = new BufferedReader(new InputStreamReader((new URL(fname)).openConnection().getInputStream())); |
|
65 } catch (Exception exn) { |
|
66 rd = new FileReader(path + fname); |
|
67 } |
|
68 br = new BufferedReader(rd); |
|
69 |
63 while ((line = br.readLine()) != null) |
70 while ((line = br.readLine()) != null) |
64 text += line + "\n"; |
71 text += line + "\n"; |
65 |
72 |
66 if (fname.endsWith(".html")) { |
73 if (fname.endsWith(".html")) { |
67 /**** convert HTML to text (just a quick hack) ****/ |
74 /**** convert HTML to text (just a quick hack) ****/ |