tuned signature;
authorwenzelm
Fri Jul 08 11:13:21 2011 +0200 (2011-07-08)
changeset 43699fb3d99df4b1e
parent 43698 91c4d7397f0e
child 43700 e4ece46a9ca7
tuned signature;
src/Pure/Thy/thy_header.scala
     1.1 --- a/src/Pure/Thy/thy_header.scala	Thu Jul 07 23:55:15 2011 +0200
     1.2 +++ b/src/Pure/Thy/thy_header.scala	Fri Jul 08 11:13:21 2011 +0200
     1.3 @@ -25,12 +25,10 @@
     1.4  
     1.5    val lexicon = Scan.Lexicon("%", "(", ")", ";", BEGIN, HEADER, IMPORTS, THEORY, USES)
     1.6  
     1.7 -  final case class Header(val name: String, val imports: List[String], val uses: List[String])
     1.8 +  sealed case class Header(val name: String, val imports: List[String], val uses: List[String])
     1.9    {
    1.10 -    def decode_permissive_utf8: Header =
    1.11 -      Header(Standard_System.decode_permissive_utf8(name),
    1.12 -        imports.map(Standard_System.decode_permissive_utf8),
    1.13 -        uses.map(Standard_System.decode_permissive_utf8))
    1.14 +    def map(f: String => String): Header =
    1.15 +      Header(f(name), imports.map(f), uses.map(f))
    1.16    }
    1.17  
    1.18  
    1.19 @@ -97,7 +95,7 @@
    1.20    def read(file: File): Header =
    1.21    {
    1.22      val reader = Scan.byte_reader(file)
    1.23 -    try { read(reader).decode_permissive_utf8 }
    1.24 +    try { read(reader).map(Standard_System.decode_permissive_utf8) }
    1.25      finally { reader.close }
    1.26    }
    1.27