--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Concurrent/future.scala Sat Jan 02 20:10:21 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]]
+ }
+ }
+}
+
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/General/download.scala Sat Jan 02 20:10:21 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 }
+ }
+}
+
--- a/src/Pure/General/swing_thread.scala Fri Jan 01 19:15:43 2010 +0100
+++ b/src/Pure/General/swing_thread.scala Sat Jan 02 20:10:21 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
--- a/src/Pure/IsaMakefile Fri Jan 01 19:15:43 2010 +0100
+++ b/src/Pure/IsaMakefile Sat Jan 02 20:10:21 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 \
--- a/src/Pure/System/cygwin.scala Fri Jan 01 19:15:43 2010 +0100
+++ b/src/Pure/System/cygwin.scala Sat Jan 02 20:10:21 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)
}
}
--- a/src/Pure/System/isabelle_system.scala Fri Jan 01 19:15:43 2010 +0100
+++ b/src/Pure/System/isabelle_system.scala Sat Jan 02 20:10:21 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: _*)
}
--- a/src/Pure/System/standard_system.scala Fri Jan 01 19:15:43 2010 +0100
+++ b/src/Pure/System/standard_system.scala Sat Jan 02 20:10:21 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)