Opened 15 years ago

Closed 14 years ago

#298 closed defect (fixed)

Isabelle indentation

Reported by: Norbert Schirmer Owned by: David Aspinall
Priority: major Milestone: PG-Emacs-4.0
Component: 2:pg-emacs Keywords:
Cc:

Description (last modified by David Aspinall)

The automatic indentation for Isar proofs has some problems: currently, 

have A
by x

should be: 

have A
  by x

the same for: 

have A
apply x

otherwise subsequent 'haves' get out of line.

Change History (5)

comment:1 Changed 14 years ago by David Aspinall

Description: modified (diff)
Status: new → accepted

comment:2 Changed 14 years ago by Makarius

Seems to work again in Release-4-0pre091112

comment:3 Changed 14 years ago by Makarius

Err, works for Emacs 22 only, not Emacs 23 (both on Ubuntu 9.10).

comment:5 Changed 14 years ago by David Aspinall

Resolution: → fixed
Status: accepted → closed

Should be fixed in CVS head now.

Note: See TracTickets for help on using tickets.