--- a/src/Pure/General/exn.scala Sat Jan 09 23:22:24 2010 +0100
+++ b/src/Pure/General/exn.scala Sat Jan 09 23:22:56 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/System/standard_system.scala Sat Jan 09 23:22:24 2010 +0100
+++ b/src/Pure/System/standard_system.scala Sat Jan 09 23:22:56 2010 +0100
@@ -98,6 +98,7 @@
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]
--- a/src/Pure/Thy/thy_header.scala Sat Jan 09 23:22:24 2010 +0100
+++ b/src/Pure/Thy/thy_header.scala Sat Jan 09 23:22:56 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])
}