| author | wenzelm | 
| Wed, 04 Jan 2012 15:41:18 +0100 | |
| changeset 46117 | edd50ec8d471 | 
| parent 45673 | cd41e3903fbf | 
| permissions | -rw-r--r-- | 
| 36676 | 1 | /* Title: Pure/System/download.scala | 
| 45673 
cd41e3903fbf
separate compilation of PIDE vs. Pure sources, which enables independent Scala library;
 wenzelm parents: 
45667diff
changeset | 2 | Module: PIDE | 
| 34218 | 3 | Author: Makarius | 
| 4 | ||
| 5 | Download URLs -- with progress monitor. | |
| 6 | */ | |
| 7 | ||
| 8 | package isabelle | |
| 9 | ||
| 10 | ||
| 34220 | 11 | import java.io.{BufferedInputStream, BufferedOutputStream, FileOutputStream,
 | 
| 12 | File, InterruptedIOException} | |
| 34218 | 13 | import java.net.{URL, URLConnection}
 | 
| 14 | import java.awt.{Component, HeadlessException}
 | |
| 15 | import javax.swing.ProgressMonitorInputStream | |
| 16 | ||
| 17 | ||
| 18 | object Download | |
| 19 | {
 | |
| 39703 | 20 | def stream(parent: Component, title: String, url: URL): (URLConnection, BufferedInputStream) = | 
| 34218 | 21 |   {
 | 
| 22 | val connection = url.openConnection | |
| 23 | ||
| 39703 | 24 | val stream = new ProgressMonitorInputStream(parent, title, connection.getInputStream) | 
| 34218 | 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 | ||
| 39703 | 34 | def file(parent: Component, title: String, url: URL, file: File) | 
| 34218 | 35 |   {
 | 
| 39703 | 36 | val (connection, instream) = stream(parent, title, url) | 
| 34218 | 37 | val mod_time = connection.getLastModified | 
| 38 | ||
| 34220 | 39 | def read() = | 
| 40 |       try { instream.read }
 | |
| 39703 | 41 |       catch { case _ : InterruptedIOException => error("Canceled by user") }
 | 
| 34220 | 42 |     try {
 | 
| 43 | val outstream = new BufferedOutputStream(new FileOutputStream(file)) | |
| 44 |       try {
 | |
| 45 | var c: Int = 0 | |
| 39730 | 46 |         while ({ c = read(); c != -1 }) outstream.write(c)
 | 
| 34220 | 47 | } | 
| 48 |       finally { outstream.close }
 | |
| 49 | if (mod_time > 0) file.setLastModified(mod_time) | |
| 50 | } | |
| 51 |     finally { instream.close }
 | |
| 34218 | 52 | } | 
| 53 | } | |
| 54 |