# HG changeset patch # User wenzelm # Date 1263075776 -3600 # Node ID 3f2e25dc99ab91690178bade1b32c96aa933865d # Parent 68716caa77458a2d14d133f3a75efc4012a01635 misc tuning; diff -r 68716caa7745 -r 3f2e25dc99ab src/Pure/General/exn.scala --- 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 { diff -r 68716caa7745 -r 3f2e25dc99ab src/Pure/System/standard_system.scala --- 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] diff -r 68716caa7745 -r 3f2e25dc99ab src/Pure/Thy/thy_header.scala --- 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]) }