diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2000-04-25 12:04:08 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2000-04-25 12:04:08 +0000 |
| commit | 3d24958fe1b4db950e5f4cb45ca5db122a84f62b (patch) | |
| tree | 565d34b20ca0e12f4c1a336a8a8e5ffde712533b | |
| parent | 77a02fbecc93f93e54bcd295c9d74b35e1c01473 (diff) | |
Note about efficiency/bug fix by Markus.
| -rw-r--r-- | CHANGES | 5 | ||||
| -rw-r--r-- | generic/proof-script.el | 6 |
2 files changed, 5 insertions, 6 deletions
@@ -16,6 +16,11 @@ *** Improved behaviour of electric terminator +*** Efficiency improvement in parsing + + Also works around crash bug in xemacs-21.1.7/SuSE. + Fix by Markus Wenzel. + *** Added possibility for switching prover's output on/off. Already implemented in Coq and Isabelle(/Isar). diff --git a/generic/proof-script.el b/generic/proof-script.el index 00e7c564..6d2708b2 100644 --- a/generic/proof-script.el +++ b/generic/proof-script.el @@ -1182,12 +1182,6 @@ the ACS is marked in the current buffer. If CMD does not match any, ;; Emacs should be better at skipping whitespace and comments than the ;; proof process itself! -;; FIXME da: this annoyingly slow even in a buffer only several -;; hundred lines long, even when compiled. -;; One improvement would be to make a list of buffer *positions* -;; rather than strings, or at least, not by allocating a -;; string possibly as large as the buffer!!! - ;; FIXME da: using the family of functions buffer-syntactic-context-* ;; may be helpful here. |