# HG changeset patch
# User wenzelm
# Date 1310116401 -7200
# Node ID fb3d99df4b1e6c4df24d29db9fdc908bede7a785
# Parent  91c4d7397f0ed6facf0bc3d4698bb49db0bf222c
tuned signature;

diff -r 91c4d7397f0e -r fb3d99df4b1e src/Pure/Thy/thy_header.scala
--- a/src/Pure/Thy/thy_header.scala	Thu Jul 07 23:55:15 2011 +0200
+++ b/src/Pure/Thy/thy_header.scala	Fri Jul 08 11:13:21 2011 +0200
@@ -25,12 +25,10 @@
 
   val lexicon = Scan.Lexicon("%", "(", ")", ";", BEGIN, HEADER, IMPORTS, THEORY, USES)
 
-  final case class Header(val name: String, val imports: List[String], val uses: List[String])
+  sealed case class Header(val name: String, val imports: List[String], val uses: List[String])
   {
-    def decode_permissive_utf8: Header =
-      Header(Standard_System.decode_permissive_utf8(name),
-        imports.map(Standard_System.decode_permissive_utf8),
-        uses.map(Standard_System.decode_permissive_utf8))
+    def map(f: String => String): Header =
+      Header(f(name), imports.map(f), uses.map(f))
   }
 
 
@@ -97,7 +95,7 @@
   def read(file: File): Header =
   {
     val reader = Scan.byte_reader(file)
-    try { read(reader).decode_permissive_utf8 }
+    try { read(reader).map(Standard_System.decode_permissive_utf8) }
     finally { reader.close }
   }