src/Pure/PIDE/resources.scala
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