--- a/src/Pure/Thy/thy_header.scala Wed Oct 25 14:36:29 2017 +0200
+++ b/src/Pure/Thy/thy_header.scala Wed Oct 25 14:39:22 2017 +0200
@@ -189,10 +189,7 @@
def read(reader: Reader[Char], start: Token.Pos, strict: Boolean = true): Thy_Header =
{
val (_, tokens0) = read_tokens(reader, true)
- val text =
- if (reader.isInstanceOf[Scan.Byte_Reader])
- UTF8.decode_permissive(Token.implode(tokens0))
- else Token.implode(tokens0)
+ val text = Scan.reader_decode_utf8(reader, Token.implode(tokens0))
val (drop_tokens, tokens) = read_tokens(Scan.char_reader(text), strict)
val pos = (start /: drop_tokens)(_.advance(_))