--- a/src/Pure/Thy/thy_header.scala Sun Dec 27 23:09:16 2009 +0100
+++ b/src/Pure/Thy/thy_header.scala Sun Dec 27 23:10:03 2009 +0100
@@ -36,8 +36,8 @@
val header: Parser[Header] =
{
- val file_name = atom("file name", _.is_name)
- val theory_name = atom("theory name", _.is_name)
+ val file_name = atom("file name", _.is_name) ^^ Library.decode_permissive_utf8
+ val theory_name = atom("theory name", _.is_name) ^^ Library.decode_permissive_utf8
val file =
keyword("(") ~! (file_name ~ keyword(")")) ^^ { case _ ~ (x ~ _) => x } | file_name