# HG changeset patch
# User haftmann
# Date 1263143669 -3600
# Node ID d91c3fce478eb1909dedb04a70f0b3819589a621
# Parent  3f2e25dc99ab91690178bade1b32c96aa933865d# Parent  394fc3cce91561f7ef971e51e9f6c885564f1daf
merged

diff -r 394fc3cce915 -r d91c3fce478e Admin/build
--- 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
 }
 
diff -r 394fc3cce915 -r d91c3fce478e Admin/isatest/settings/mac-poly64-M4
--- 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
diff -r 394fc3cce915 -r d91c3fce478e Admin/isatest/settings/mac-poly64-M8
--- 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
diff -r 394fc3cce915 -r d91c3fce478e lib/Tools/browser
--- 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"
 
diff -r 394fc3cce915 -r d91c3fce478e lib/Tools/scala
--- 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" "$@"
diff -r 394fc3cce915 -r d91c3fce478e src/Pure/General/exn.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 {
diff -r 394fc3cce915 -r d91c3fce478e src/Pure/General/swing_thread.scala
--- 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 })
   }
diff -r 394fc3cce915 -r d91c3fce478e src/Pure/System/standard_system.scala
--- 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 */
 
diff -r 394fc3cce915 -r d91c3fce478e src/Pure/Thy/thy_header.scala
--- 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])
 }