diff options
| -rw-r--r-- | doc/NewDoc.texi | 5 | ||||
| -rw-r--r-- | lego/lego.el | 25 | ||||
| -rw-r--r-- | todo | 8 |
3 files changed, 3 insertions, 35 deletions
diff --git a/doc/NewDoc.texi b/doc/NewDoc.texi index 941c35a6..9c04543d 100644 --- a/doc/NewDoc.texi +++ b/doc/NewDoc.texi @@ -1315,7 +1315,7 @@ front of the list. When the prover retracts across file boundaries, this list is resynchronised. It contains files in canonical truename format. @inforef{Truenames,,lispref}. You should not set this variable directly. The generic Proof General will modify @code{proof-included-files-list} -itself. Instead for a specific proof assistant you need to customise +itself. Instead, for a specific proof assistant you need to customise @code{proof-shell-process-file}. @code{proof-shell-retract-files-regexp} and @code{proof-shell-compute-new-files-list}. @@ -1388,9 +1388,6 @@ Rod Burstall, Paul Callaghan, Martin Hofmann, James McKinna, -Mark Ruys, -Martin Steffen, -Perdita Stevens, and Markus Wenzel. Thanks to all of you! diff --git a/lego/lego.el b/lego/lego.el index 8fd09c64..8821591a 100644 --- a/lego/lego.el +++ b/lego/lego.el @@ -185,28 +185,11 @@ ;; Code that's lego specific ;; ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; Martin Steffen <mnsteffe@informatik.uni-erlangen.de> has pointed -;; out that calling lego-get-path has to deal with a user who hasn't -;; set the environmental variable LEGOPATH. It is probably best if -;; lego is installed as a shell script which sets a sensible default -;; for LEGOPATH if the user hasn't done so before. See the -;; documentation of the library for further details. - -(defun lego-get-path () - (let ((path-name (getenv lego-path-name))) - (cond ((not path-name) - (message "Warning: LEGOPATH has not been set!") - (setq path-name "."))) - (proof-string-to-list path-name lego-path-separator))) - -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; This is how to work out what the undo commands are, given the ;; -;; first span which needs to be undone ;; -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - ;; needs to handle Normal as well ;; it should ignore Normal TReg Normal VReg and (Normal ...) (defun lego-count-undos (span) + "This is how to work out what the undo commands are. +Given is the first SPAN which needs to be undone." (let ((ct 0) str i) (while span (setq str (span-property span 'cmd)) @@ -428,10 +411,6 @@ ("lego" . lego-tags)) tag-table-alist))) -;; where to find files - - (setq compilation-search-path (cons nil (lego-get-path))) - (setq blink-matching-paren-dont-ignore-comments t) ;; font-lock @@ -389,14 +389,6 @@ X pbp code doesn't quite accord with the tech report; in particular it C fix Pbp implementation (10h) -B `lego-get-path' assumes that LEGOPATH has been set in the - environment. This is not likely to be the case with the current lego - shell script. Proof General needs to query the LEGO process as part - of `lego-process-config' e.g. by - sending (a yet to be implemented command) LEGOPATH. The output could - be analysed with the help of a LEGO specific extension of - `proof-shell-process-urgent-message'. (1h tms) - B Equiv, Next,... aren't handled properly, because LEGO does not refresh the proof state. Perhaps it would be easiest to get LEGO to output more information in proof script mode (2h) |