src/Pure/System/download.scala
author wenzelm
Wed Jun 02 11:09:26 2010 +0200 (2010-06-02 ago)
changeset 37251 72c7e636067b
parent 36676 ac7961d42ac3
child 39703 545cc67324d8
permissions -rw-r--r--
normalize and postprocess proof body in a separate future, taking care of platforms without multithreading (greately improves parallelization in general without the overhead of promised proofs, cf. usedir -q 0);
     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