diff options
| -rw-r--r-- | todo | 14 |
1 files changed, 7 insertions, 7 deletions
@@ -31,13 +31,19 @@ A BUGS to investigate: - Is there a catch bug on Solaris when a process shell killed? - There is a bizarre process bug with "\"'s on 254th character. This now seems to be the root cause of the Solaris bug mentioned - later, and might be XEmacs rather than Solaris. + below. - Thomas has a bizarre .emacs file which causes Seg Faults with Proof General and FSF Emacs. Doesn't happen with "emacs -q". Investigate which package/setting he adds is to blame. - outline mode when proof-strict-read-only is nil ought to work, but there may be problems. +B We need to go over to piped communication rather than ptys to fix + the (Solaris) ^G bug. (Set process-connection-type to nil). + In this circumstance there's a bug in the eager annotation code. + Document this problem so that it can be tested for future versions. + [Currently the problem is documented in Email messages sent to lego] + A Fix INFO-DIR-ENTRY in doc/ProofGeneral.texi to put Proof General info file into a good place. @@ -406,12 +412,6 @@ X Ideas for efficiency improvements. Rather than repeatedly The function proof-segment-up-to could be made to cache its result. -X We need to go over to piped communication rather than ptys to fix - the (Solaris) ^G bug. In this circumstance there's a bug in the - eager annotation code. Document this problem so that it can be - tested for future versions. [Currently the problem is documented in - Email messages sent to lego] - X proof-mark-buffer-atomic marks the buffer as only containing comments if the first ACS is a goal-save span. This is however not a problem for LEGO and Isabelle. (30 min) |