# HG changeset patch
# User wenzelm
# Date 1261951803 -3600
# Node ID 619552fe8d7fd583f0a4940c24f70db54582a5a9
# Parent  b6960fc09ef3795240841f59a0917b6edd9c032c
allow UTF-8 in theory and file names;

diff -r b6960fc09ef3 -r 619552fe8d7f src/Pure/Thy/thy_header.scala
--- 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