diff options
| author | David Aspinall | 1998-10-12 16:37:54 +0000 |
|---|---|---|
| committer | David Aspinall | 1998-10-12 16:37:54 +0000 |
| commit | 78bfc48fc58ef311c187be6b89e2fb9c006cf2c4 (patch) | |
| tree | 99714ec701906b18d14ca88888cae1811b3f775e | |
| parent | ecb7fa25b913a4a17378344275f727b4ec90c3a6 (diff) | |
Removed A* items done. Raised importance of FSF Emacs bug fix to A.
| -rw-r--r-- | todo | 13 |
1 files changed, 4 insertions, 9 deletions
@@ -14,6 +14,10 @@ X (Low) probably not worth wasting time on * This is a list of things which need doing in the generic interface ==================================================================== +A Bug in proof-shell-handle-output run on FSF Emacs, gives error + (wrong-type-argument markerp nil) when font-lock-fontify-region + is called to fontify the shell buffer. + B proof-issue-goal should refuse to work when a proof is in progress. Similarly proof-issue-save should refuse to work when a proof hasn't been completed! @@ -23,10 +27,6 @@ B Bug in proof-retract-until-point when called twice in succession: locked region, or "nothing to retract"). Problems is that there is a proof-locked-end, but it's at (point-min). -B Bug in proof-shell-handle-output run on FSF Emacs, gives error - (wrong-type-argument markerp nil) when font-lock-fontify-region - is called to fontify the shell buffer. - B proof-find-next-terminator doesn't work properly: first;second;third @@ -44,11 +44,6 @@ D Add proof-quit-command: some provers may like a quit command to be D Multiple files (after basic feature added): handle failures in reading ancestors. -A* Fix Non Sequitur nonsense with Isabelle when warnings appear before - proofstate. (da, 1hr?) - -A* Check & fix support for a recent version of FSFmacs. (da, 2hr). - A Add support for putting a locked region in processed files. (tms 4h) |
