1 /* Title: Pure/System/download.scala |
|
2 Module: PIDE |
|
3 Author: Makarius |
|
4 |
|
5 Download URLs -- with progress monitor. |
|
6 */ |
|
7 |
|
8 package isabelle |
|
9 |
|
10 |
|
11 import java.io.{BufferedInputStream, BufferedOutputStream, FileOutputStream, |
|
12 File, InterruptedIOException} |
|
13 import java.net.{URL, URLConnection} |
|
14 import java.awt.{Component, HeadlessException} |
|
15 import javax.swing.ProgressMonitorInputStream |
|
16 |
|
17 |
|
18 object Download |
|
19 { |
|
20 def stream(parent: Component, title: String, url: URL): (URLConnection, BufferedInputStream) = |
|
21 { |
|
22 val connection = url.openConnection |
|
23 |
|
24 val stream = new ProgressMonitorInputStream(parent, title, connection.getInputStream) |
|
25 val monitor = stream.getProgressMonitor |
|
26 monitor.setNote(connection.getURL.toString) |
|
27 |
|
28 val length = connection.getContentLength |
|
29 if (length != -1) monitor.setMaximum(length) |
|
30 |
|
31 (connection, new BufferedInputStream(stream)) |
|
32 } |
|
33 |
|
34 def file(parent: Component, title: String, url: URL, file: File) |
|
35 { |
|
36 val (connection, instream) = stream(parent, title, url) |
|
37 val mod_time = connection.getLastModified |
|
38 |
|
39 def read() = |
|
40 try { instream.read } |
|
41 catch { case _ : InterruptedIOException => error("Canceled by user") } |
|
42 try { |
|
43 val outstream = new BufferedOutputStream(new FileOutputStream(file)) |
|
44 try { |
|
45 var c: Int = 0 |
|
46 while ({ c = read(); c != -1 }) outstream.write(c) |
|
47 } |
|
48 finally { outstream.close } |
|
49 if (mod_time > 0) file.setLastModified(mod_time) |
|
50 } |
|
51 finally { instream.close } |
|
52 } |
|
53 } |
|
54 |
|