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