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
Owner: | changed from David Aspinall to courtieu |
---|---|
Status: | new → accepted |
comment:2 Changed 11 years ago by
Resolution: | → fixed |
---|---|
Status: | accepted → closed |
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.
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.