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
Keywords: | isabelle added |
---|---|
Milestone: | PG-Emacs-3.7 → PG-Emacs-3.7.1 |
Status: | new → assigned |
Type: | defect → enhancement |
comment:2 Changed 16 years ago by
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
Milestone: | PG-Emacs-3.7.1 → PG-Emacs-3.7.2 |
---|
comment:4 Changed 16 years ago by
Milestone: | PG-Emacs-3.7.2 → PG-Emacs-4.0 |
---|
comment:5 Changed 15 years ago by
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
Resolution: | → fixed |
---|---|
Status: | assigned → closed |
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!
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.