# HG changeset patch
# User nipkow
# Date 1262464293 -3600
# Node ID aec597ef135c501eec3d563bbcfa9ddfaa044dd0
# Parent  143e3dabec2b55147ec38b57ab008068dd9e0d38# Parent  21c5405deb6b49a0281a4afff3fcc7a736392167
merged

diff -r 21c5405deb6b -r aec597ef135c src/Pure/Concurrent/future.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Concurrent/future.scala	Sat Jan 02 21:31:33 2010 +0100
@@ -0,0 +1,67 @@
+/*  Title:      Pure/Concurrent/future.scala
+    Author:     Makarius
+
+Future values.
+
+Notable differences to scala.actors.Future (as of Scala 2.7.7):
+
+  * We capture/release exceptions as in the ML variant.
+
+  * Future.join works for *any* actor, not just the one of the
+    original fork.
+*/
+
+package isabelle
+
+
+import scala.actors.Actor._
+
+
+object Future
+{
+  def value[A](x: A): Future[A] = new Finished_Future(x)
+  def fork[A](body: => A): Future[A] = new Pending_Future(body)
+}
+
+abstract class Future[A]
+{
+  def peek: Option[Exn.Result[A]]
+  def is_finished: Boolean = peek.isDefined
+  def join: A
+  def map[B](f: A => B): Future[B] = Future.fork { f(join) }
+
+  override def toString =
+    peek match {
+      case None => "<future>"
+      case Some(Exn.Exn(_)) => "<failed>"
+      case Some(Exn.Res(x)) => x.toString
+    }
+}
+
+private class Finished_Future[A](x: A) extends Future[A]
+{
+  val peek: Option[Exn.Result[A]] = Some(Exn.Res(x))
+  val join: A = x
+}
+
+private class Pending_Future[A](body: => A) extends Future[A]
+{
+  @volatile private var result: Option[Exn.Result[A]] = None
+
+  private val evaluator = actor {
+    result = Some(Exn.capture(body))
+    loop { react { case _ => reply(result.get) } }
+  }
+
+  def peek: Option[Exn.Result[A]] = result
+
+  def join: A =
+    Exn.release {
+      peek match {
+        case Some(res) => res
+        case None => (evaluator !? ()).asInstanceOf[Exn.Result[A]]
+      }
+    }
+}
+
+
diff -r 21c5405deb6b -r aec597ef135c src/Pure/General/download.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/General/download.scala	Sat Jan 02 21:31:33 2010 +0100
@@ -0,0 +1,53 @@
+/*  Title:      Pure/General/download.scala
+    Author:     Makarius
+
+Download URLs -- with progress monitor.
+*/
+
+package isabelle
+
+
+import java.io.{BufferedInputStream, BufferedOutputStream, FileOutputStream,
+  File, InterruptedIOException}
+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))
+  }
+
+  def file(parent: Component, url: URL, file: File)
+  {
+    val (connection, instream) = stream(parent, url)
+    val mod_time = connection.getLastModified
+
+    def read() =
+      try { instream.read }
+      catch { case _ : InterruptedIOException => error("Download canceled!") }
+    try {
+      val outstream = new BufferedOutputStream(new FileOutputStream(file))
+      try {
+        var c: Int = 0
+        while ({ c = read(); c != -1}) outstream.write(c)
+      }
+      finally { outstream.close }
+      if (mod_time > 0) file.setLastModified(mod_time)
+    }
+    finally { instream.close }
+  }
+}
+
diff -r 21c5405deb6b -r aec597ef135c src/Pure/General/swing_thread.scala
--- a/src/Pure/General/swing_thread.scala	Sat Jan 02 21:31:15 2010 +0100
+++ b/src/Pure/General/swing_thread.scala	Sat Jan 02 21:31:33 2010 +0100
@@ -10,8 +10,6 @@
 import javax.swing.{SwingUtilities, Timer}
 import java.awt.event.{ActionListener, ActionEvent}
 
-import scala.actors.{Future, Futures}
-
 
 object Swing_Thread
 {
@@ -31,8 +29,7 @@
     result.get
   }
 
