misc tuning;
authorwenzelm
Sat Jan 09 23:22:56 2010 +0100 (2010-01-09)
changeset 343003f2e25dc99ab
parent 34299 68716caa7745
child 34301 78c10aea025d
child 34309 d91c3fce478e
child 34907 b0aaec87751c
misc tuning;
src/Pure/General/exn.scala
src/Pure/System/standard_system.scala
src/Pure/Thy/thy_header.scala
     1.1 --- a/src/Pure/General/exn.scala	Sat Jan 09 23:22:24 2010 +0100
     1.2 +++ b/src/Pure/General/exn.scala	Sat Jan 09 23:22:56 2010 +0100
     1.3 @@ -17,7 +17,7 @@
     1.4  
     1.5    def capture[A](e: => A): Result[A] =
     1.6      try { Res(e) }
     1.7 -    catch { case exn: RuntimeException => Exn[A](exn) }
     1.8 +    catch { case exn: RuntimeException => Exn[A](exn) }   // FIXME *all* exceptions (!?), cf. ML version
     1.9  
    1.10    def release[A](result: Result[A]): A =
    1.11      result match {
     2.1 --- a/src/Pure/System/standard_system.scala	Sat Jan 09 23:22:24 2010 +0100
     2.2 +++ b/src/Pure/System/standard_system.scala	Sat Jan 09 23:22:56 2010 +0100
     2.3 @@ -98,6 +98,7 @@
     2.4      finally { writer.close }
     2.5    }
     2.6  
     2.7 +  // FIXME handle (potentially cyclic) directory graph
     2.8    def find_files(start: File, ok: File => Boolean): List[File] =
     2.9    {
    2.10      val files = new mutable.ListBuffer[File]
     3.1 --- a/src/Pure/Thy/thy_header.scala	Sat Jan 09 23:22:24 2010 +0100
     3.2 +++ b/src/Pure/Thy/thy_header.scala	Sat Jan 09 23:22:56 2010 +0100
     3.3 @@ -23,7 +23,7 @@
     3.4  
     3.5    val lexicon = Scan.Lexicon("%", "(", ")", ";", BEGIN, HEADER, IMPORTS, THEORY, USES)
     3.6  
     3.7 -  sealed case class Header(val name: String, val imports: List[String], val uses: List[String])
     3.8 +  final case class Header(val name: String, val imports: List[String], val uses: List[String])
     3.9  }
    3.10  
    3.11