fix(library/definitional/projection): remove redundant 'error in'
fix(frontends/lean/info_manager): suppress useless tactic type information, closes #277
fix(emacs/lean-flycheck): should accept error messages with empty lines
feat(library/tactic/proof_state): add empty line between goals, closes #281
fix(frontends/lean/elaborator): incorrect error position in begin-end block, fixes #276
feat(emacs/lean-info): add goal visualization options 'lean-proofstate-display-style'

lean-proofstate-display-style:

 - 'show-all: Show all goals
        a : Prop,
        b : Prop,
        c : Prop,
        H_1 : a,
        H_2 : b,
        H_3 : c
        ⊢ id a

        a : Prop,
        b : Prop,
        c : Prop,
        H_1 : a,
        H_2 : b,
        H_3 : c
        ⊢ b ∧ c

 - 'show-first: Show only the first
        a : Prop,
        b : Prop,
        c : Prop,
        H_1 : a,
        H_2 : b,
        H_3 : c
        ⊢ id a

 - 'show-first-and-other-conclusions: Show the first goal, and the
   conclusions of all other goals (DEFAULT OPTION)
        a : Prop,
        b : Prop,
        c : Prop,
        H_1 : a,
        H_2 : b,
        H_3 : c
        ⊢ id a

        ⊢ b ∧ c

Close #279
test(emacs/lean-info-test): add test cases for goal visualization

[skip ci]