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