Add syntax node kinds to syntax json

[sorgfresser]

Currently, the Syntax part of the InfoTree json is missing a lot of information compared to the Syntax object in Lean. The changes here enable to check for specific SyntaxNodeKinds in the InfoTree. Also, I included the kinds of the node array, as these are not the same as the SyntaxNodeKind of child InfoTrees. The argKinds are for example needed to differentiate between theorem and def for a CommandInfo with a Syntax of SyntaxNodeKind Lean.Parser.Command.declaration.

For example, getting all theorems of an InfoTree (in Python using dataclasses for illustration) involves:

    def theorems(self) -> Generator[Self, None, None]:
        for tree in self.commands():
            if tree.node.stx.kind != "Lean.Parser.Command.declaration":
               continue
            if tree.node.stx.argKinds[-1] != "Lean.Parser.Command.theorem":
                continue
            yield tree

[kim-em]

Could you add a test that verifies this output?

[sorgfresser]

Thanks for the review @kim-em! Added a test now. Sadly, testing the theorem procedure described above requires a full infotree. I tried to keep the example as minimal as possible, but it's still almost 300 lines of expected output...