User command cannot be used directly after import

[Kha]

As witnessed in formalabstracts.

I can think of multiple workarounds to this:

• The one used in the link above and only one currently working: use any other command in between
• We already have noncomputable theory as a separator, so we could allow just theory as a dummy separator. I can think of some further cleanups on top of this: /-! -/ could become /-- -/ theory, prelude could become prelude theory.
• Allow . as a separator as with commands. Consistent, but looks a bit weird.
• Heuristic: Do not extend import statement to unindented lines. Works "out of the box", but we aren't usually whitespace sensitive.

[leodemoura]

Heuristic: Do not extend import statement to unindented lines. Works "out of the box", but we aren't usually whitespace sensitive.

This heuristic would solve other issues we have. By heuristic, I mean "blank lines as command separators". I'm fine with it. What do you think?

[leodemoura]

@kha I'm happy to hear more whitespace sensitive hacks that would make Lean nicer to use. Do you have more suggestions? :)

[Kha]

Right, I was considering using a blank lines heuristic for that as well at some point. I'm not sure any code would break right now (could be an interesting experiment), but I can imagine some users may want to format long proofs like follows

have h,
...,

have hh,
...,

-- we're finally done
show hhh, ...

So the heuristic may need to be a bit cleverer, e.g. only forbid blank lines inside top-level applications (which should be a very safe assumption).

[leodemoura]

So the heuristic may need to be a bit cleverer, e.g. only forbid blank lines inside top-level applications (which should be a very safe assumption).

I think if we just forbid it after , it would already be good enough.

We may also tell users to use -- on big proofs instead of blank line.

have h,
...,
--
have hh,
...,
--
-- we're finally done
show hhh, ...

I acknowledge this is not super nice.

[Kha]

I think if we just forbid it after , it would already be good enough.

Ok, sounds very reasonable.