fewer messages;
authorwenzelm
Sat Mar 17 21:54:33 2018 +0100 (14 months ago)
changeset 67898736673784fac
parent 67897 a5b9d1f51b04
child 67899 730fa992da38
fewer messages;
src/Pure/Thy/thy_resources.scala
     1.1 --- a/src/Pure/Thy/thy_resources.scala	Sat Mar 17 20:49:28 2018 +0100
     1.2 +++ b/src/Pure/Thy/thy_resources.scala	Sat Mar 17 21:54:33 2018 +0100
     1.3 @@ -65,6 +65,7 @@
     1.4            Document.Node.Commands.starts_pos(node.commands.iterator, Token.Pos.file(node_name.node))
     1.5          pos = command.span.keyword_pos(start).position(command.span.name)
     1.6          (_, tree) <- state.command_results(version, command).iterator
     1.7 +        if Protocol.is_inlined(tree)
     1.8         } yield (tree, pos)).toList
     1.9      }
    1.10    }