src/Pure/General/download.scala
author wenzelm
Sat, 02 Jan 2010 01:14:49 +0100
changeset 34219 d37cfca69887
parent 34218 f65c717952c0
child 34220 f7a0088518e1
permissions -rw-r--r--
Standard_System.raw_execute: optional cwd; basic Cygwin.setup with download and unattended installation;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
34218
f65c717952c0 Download URLs -- with progress monitor.
wenzelm
parents:
diff changeset
     1
/*  Title:      Pure/General/download.scala
f65c717952c0 Download URLs -- with progress monitor.
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
f65c717952c0 Download URLs -- with progress monitor.
wenzelm
parents:
diff changeset
     3
f65c717952c0 Download URLs -- with progress monitor.
wenzelm
parents:
diff changeset
     4
Download URLs -- with progress monitor.
f65c717952c0 Download URLs -- with progress monitor.
wenzelm
parents:
diff changeset
     5
*/
f65c717952c0 Download URLs -- with progress monitor.
wenzelm
parents:
diff changeset
     6
f65c717952c0 Download URLs -- with progress monitor.
wenzelm
parents:
diff changeset
     7
package isabelle
f65c717952c0 Download URLs -- with progress monitor.
wenzelm
parents:
diff changeset
     8
f65c717952c0 Download URLs -- with progress monitor.
wenzelm
parents:
diff changeset
     9
f65c717952c0 Download URLs -- with progress monitor.
wenzelm
parents:
diff changeset
    10
import java.io.{BufferedInputStream, BufferedOutputStream, FileOutputStream, File}
f65c717952c0 Download URLs -- with progress monitor.
wenzelm
parents:
diff changeset
    11
import java.net.{URL, URLConnection}
f65c717952c0 Download URLs -- with progress monitor.
wenzelm
parents:
diff changeset
    12
import java.awt.{Component, HeadlessException}
f65c717952c0 Download URLs -- with progress monitor.
wenzelm
parents:
diff changeset
    13
import javax.swing.ProgressMonitorInputStream
f65c717952c0 Download URLs -- with progress monitor.
wenzelm
parents:
diff changeset
    14
f65c717952c0 Download URLs -- with progress monitor.
wenzelm
parents:
diff changeset
    15
f65c717952c0 Download URLs -- with progress monitor.
wenzelm
parents:
diff changeset
    16
object Download
f65c717952c0 Download URLs -- with progress monitor.
wenzelm
parents:
diff changeset
    17
{
f65c717952c0 Download URLs -- with progress monitor.
wenzelm
parents:
diff changeset
    18
  def stream(parent: Component, url: URL): (URLConnection, BufferedInputStream) =
f65c717952c0 Download URLs -- with progress monitor.
wenzelm
parents:
diff changeset
    19
  {
f65c717952c0 Download URLs -- with progress monitor.
wenzelm
parents:
diff changeset
    20
    val connection = url.openConnection
f65c717952c0 Download URLs -- with progress monitor.
wenzelm
parents:
diff changeset
    21
f65c717952c0 Download URLs -- with progress monitor.
wenzelm
parents:
diff changeset
    22
    val stream = new ProgressMonitorInputStream(null, "Downloading", connection.getInputStream)
f65c717952c0 Download URLs -- with progress monitor.
wenzelm
parents:
diff changeset
    23
    val monitor = stream.getProgressMonitor
f65c717952c0 Download URLs -- with progress monitor.
wenzelm
parents:
diff changeset
    24
    monitor.setNote(connection.getURL.toString)
f65c717952c0 Download URLs -- with progress monitor.
wenzelm
parents:
diff changeset
    25
f65c717952c0 Download URLs -- with progress monitor.
wenzelm
parents:
diff changeset
    26
    val length = connection.getContentLength
f65c717952c0 Download URLs -- with progress monitor.
wenzelm
parents:
diff changeset
    27
    if (length != -1) monitor.setMaximum(length)
f65c717952c0 Download URLs -- with progress monitor.
wenzelm
parents:
diff changeset
    28
f65c717952c0 Download URLs -- with progress monitor.
wenzelm
parents:
diff changeset
    29
    (connection, new BufferedInputStream(stream))
f65c717952c0 Download URLs -- with progress monitor.
wenzelm
parents:
diff changeset
    30
  }
f65c717952c0 Download URLs -- with progress monitor.
wenzelm
parents:
diff changeset
    31
34219
d37cfca69887 Standard_System.raw_execute: optional cwd;
wenzelm
parents: 34218
diff changeset
    32
  // FIXME error handling (dialogs)
d37cfca69887 Standard_System.raw_execute: optional cwd;
wenzelm
parents: 34218
diff changeset
    33
  def file(parent: Component, url: URL, file: File): Boolean =
34218
f65c717952c0 Download URLs -- with progress monitor.
wenzelm
parents:
diff changeset
    34
  {
f65c717952c0 Download URLs -- with progress monitor.
wenzelm
parents:
diff changeset
    35
    val outstream = new BufferedOutputStream(new FileOutputStream(file))
f65c717952c0 Download URLs -- with progress monitor.
wenzelm
parents:
diff changeset
    36
f65c717952c0 Download URLs -- with progress monitor.
wenzelm
parents:
diff changeset
    37
    val (connection, instream) = stream(parent, url)
f65c717952c0 Download URLs -- with progress monitor.
wenzelm
parents:
diff changeset
    38
    val mod_time = connection.getLastModified
f65c717952c0 Download URLs -- with progress monitor.
wenzelm
parents:
diff changeset
    39
f65c717952c0 Download URLs -- with progress monitor.
wenzelm
parents:
diff changeset
    40
    var c: Int = 0
f65c717952c0 Download URLs -- with progress monitor.
wenzelm
parents:
diff changeset
    41
    while ({ c = instream.read; c != -1}) outstream.write(c)
f65c717952c0 Download URLs -- with progress monitor.
wenzelm
parents:
diff changeset
    42
f65c717952c0 Download URLs -- with progress monitor.
wenzelm
parents:
diff changeset
    43
    instream.close
f65c717952c0 Download URLs -- with progress monitor.
wenzelm
parents:
diff changeset
    44
    outstream.close
f65c717952c0 Download URLs -- with progress monitor.
wenzelm
parents:
diff changeset
    45
    file.setLastModified(mod_time)
f65c717952c0 Download URLs -- with progress monitor.
wenzelm
parents:
diff changeset
    46
  }
f65c717952c0 Download URLs -- with progress monitor.
wenzelm
parents:
diff changeset
    47
}
f65c717952c0 Download URLs -- with progress monitor.
wenzelm
parents:
diff changeset
    48