--- a/Admin/build Fri Jan 08 14:34:18 2010 +0100
+++ b/Admin/build Sun Jan 10 18:14:29 2010 +0100
@@ -59,7 +59,7 @@
function build_browser ()
{
pushd "$ISABELLE_HOME/lib/browser" >/dev/null
- "$ISABELLE_TOOL" env ./build || fail "Failed!"
+ "$ISABELLE_TOOL" env ./build || exit $?
popd >/dev/null
}
@@ -84,7 +84,7 @@
function build_jars ()
{
pushd "$ISABELLE_HOME/src/Pure" >/dev/null
- "$ISABELLE_TOOL" env ./build-jars || fail "Failed!"
+ "$ISABELLE_TOOL" env ./build-jars || exit $?
popd >/dev/null
}
--- a/Admin/isatest/settings/mac-poly64-M4 Fri Jan 08 14:34:18 2010 +0100
+++ b/Admin/isatest/settings/mac-poly64-M4 Sun Jan 10 18:14:29 2010 +0100
@@ -4,7 +4,7 @@
ML_SYSTEM="polyml-5.3.0"
ML_PLATFORM="x86_64-darwin"
ML_HOME="$POLYML_HOME/$ML_PLATFORM"
- ML_OPTIONS="--mutable 4000 --immutable 2000"
+ ML_OPTIONS="--mutable 12000 --immutable 4000"
ISABELLE_HOME_USER=~/isabelle-mac-poly64-M4
--- a/Admin/isatest/settings/mac-poly64-M8 Fri Jan 08 14:34:18 2010 +0100
+++ b/Admin/isatest/settings/mac-poly64-M8 Sun Jan 10 18:14:29 2010 +0100
@@ -4,7 +4,7 @@
ML_SYSTEM="polyml-5.3.0"
ML_PLATFORM="x86_64-darwin"
ML_HOME="$POLYML_HOME/$ML_PLATFORM"
- ML_OPTIONS="--mutable 4000 --immutable 2000"
+ ML_OPTIONS="--mutable 12000 --immutable 4000"
ISABELLE_HOME_USER=~/isabelle-mac-poly64-M8
--- a/lib/Tools/browser Fri Jan 08 14:34:18 2010 +0100
+++ b/lib/Tools/browser Sun Jan 10 18:14:29 2010 +0100
@@ -60,7 +60,7 @@
## main
-[ -e "$ISABELLE_HOME/Admin/build" ] && "$ISABELLE_HOME/Admin/build" browser
+[ -e "$ISABELLE_HOME/Admin/build" ] && { "$ISABELLE_HOME/Admin/build" browser || exit $?; }
classpath "$ISABELLE_HOME/lib/browser/GraphBrowser.jar"
--- a/lib/Tools/scala Fri Jan 08 14:34:18 2010 +0100
+++ b/lib/Tools/scala Sun Jan 10 18:14:29 2010 +0100
@@ -4,7 +4,7 @@
#
# DESCRIPTION: invoke Scala within the Isabelle environment
-[ -e "$ISABELLE_HOME/Admin/build" ] && "$ISABELLE_HOME/Admin/build" jars
+[ -e "$ISABELLE_HOME/Admin/build" ] && { "$ISABELLE_HOME/Admin/build" jars || exit $?; }
CLASSPATH="$(jvmpath "$CLASSPATH")"
exec "$ISABELLE_SCALA" "$@"
--- a/src/Pure/General/exn.scala Fri Jan 08 14:34:18 2010 +0100
+++ b/src/Pure/General/exn.scala Sun Jan 10 18:14:29 2010 +0100
@@ -17,7 +17,7 @@
def capture[A](e: => A): Result[A] =
try { Res(e) }
- catch { case exn: RuntimeException => Exn[A](exn) }
+ catch { case exn: RuntimeException => Exn[A](exn) } // FIXME *all* exceptions (!?), cf. ML version
def release[A](result: Result[A]): A =
result match {
--- a/src/Pure/General/swing_thread.scala Fri Jan 08 14:34:18 2010 +0100
+++ b/src/Pure/General/swing_thread.scala Sun Jan 10 18:14:29 2010 +0100
@@ -29,9 +29,14 @@
result.get
}
- def future[A](body: => A): Future[A] = Future.fork { now(body) }
+ def future[A](body: => A): Future[A] =
+ {
+ if (SwingUtilities.isEventDispatchThread()) Future.value(body)
+ else Future.fork { now(body) }
+ }
- def later(body: => Unit) {
+ def later(body: => Unit)
+ {
if (SwingUtilities.isEventDispatchThread()) body
else SwingUtilities.invokeLater(new Runnable { def run = body })
}
--- a/src/Pure/System/standard_system.scala Fri Jan 08 14:34:18 2010 +0100
+++ b/src/Pure/System/standard_system.scala Sun Jan 10 18:14:29 2010 +0100
@@ -10,7 +10,7 @@
import java.util.Locale
import java.io.{BufferedWriter, OutputStreamWriter, FileOutputStream,
BufferedInputStream, FileInputStream, BufferedReader, InputStreamReader,
- File, IOException}
+ File, FileFilter, IOException}
import scala.io.Source
import scala.util.matching.Regex
@@ -98,6 +98,20 @@
finally { writer.close }
}
+ // FIXME handle (potentially cyclic) directory graph
+ def find_files(start: File, ok: File => Boolean): List[File] =
+ {
+ val files = new mutable.ListBuffer[File]
+ val filter = new FileFilter { def accept(entry: File) = entry.isDirectory || ok(entry) }
+ def find_entry(entry: File)
+ {
+ if (ok(entry)) files += entry
+ if (entry.isDirectory) entry.listFiles(filter).foreach(find_entry)
+ }
+ find_entry(start)
+ files.toList
+ }
+
/* shell processes */
--- a/src/Pure/Thy/thy_header.scala Fri Jan 08 14:34:18 2010 +0100
+++ b/src/Pure/Thy/thy_header.scala Sun Jan 10 18:14:29 2010 +0100
@@ -23,7 +23,7 @@
val lexicon = Scan.Lexicon("%", "(", ")", ";", BEGIN, HEADER, IMPORTS, THEORY, USES)
- sealed case class Header(val name: String, val imports: List[String], val uses: List[String])
+ final case class Header(val name: String, val imports: List[String], val uses: List[String])
}