merged
authorwenzelm
Sat Jan 02 20:10:21 2010 +0100 (2010-01-02)
changeset 34224143e3dabec2b
parent 34223 dce32a1e05fe
parent 34220 f7a0088518e1
child 34226 aec597ef135c
merged
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Pure/Concurrent/future.scala	Sat Jan 02 20:10:21 2010 +0100
     1.3 @@ -0,0 +1,67 @@
     1.4 +/*  Title:      Pure/Concurrent/future.scala
     1.5 +    Author:     Makarius
     1.6 +
     1.7 +Future values.
     1.8 +
     1.9 +Notable differences to scala.actors.Future (as of Scala 2.7.7):
    1.10 +
    1.11 +  * We capture/release exceptions as in the ML variant.
    1.12 +
    1.13 +  * Future.join works for *any* actor, not just the one of the
    1.14 +    original fork.
    1.15 +*/
    1.16 +
    1.17 +package isabelle
    1.18 +
    1.19 +
    1.20 +import scala.actors.Actor._
    1.21 +
    1.22 +
    1.23 +object Future
    1.24 +{
    1.25 +  def value[A](x: A): Future[A] = new Finished_Future(x)
    1.26 +  def fork[A](body: => A): Future[A] = new Pending_Future(body)
    1.27 +}
    1.28 +
    1.29 +abstract class Future[A]
    1.30 +{
    1.31 +  def peek: Option[Exn.Result[A]]
    1.32 +  def is_finished: Boolean = peek.isDefined
    1.33 +  def join: A
    1.34 +  def map[B](f: A => B): Future[B] = Future.fork { f(join) }
    1.35 +
    1.36 +  override def toString =
    1.37 +    peek match {
    1.38 +      case None => "<future>"
    1.39 +      case Some(Exn.Exn(_)) => "<failed>"
    1.40 +      case Some(Exn.Res(x)) => x.toString
    1.41 +    }
    1.42 +}
    1.43 +
    1.44 +private class Finished_Future[A](x: A) extends Future[A]
    1.45 +{
    1.46 +  val peek: Option[Exn.Result[A]] = Some(Exn.Res(x))
    1.47 +  val join: A = x
    1.48 +}
    1.49 +
    1.50 +private class Pending_Future[A](body: => A) extends Future[A]
    1.51 +{
    1.52 +  @volatile private var result: Option[Exn.Result[A]] = None
    1.53 +
    1.54 +  private val evaluator = actor {
    1.55 +    result = Some(Exn.capture(body))
    1.56 +    loop { react { case _ => reply(result.get) } }
    1.57 +  }
    1.58 +
    1.59 +  def peek: Option[Exn.Result[A]] = result
    1.60 +
    1.61 +  def join: A =
    1.62 +    Exn.release {
    1.63 +      peek match {
    1.64 +        case Some(res) => res
    1.65 +        case None => (evaluator !? ()).asInstanceOf[Exn.Result[A]]
    1.66 +      }
    1.67 +    }
    1.68 +}
    1.69 +
    1.70 +
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/Pure/General/download.scala	Sat Jan 02 20:10:21 2010 +0100
     2.3 @@ -0,0 +1,53 @@
     2.4 +/*  Title:      Pure/General/download.scala
     2.5 +    Author:     Makarius
     2.6 +
     2.7 +Download URLs -- with progress monitor.
     2.8 +*/
     2.9 +
    2.10 +package isabelle
    2.11 +
    2.12 +
    2.13 +import java.io.{BufferedInputStream, BufferedOutputStream, FileOutputStream,
    2.14 +  File, InterruptedIOException}
    2.15 +import java.net.{URL, URLConnection}
    2.16 +import java.awt.{Component, HeadlessException}
    2.17 +import javax.swing.ProgressMonitorInputStream
    2.18 +
    2.19 +
    2.20 +object Download
    2.21 +{
    2.22 +  def stream(parent: Component, url: URL): (URLConnection, BufferedInputStream) =
    2.23 +  {
    2.24 +    val connection = url.openConnection
    2.25 +
    2.26 +    val stream = new ProgressMonitorInputStream(null, "Downloading", connection.getInputStream)
    2.27 +    val monitor = stream.getProgressMonitor
    2.28 +    monitor.setNote(connection.getURL.toString)
    2.29 +
    2.30 +    val length = connection.getContentLength
    2.31 +    if (length != -1) monitor.setMaximum(length)
    2.32 +
    2.33 +    (connection, new BufferedInputStream(stream))
    2.34 +  }
    2.35 +
    2.36 +  def file(parent: Component, url: URL, file: File)
    2.37 +  {
    2.38 +    val (connection, instream) = stream(parent, url)
    2.39 +    val mod_time = connection.getLastModified
    2.40 +
    2.41 +    def read() =
    2.42 +      try { instream.read }
    2.43 +      catch { case _ : InterruptedIOException => error("Download canceled!") }
    2.44 +    try {
    2.45 +      val outstream = new BufferedOutputStream(new FileOutputStream(file))
    2.46 +      try {
    2.47 +        var c: Int = 0
    2.48 +        while ({ c = read(); c != -1}) outstream.write(c)
    2.49 +      }
    2.50 +      finally { outstream.close }
    2.51 +      if (mod_time > 0) file.setLastModified(mod_time)
    2.52 +    }
    2.53 +    finally { instream.close }
    2.54 +  }
    2.55 +}
    2.56 +
     3.1 --- a/src/Pure/General/swing_thread.scala	Fri Jan 01 19:15:43 2010 +0100
     3.2 +++ b/src/Pure/General/swing_thread.scala	Sat Jan 02 20:10:21 2010 +0100
     3.3 @@ -10,8 +10,6 @@
     3.4  import javax.swing.{SwingUtilities, Timer}
     3.5  import java.awt.event.{ActionListener, ActionEvent}
     3.6  
     3.7 -import scala.actors.{Future, Futures}
     3.8 -
     3.9  
    3.10  object Swing_Thread
    3.11  {
    3.12 @@ -31,8 +29,7 @@
    3.13      result.get
    3.14    }
    3.15  
    3.16 -  def future[A](body: => A): Future[A] =
    3.17 -    Futures.future(now(body))
    3.18 +  def future[A](body: => A): Future[A] = Future.fork { now(body) }
    3.19  
    3.20    def later(body: => Unit) {
    3.21      if (SwingUtilities.isEventDispatchThread()) body
     4.1 --- a/src/Pure/IsaMakefile	Fri Jan 01 19:15:43 2010 +0100
     4.2 +++ b/src/Pure/IsaMakefile	Sat Jan 02 20:10:21 2010 +0100
     4.3 @@ -121,12 +121,13 @@
     4.4  
     4.5  ## Scala material
     4.6  
     4.7 -SCALA_FILES = General/event_bus.scala General/exn.scala			\
     4.8 -  General/linear_set.scala General/markup.scala General/position.scala	\
     4.9 -  General/scan.scala General/swing_thread.scala General/symbol.scala	\
    4.10 -  General/xml.scala General/yxml.scala Isar/isar_document.scala		\
    4.11 -  Isar/outer_keyword.scala Isar/outer_lex.scala Isar/outer_parse.scala	\
    4.12 -  Isar/outer_syntax.scala System/cygwin.scala System/gui_setup.scala	\
    4.13 +SCALA_FILES = Concurrent/future.scala General/download.scala		\
    4.14 +  General/event_bus.scala General/exn.scala General/linear_set.scala	\
    4.15 +  General/markup.scala General/position.scala General/scan.scala	\
    4.16 +  General/swing_thread.scala General/symbol.scala General/xml.scala	\
    4.17 +  General/yxml.scala Isar/isar_document.scala Isar/outer_keyword.scala	\
    4.18 +  Isar/outer_lex.scala Isar/outer_parse.scala Isar/outer_syntax.scala	\
    4.19 +  System/cygwin.scala System/gui_setup.scala				\
    4.20    System/isabelle_process.scala System/isabelle_syntax.scala		\
    4.21    System/isabelle_system.scala System/platform.scala			\
    4.22    System/session_manager.scala System/standard_system.scala		\
     5.1 --- a/src/Pure/System/cygwin.scala	Fri Jan 01 19:15:43 2010 +0100
     5.2 +++ b/src/Pure/System/cygwin.scala	Sat Jan 02 20:10:21 2010 +0100
     5.3 @@ -8,6 +8,8 @@
     5.4  
     5.5  import java.lang.reflect.Method
     5.6  import java.io.File
     5.7 +import java.net.URL
     5.8 +import java.awt.Component
     5.9  
    5.10  
    5.11  object Cygwin
    5.12 @@ -79,6 +81,14 @@
    5.13    private val CYGWIN_SETUP1 = "Software\\Cygwin\\setup"
    5.14    private val CYGWIN_SETUP2 = "Software\\Wow6432Node\\Cygwin\\setup"
    5.15  
    5.16 +  private def sanity_check(root: File)
    5.17 +  {
    5.18 +    if (!new File(root, "bin\\bash.exe").isFile ||
    5.19 +        !new File(root, "bin\\env.exe").isFile ||
    5.20 +        !new File(root, "bin\\tar.exe").isFile)
    5.21 +      error("Bad Cygwin installation: " + root.toString)
    5.22 +  }
    5.23 +
    5.24    def check_root(): String =
    5.25    {
    5.26      val root_env = java.lang.System.getenv("CYGWIN_ROOT")
    5.27 @@ -88,20 +98,29 @@
    5.28          query_registry(CYGWIN_SETUP1, "rootdir") orElse
    5.29          query_registry(CYGWIN_SETUP2, "rootdir") getOrElse
    5.30          error("Failed to determine Cygwin installation -- version 1.7 required")
    5.31 -    val ok =
    5.32 -      new File(root + "\\bin\\bash.exe").isFile &&
    5.33 -      new File(root + "\\bin\\env.exe").isFile
    5.34 -    if (!ok) error("Bad Cygwin installation: " + root)
    5.35 +    sanity_check(new File(root))
    5.36      root
    5.37    }
    5.38  
    5.39 -  def setup(exe: String, root: String): Int =
    5.40 +  def setup(parent: Component, root: File)
    5.41    {
    5.42 -    val (output, rc) = Standard_System.process_output(
    5.43 -    	Standard_System.raw_execute(null, true, exe, "-R", root, "-P", "perl,python", "-q", "-n"))
    5.44 -    val root_dir = new File(root)
    5.45 -    if (root_dir.isDirectory) Standard_System.write_file(new File(root, "setup.log"), output)
    5.46 -    rc
    5.47 +    if (!root.mkdirs) error("Failed to create root directory: " + root)
    5.48 +
    5.49 +    val download = new File(root, "download")
    5.50 +    if (!download.mkdir) error("Failed to create download directory: " + download)
    5.51 +
    5.52 +    val setup_exe = new File(root, "setup.exe")
    5.53 +
    5.54 +    try { Download.file(parent, new URL("http://www.cygwin.com/setup.exe"), setup_exe) }
    5.55 +    catch { case _: RuntimeException => error("Failed to download Cygwin setup program") }
    5.56 +
    5.57 +    val (_, rc) = Standard_System.process_output(
    5.58 +    	Standard_System.raw_execute(root, null, true,
    5.59 +    	  setup_exe.toString, "-R", root.toString, "-l", download.toString,
    5.60 +    	    "-P", "perl,python", "-q", "-n"))
    5.61 +    if (rc != 0) error("Cygwin setup failed!")
    5.62 +
    5.63 +    sanity_check(root)
    5.64    }
    5.65  }
    5.66  
     6.1 --- a/src/Pure/System/isabelle_system.scala	Fri Jan 01 19:15:43 2010 +0100
     6.2 +++ b/src/Pure/System/isabelle_system.scala	Sat Jan 02 20:10:21 2010 +0100
     6.3 @@ -43,7 +43,7 @@
     6.4          val cmdline =
     6.5            shell_prefix ::: List(isabelle_home + "/bin/isabelle", "getenv", "-d", dump.toString)
     6.6          val (output, rc) =
     6.7 -          Standard_System.process_output(Standard_System.raw_execute(env0, true, cmdline: _*))
     6.8 +          Standard_System.process_output(Standard_System.raw_execute(null, env0, true, cmdline: _*))
     6.9          if (rc != 0) error(output)
    6.10  
    6.11          val entries =
    6.12 @@ -66,7 +66,7 @@
    6.13      val cmdline =
    6.14        if (Platform.is_windows) List(platform_root + "\\bin\\env.exe") ++ args
    6.15        else args
    6.16 -    Standard_System.raw_execute(environment, redirect, cmdline: _*)
    6.17 +    Standard_System.raw_execute(null, environment, redirect, cmdline: _*)
    6.18    }
    6.19  
    6.20  
     7.1 --- a/src/Pure/System/standard_system.scala	Fri Jan 01 19:15:43 2010 +0100
     7.2 +++ b/src/Pure/System/standard_system.scala	Sat Jan 02 20:10:21 2010 +0100
     7.3 @@ -101,12 +101,13 @@
     7.4  
     7.5    /* shell processes */
     7.6  
     7.7 -  def raw_execute(env: Map[String, String], redirect: Boolean, args: String*): Process =
     7.8 +  def raw_execute(cwd: File, env: Map[String, String], redirect: Boolean, args: String*): Process =
     7.9    {
    7.10      val cmdline = new java.util.LinkedList[String]
    7.11      for (s <- args) cmdline.add(s)
    7.12  
    7.13      val proc = new ProcessBuilder(cmdline)
    7.14 +    if (cwd != null) proc.directory(cwd)
    7.15      if (env != null) {
    7.16        proc.environment.clear
    7.17        for ((x, y) <- env) proc.environment.put(x, y)