# HG changeset patch
# User wenzelm
# Date 1262387327 -3600
# Node ID f65c717952c0d7ead81f5bb34c18fbc434a91202
# Parent  67e1ac2d3b2c38212ddc76b4d84f928b620d1a14
Download URLs -- with progress monitor.

diff -r 67e1ac2d3b2c -r f65c717952c0 src/Pure/General/download.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/General/download.scala	Sat Jan 02 00:08:47 2010 +0100
@@ -0,0 +1,48 @@
+/*  Title:      Pure/General/download.scala
+    Author:     Makarius
+
+Download URLs -- with progress monitor.
+*/
+
+package isabelle
+
+
+import java.io.{BufferedInputStream, BufferedOutputStream, FileOutputStream, File}
+import java.net.{URL, URLConnection}
+import java.awt.{Component, HeadlessException}
+import javax.swing.ProgressMonitorInputStream
+
+
+object Download
+{
+  def stream(parent: Component, url: URL): (URLConnection, BufferedInputStream) =
+  {
+    val connection = url.openConnection
+
+    val stream = new ProgressMonitorInputStream(null, "Downloading", connection.getInputStream)
+    val monitor = stream.getProgressMonitor
+    monitor.setNote(connection.getURL.toString)
+
+    val length = connection.getContentLength
+    if (length != -1) monitor.setMaximum(length)
+
+    (connection, new BufferedInputStream(stream))
+  }
+
+  // FIXME error handling
+  def file(parent: Component, url: URL, file: File)
+  {
+    val outstream = new BufferedOutputStream(new FileOutputStream(file))
+
+    val (connection, instream) = stream(parent, url)
+    val mod_time = connection.getLastModified
+
+    var c: Int = 0
+    while ({ c = instream.read; c != -1}) outstream.write(c)
+
+    instream.close
+    outstream.close
+    file.setLastModified(mod_time)
+  }
+}
+
diff -r 67e1ac2d3b2c -r f65c717952c0 src/Pure/IsaMakefile
--- a/src/Pure/IsaMakefile	Fri Jan 01 21:26:02 2010 +0100
+++ b/src/Pure/IsaMakefile	Sat Jan 02 00:08:47 2010 +0100
@@ -121,11 +121,11 @@
 
 ## Scala material
 
-SCALA_FILES = Concurrent/future.scala General/event_bus.scala		\
-  General/exn.scala General/linear_set.scala General/markup.scala	\
-  General/position.scala General/scan.scala General/swing_thread.scala	\
-  General/symbol.scala General/xml.scala General/yxml.scala		\
-  Isar/isar_document.scala Isar/outer_keyword.scala			\
+SCALA_FILES = Concurrent/future.scala General/download.scala		\
+  General/event_bus.scala General/exn.scala General/linear_set.scala	\
+  General/markup.scala General/position.scala General/scan.scala	\
+  General/swing_thread.scala General/symbol.scala General/xml.scala	\
+  General/yxml.scala Isar/isar_document.scala Isar/outer_keyword.scala	\
   Isar/outer_lex.scala Isar/outer_parse.scala Isar/outer_syntax.scala	\
   System/cygwin.scala System/gui_setup.scala				\
   System/isabelle_process.scala System/isabelle_syntax.scala		\