src/Pure/System/download.scala
changeset 36676 ac7961d42ac3
parent 34220 f7a0088518e1
child 39703 545cc67324d8
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Pure/System/download.scala	Wed May 05 22:23:45 2010 +0200
     1.3 @@ -0,0 +1,53 @@
     1.4 +/*  Title:      Pure/System/download.scala
     1.5 +    Author:     Makarius
     1.6 +
     1.7 +Download URLs -- with progress monitor.
     1.8 +*/
     1.9 +
    1.10 +package isabelle
    1.11 +
    1.12 +
    1.13 +import java.io.{BufferedInputStream, BufferedOutputStream, FileOutputStream,
    1.14 +  File, InterruptedIOException}
    1.15 +import java.net.{URL, URLConnection}
    1.16 +import java.awt.{Component, HeadlessException}
    1.17 +import javax.swing.ProgressMonitorInputStream
    1.18 +
    1.19 +
    1.20 +object Download
    1.21 +{
    1.22 +  def stream(parent: Component, url: URL): (URLConnection, BufferedInputStream) =
    1.23 +  {
    1.24 +    val connection = url.openConnection
    1.25 +
    1.26 +    val stream = new ProgressMonitorInputStream(null, "Downloading", connection.getInputStream)
    1.27 +    val monitor = stream.getProgressMonitor
    1.28 +    monitor.setNote(connection.getURL.toString)
    1.29 +
    1.30 +    val length = connection.getContentLength
    1.31 +    if (length != -1) monitor.setMaximum(length)
    1.32 +
    1.33 +    (connection, new BufferedInputStream(stream))
    1.34 +  }
    1.35 +
    1.36 +  def file(parent: Component, url: URL, file: File)
    1.37 +  {
    1.38 +    val (connection, instream) = stream(parent, url)
    1.39 +    val mod_time = connection.getLastModified
    1.40 +
    1.41 +    def read() =
    1.42 +      try { instream.read }
    1.43 +      catch { case _ : InterruptedIOException => error("Download canceled!") }
    1.44 +    try {
    1.45 +      val outstream = new BufferedOutputStream(new FileOutputStream(file))
    1.46 +      try {
    1.47 +        var c: Int = 0
    1.48 +        while ({ c = read(); c != -1}) outstream.write(c)
    1.49 +      }
    1.50 +      finally { outstream.close }
    1.51 +      if (mod_time > 0) file.setLastModified(mod_time)
    1.52 +    }
    1.53 +    finally { instream.close }
    1.54 +  }
    1.55 +}
    1.56 +