Opened 16 years ago

Closed 15 years ago

#188 closed enhancement (fixed)

Option to treat comments as individual statements.

Reported by: RafalKolanski Owned by: David Aspinall
Priority: minor Milestone: PG-Emacs-4.0
Component: 2:pg-emacs Keywords: comment parsing isabelle
Cc:

Description

The commands of type (* comment *) and -- "comment" are absorbed as part of the previous command. They hardly ever describe the previous command, instead describing the *following* one.

I would much prefer if when I pressed "previous" or performed an undo using c-c c-return, I could go up to before the comment without undoing the previous command.

This is one of the reasons I've taken to working with strict read-only turned off, but for beginners this is not such a good idea.

Change History (6)

comment:1 Changed 16 years ago by David Aspinall

Keywords: isabelle added
Milestone: PG-Emacs-3.7PG-Emacs-3.7.1
Status: newassigned
Type: defectenhancement

Thanks for the suggestion. I agree with the first case but I thought comments --- "like this" specifically referred to the previous command?

Anyway, I think this would need a bit of reworking inside the parsing code for Isabelle, which requires a strong constitution and a steady hand. So I'm bumping this to the next release.

comment:2 Changed 16 years ago by RafalKolanski

I've thought about this. With -- comments I think you're right. However, I do find myself sometimes changing these comments, at which point I just want to step back to before the comment, not before the whole command. Anyway, thanks for taking it into account, I'm looking forward to it in the next version!

comment:3 Changed 16 years ago by David Aspinall

Milestone: PG-Emacs-3.7.1PG-Emacs-3.7.2

comment:4 Changed 16 years ago by David Aspinall

Milestone: PG-Emacs-3.7.2PG-Emacs-4.0

comment:5 Changed 15 years ago by Makarius

There is a bit of a misunterstanding here what a "comment" actually is in Isar. (* source comments *) are not part of the proper text -- it is hard to associate them with one command or the other (although some newer internal Isabelle source parsing mechanisms treat such comments *between* commands as belonging to neither side).

Note that the main purpose of (* foo *) is to comment out things, or indicate strange technical problems. A bit like % in TeX. Normally you never put text to be read by the user within (). Proper formal comments are always explicitly marked up as such, using -- "text" for small things, or the commands 'text', 'txt' respectively.

comment:6 Changed 15 years ago by David Aspinall

Resolution: fixed
Status: assignedclosed

There's a new option 'Retract on Edit' which allows you to edit some comments without needing to undo them. Additionally, the -- "comments" like this are classified as comments now. I think this is a reasonable fix to this problem without altering parsing, hope you like it!

Note: See TracTickets for help on using tickets.