Curiosity about syntax positions

Stream: lean4

[Damiano Testa]

This question is mostly out of curiosity.

When Lean parses a file it creates Syntax objects for the various commands that the file contains.

1. Do the syntax ranges for the parsed commands cover the entire file (or the file until #exit)?
2. Is it true that the ranges of two syntax objects are either disjoint or nested?
3. Is it always the case that "comments"/whitespace are appended to the end of some Syntax leaf, or can they be somewhere else?

Thanks!

[Mario Carneiro]

1. it includes #exit, but not any commands following it, and also the header is parsed separately
2. Syntax objects are created synthetically too, so it's not always so simple. For syntax from the parser, yes this should be the case.
3. Yes, at least in theory; if you concatenate the atoms, leading/trailing whitespace, and the ident's rawVal you should reconstitute the exact contents of the original file.

[Damiano Testa]

Ok, great, thank you for the confirmation!

[Damiano Testa]

Even though I did not say so, I had in mind of only .original syntax: I had asked about creating "artificial" syntax nodes with specified ranges (and you and Eric showed me how to do it). Same goes for the header.