-  def future[A](body: => A): Future[A] =
-    Futures.future(now(body))
+  def future[A](body: => A): Future[A] = Future.fork { now(body) }
 
   def later(body: => Unit) {
     if (SwingUtilities.isEventDispatchThread()) body
diff -r 21c5405deb6b -r aec597ef135c src/Pure/IsaMakefile
--- a/src/Pure/IsaMakefile	Sat Jan 02 21:31:15 2010 +0100
+++ b/src/Pure/IsaMakefile	Sat Jan 02 21:31:33 2010 +0100
@@ -121,12 +121,13 @@
 
 ## Scala material
 
-SCALA_FILES = 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	\
+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		\
   System/isabelle_system.scala System/platform.scala			\
   System/session_manager.scala System/standard_system.scala		\
diff -r 21c5405deb6b -r aec597ef135c src/Pure/System/cygwin.scala
--- a/src/Pure/System/cygwin.scala	Sat Jan 02 21:31:15 2010 +0100
+++ b/src/Pure/System/cygwin.scala	Sat Jan 02 21:31:33 2010 +0100
@@ -8,6 +8,8 @@
 
 import java.lang.reflect.Method
 import java.io.File
+import java.net.URL
+import java.awt.Component
 
 
 object Cygwin
@@ -79,6 +81,14 @@
   private val CYGWIN_SETUP1 = "Software\\Cygwin\\setup"
   private val CYGWIN_SETUP2 = "Software\\Wow6432Node\\Cygwin\\setup"
 
+  private def sanity_check(root: File)
+  {
+    if (!new File(root, "bin\\bash.exe").isFile ||
+        !new File(root, "bin\\env.exe").isFile ||
+        !new File(root, "bin\\tar.exe").isFile)
+      error("Bad Cygwin installation: " + root.toString)
+  }
+
   def check_root(): String =
   {
     val root_env = java.lang.System.getenv("CYGWIN_ROOT")
@@ -88,20 +98,29 @@
         query_registry(CYGWIN_SETUP1, "rootdir") orElse
         query_registry(CYGWIN_SETUP2, "rootdir") getOrElse
         error("Failed to determine Cygwin installation -- version 1.7 required")
-    val ok =
-      new File(root + "\\bin\\bash.exe").isFile &&
-      new File(root + "\\bin\\env.exe").isFile
-    if (!ok) error("Bad Cygwin installation: " + root)
+    sanity_check(new File(root))
     root
   }
 
-  def setup(exe: String, root: String): Int =
+  def setup(parent: Component, root: File)
   {
-    val (output, rc) = Standard_System.process_output(
-    	Standard_System.raw_execute(null, true, exe, "-R", root, "-P", "perl,python", "-q", "-n"))
-    val root_dir = new File(root)
-    if (root_dir.isDirectory) Standard_System.write_file(new File(root, "setup.log"), output)
-    rc
+    if (!root.mkdirs) error("Failed to create root directory: " + root)
+
+    val download = new File(root, "download")
+    if (!download.mkdir) error("Failed to create download directory: " + download)
+
+    val setup_exe = new File(root, "setup.exe")
+
+    try { Download.file(parent, new URL("http://www.cygwin.com/setup.exe"), setup_exe) }
+    catch { case _: RuntimeException => error("Failed to download Cygwin setup program") }
+
+    val (_, rc) = Standard_System.process_output(
+    	Standard_System.raw_execute(root, null, true,
+    	  setup_exe.toString, "-R", root.toString, "-l", download.toString,
+    	    "-P", "perl,python", "-q", "-n"))
+    if (rc != 0) error("Cygwin setup failed!")
+
+    sanity_check(root)
   }
 }
 
diff -r 21c5405deb6b -r aec597ef135c src/Pure/System/isabelle_system.scala
--- a/src/Pure/System/isabelle_system.scala	Sat Jan 02 21:31:15 2010 +0100
+++ b/src/Pure/System/isabelle_system.scala	Sat Jan 02 21:31:33 2010 +0100
@@ -43,7 +43,7 @@
         val cmdline =
           shell_prefix ::: List(isabelle_home + "/bin/isabelle", "getenv", "-d", dump.toString)
         val (output, rc) =
-          Standard_System.process_output(Standard_System.raw_execute(env0, true, cmdline: _*))
+          Standard_System.process_output(Standard_System.raw_execute(null, env0, true, cmdline: _*))
         if (rc != 0) error(output)
 
         val entries =
@@ -66,7 +66,7 @@
     val cmdline =
       if (Platform.is_windows) List(platform_root + "\\bin\\env.exe") ++ args
       else args
-    Standard_System.raw_execute(environment, redirect, cmdline: _*)
+    Standard_System.raw_execute(null, environment, redirect, cmdline: _*)
   }
 
 
diff -r 21c5405deb6b -r aec597ef135c src/Pure/System/standard_system.scala
--- a/src/Pure/System/standard_system.scala	Sat Jan 02 21:31:15 2010 +0100
+++ b/src/Pure/System/standard_system.scala	Sat Jan 02 21:31:33 2010 +0100
@@ -101,12 +101,13 @@
 
   /* shell processes */
 
-  def raw_execute(env: Map[String, String], redirect: Boolean, args: String*): Process =
+  def raw_execute(cwd: File, env: Map[String, String], redirect: Boolean, args: String*): Process =
   {
     val cmdline = new java.util.LinkedList[String]
     for (s <- args) cmdline.add(s)
 
     val proc = new ProcessBuilder(cmdline)
+    if (cwd != null) proc.directory(cwd)
     if (env != null) {
       proc.environment.clear
       for ((x, y) <- env) proc.environment.put(x, y)