stricter #eval syntax

Stream: lean4

[Damiano Testa]

Dear All,

is it possible to enforce that an #eval that spans several lines must have indented lines after the first? That is, I would like this behaviour:

#eval 0 -- accepted, no surprise

#eval
0 -- error, new behaviour

#eval
 0 -- accepted, with any non-zero number of spaces before the `0`

Thanks!

[James Gallicchio]

I'm not sure that's the behavior I'd want... is there justification for it?

[Damiano Testa]

This was a possible workaround for getting the end positions of the syntax: if #eval gives an error without an indent, I can guess where a command ends, by looking for the first line that begins without a space!

However, I think that your answer to my earlier questions may have solved this issue, thank you again!