src/Pure/System/download.scala
author wenzelm
Wed May 05 22:23:45 2010 +0200 (2010-05-05 ago)
changeset 36676 ac7961d42ac3
parent 34220 src/Pure/General/download.scala@f7a0088518e1
child 39703 545cc67324d8
permissions -rw-r--r--
some rearrangement of Scala sources;
     1 /*  Title:      Pure/System/download.scala
     2     Author:     Makarius
     3 
     4 Download URLs -- with progress monitor.
     5 */
     6 
     7 package isabelle
     8 
     9 
    10 import java.io.{BufferedInputStream, BufferedOutputStream, FileOutputStream,
    11   File, InterruptedIOException}
    12 import java.net.{URL, URLConnection}
    13 import java.awt.{Component, HeadlessException}
    14 import javax.swing.ProgressMonitorInputStream
    15 
    16 
    17 object Download
    18 {
    19   def stream(parent: Component, url: URL): (URLConnection, BufferedInputStream) =
    20   {
    21     val connection = url.openConnection
    22 
    23     val stream = new ProgressMonitorInputStream(null, "Downloading", connection.getInputStream)
    24     val monitor = stream.getProgressMonitor
    25     monitor.setNote(connection.getURL.toString)
    26 
    27     val length = connection.getContentLength
    28     if (length != -1) monitor.setMaximum(length)
    29 
    30     (connection, new BufferedInputStream(stream))
    31   }
    32 
    33   def file(parent: Component, url: URL, file: File)
    34   {
    35     val (connection, instream) = stream(parent, url)
    36     val mod_time = connection.getLastModified
    37 
    38     def read() =
    39       try { instream.read }
    40       catch { case _ : InterruptedIOException => error("Download canceled!") }
    41     try {
    42       val outstream = new BufferedOutputStream(new FileOutputStream(file))
    43       try {
    44         var c: Int = 0
    45         while ({ c = read(); c != -1}) outstream.write(c)
    46       }
    47       finally { outstream.close }
    48       if (mod_time > 0) file.setLastModified(mod_time)
    49     }
    50     finally { instream.close }
    51   }
    52 }
    53