changeset 64826 | c97296294f6d |
parent 64825 | e78b62c289bb |
child 64835 | fd1efd6dd385 |
--- a/src/Pure/PIDE/resources.scala Sat Jan 07 20:37:48 2017 +0100 +++ b/src/Pure/PIDE/resources.scala Sat Jan 07 20:44:37 2017 +0100 @@ -121,7 +121,7 @@ reader: Reader[Char], start: Token.Pos = Token.Pos.command, strict: Boolean = true) : Document.Node.Header = { - if (reader.source.length > 0) { + if (node_name.is_theory && reader.source.length > 0) { try { val header = Thy_Header.read(reader, start, strict).decode_symbols