This PR solves #451 by demanding that trailing parsers are indented more than the surrounding withPosition call (if any). This mostly affects do blocks and tactics (where it enables a proper implementation of - tactic blocks). In particular, the only affected code in the stdlib (no regressions in the tests) is code of the form

do
  a
  <|> b

or

do
  a
  <|>
  b

I believe that breaking such code is justified: in my opinion, the "signal" for continuing an action over multiple lines comes "too late/weak" in this style. It should either be part of the first line, or clearly marked via indentation:

do
  a <|>
  b

or

do
  a
    <|>  b

The new rule accepts both of these styles, and for experimentation I've used both to fix the stdlib.

Now, for the sake of completeness I should mention that there is an alternative solution to #451 that does not break the above code but requires changes in tactic syntax declarations: if we change any declaration

syntax "tac" ... term ... : tactic

to

syntax "tac" ... withPosition(term) ... : tactic

then it should be sufficient to demand that trailing parsers are at least as instead of more indented (i.e. checkColGe instead of checkColGt): code such as

apply And.intro
- ...

would then be parsed as two tactics because the - is not as indented as And.intro. The obvious problem with this solution is that all tactic writers will have to be aware of this issue.