We currently do so only for app. A general check seems consistent with Lean's indentation sensitivity and will allow us to introduce syntax such as tactic blocks as in

  apply And.intro
  - simp

which should not be interpreted as apply (And.intro - simp)