Custom Query (361 matches)

Here's some code formatted by TAB in emacs PG:

Definition A
: { T : ReallySuperDuperExtremelyLongName bar baz qux &
                                          foo T }.
  Definition B
  : { T : (ReallySuperDuperExtremelyLongName bar baz qux) &
                                                          foo T }

      Definition C
  : { T : ReallySuperDuperExtremelyLongName bar baz qux
                                            & foo T }.
    Definition D
    : { T : (ReallySuperDuperExtremelyLongName bar baz qux)
              & foo T }

The indentation of Definition is clearly broken. Additionally, I think all of them should be formatted roughly like Definition D, where the & or the foo is lined up close to the start of the line, rather than as an argument of ReallySuperDuperExtremelyLongName. I'd be even happier if sigT notation were formatted like sig notation, that is, if & acted like | here. (This change doessn't fix the screwy levels of Definition, though.)

At some point (I think related to emacs 24) Proof General changed its way for indenting lines under quantifiers. E.g.

Lemma foo_bar_baz : forall x y z,

x = y -> y = z -> x = z.

Is there a way to revert to the previous 2-space indent from the indent at the beginning of the line?

When (= (point) (point-min)), the pair coq-grab-punctuation-left/coq-is-symbol-or-punct returns an error.