author | wenzelm |
Sat, 17 Mar 2018 21:54:33 +0100 | |
changeset 67898 | 736673784fac |
parent 67897 | a5b9d1f51b04 |
child 67899 | 730fa992da38 |
--- a/src/Pure/Thy/thy_resources.scala Sat Mar 17 20:49:28 2018 +0100 +++ b/src/Pure/Thy/thy_resources.scala Sat Mar 17 21:54:33 2018 +0100 @@ -65,6 +65,7 @@ Document.Node.Commands.starts_pos(node.commands.iterator, Token.Pos.file(node_name.node)) pos = command.span.keyword_pos(start).position(command.span.name) (_, tree) <- state.command_results(version, command).iterator + if Protocol.is_inlined(tree) } yield (tree, pos)).toList } }