equal
deleted
inserted
replaced
27 if (length != -1) monitor.setMaximum(length) |
27 if (length != -1) monitor.setMaximum(length) |
28 |
28 |
29 (connection, new BufferedInputStream(stream)) |
29 (connection, new BufferedInputStream(stream)) |
30 } |
30 } |
31 |
31 |
32 // FIXME error handling |
32 // FIXME error handling (dialogs) |
33 def file(parent: Component, url: URL, file: File) |
33 def file(parent: Component, url: URL, file: File): Boolean = |
34 { |
34 { |
35 val outstream = new BufferedOutputStream(new FileOutputStream(file)) |
35 val outstream = new BufferedOutputStream(new FileOutputStream(file)) |
36 |
36 |
37 val (connection, instream) = stream(parent, url) |
37 val (connection, instream) = stream(parent, url) |
38 val mod_time = connection.getLastModified |
38 val mod_time = connection.getLastModified |