Parsing imports from a syntax linter

Stream: lean4

[Michael Rothgang]

The other day, I was trying to match import statements using a syntax linter, which didn't work. Is this because import is a keyword (right?), which doesn't have its own syntax kind? Or am I overlooking something? (I know there are environment linters about imports.)

To un-#xy, I'd like to write a linter which underlines problematic import statements directly.
Can environment linters do this? #lint doesn't do this... if an environment linter can to this, I'm happy with that too.

[Damiano Testa]

I think that the Environment contains the imported modules (the ones actually corresponding to import xxx, not the transitive closure). However, I don't think that you can access their syntax node, so I would not know how to do the highlighting.