Opened 11 years ago

Closed 11 years ago

#474 closed defect (fixed)

Indentation screwed up in sigT notations ("{ _ : _ & _ }") spanning multiple lines

Reported by: coquser Owned by: courtieu
Priority: minor Milestone: PG-Emacs-4.3
Component: 2:pg-emacs Keywords:
Cc:

Description

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.)

Change History (2)

comment:1 Changed 11 years ago by courtieu

Owner: changed from David Aspinall to courtieu
Status: newaccepted

Hi,

IMO the levels of Definitions are ok here: Definitions without an ":=" are starting a proof. So after the dot there is a shift to the right. Some other strange things are due to the lack of a dot at the end of commands.

However & is indeed badly indented. I will look at it.

Best regards. P.

Last edited 11 years ago by courtieu (previous) (diff)

comment:2 Changed 11 years ago by courtieu

Resolution: fixed
Status: acceptedclosed

Quick fix for &. But I still need a way to deal with all operators, even those declared by the user.

Note: See TracTickets for help on using tickets.