diff options
author | Hendrik Tews <hendrik@askra.de> | 2011-01-21 09:59:35 +0000 |
---|---|---|
committer | Hendrik Tews <hendrik@askra.de> | 2011-01-21 09:59:35 +0000 |
commit | e8e9187778549aa132b33321394345c99992b8b4 (patch) | |
tree | 7df88deb31bf8572f90b345302011ce5bb90bf73 /coq | |
parent | 70140e80a12f3081cfc3fdf2c77ca759cc02dddc (diff) |
- use time-less-p
- delete previous-head, simplify loop
- coq 8.2 compatibility
- describe bug for killing completely asserted active buffers in
coq/ex/test-cases/retract-completely-asserted
Diffstat (limited to 'coq')
-rw-r--r-- | coq/coq.el | 43 | ||||
-rw-r--r-- | coq/ex/test-cases/retract-completely-asserted/README | 10 |
2 files changed, 26 insertions, 27 deletions
@@ -1095,7 +1095,10 @@ Currently this doesn't take the loadpath into account." ;; ;; TODO list: -;; - update patch website +;; - 1 second precision problem +;; - bug: killing buffer omits coqtop restart +;; - unlock ancestors on retract, see span-delete, span-delete-action +;; - modify behavior of locked ancestors, see proof-span-read-only ;; - display coqdep errors in the recompile-response buffer ;; - use a variable for the recompile-response buffer ;; - fix problem with partial library names @@ -1253,27 +1256,18 @@ identifier and should therefore not be matched by this regexp.") ;; basic utilities -(defun time-less (time-1 time-2) - "Return `t' if time value time-1 is earlier than time-2. +(defun time-less-or-equal (time-1 time-2) + "Return `t' if time value time-1 is earlier or equal to time-2. A time value is a list of two integers as returned by `file-attributes'. The first integer contains the upper 16 bits and the second the lower 16 bits of the time." - (if (< (car time-1) (car time-2)) - t - (if (= (car time-1) (car time-2)) - (< (nth 1 time-1) (nth 1 time-2)) - nil))) - -(defun time-less-or-equal (time-1 time-2) - "Return `t' if time value time-1 is earlier or equal to time-2. -For time values see `time-less'." - (or (time-less time-1 time-2) + (or (time-less-p time-1 time-2) (equal time-1 time-2))) (defun coq-max-dep-mod-time (dep-mod-times) "Return the maximum in DEP-MOD-TIMES. Argument DEP-MOD-TIMES is a list where each element is either a -time value (see `time-less') or 'just-compiled. The +time value (see `time-less-or-equal') or 'just-compiled. The function returns the maximum of the elements in DEP-MOD-TIMES, where 'just-compiled is considered the greatest time value. If DEP-MOD-TIMES is empty it returns nil." @@ -1285,7 +1279,7 @@ DEP-MOD-TIMES is empty it returns nil." dep-mod-times nil)) ((eq max nil) (setq max (car dep-mod-times))) - ((time-less max (car dep-mod-times)) + ((time-less-p max (car dep-mod-times)) (setq max (car dep-mod-times)))) (setq dep-mod-times (cdr-safe dep-mod-times))) max)) @@ -1367,7 +1361,7 @@ break." coq-dependency-analyzer nil (current-buffer) nil coqdep-arguments) (setq coqdep-output (buffer-string))) ;(message "coqdep output on %s: %s" lib-src-file coqdep-output) - (if (string-match "^\\*\\*\\* Warning:" coqdep-output) + (if (string-match "^\\*\\*\\* Warning" coqdep-output) "unsatisfied dependencies" (if (string-match ": \\(.*\\)$" coqdep-output) (cdr-safe (split-string (match-string 1 coqdep-output))) @@ -1412,8 +1406,8 @@ Argument MAX-DEP-OBJ-TIME provides the information about the dependencies. It is either - 'just-compiled if one of the dependencies of SRC has just been compiled -- the time value (see`time-less') of the youngest (most recently - created) object file among the dependencies +- the time value (see`time-less-or-equal') of the youngest (most + recently created) object file among the dependencies - nil if there are no dependencies, or if they are all ignored If this function decides to compile SRC to OBJ it returns @@ -1445,7 +1439,7 @@ Check if LIB-OBJ-FILE and all it dependencies are up-to-date compiled coq library objects. Recompile the necessary objects, if not. This function returns 'just-compiled if it compiled LIB-OBJ-FILE. Otherwise it returns the modification time of -LIB-OBJ-FILE as time value (see `time-less'). +LIB-OBJ-FILE as time value (see `time-less-or-equal'). Either LIB-OBJ-FILE or its source file (or both) must exist when entering this function. @@ -1613,17 +1607,14 @@ current buffer (which contains the Require command) to If `coq-compile-before-require' it t this function performs the compilation (if necessary) of the dependencies." (if coq-compile-before-require - (let ((items queueitems) - (previous-head nil) - ;; coq-object-hash-symbol serves as a pointer to the + (let (;; coq-object-hash-symbol serves as a pointer to the ;; coq-obj-hash (see coq-make-lib-up-to-date). The hash ;; will be initialized when needed and stored in the value ;; cell of coq-object-hash-symbol. The symbol is initialized ;; here to use one hash for all the requires that are added now. (coq-object-hash-symbol nil) item string) - (while items - (setq item (car items)) + (dolist (item queueitems) ;; XXX car or concat ? (setq string (car (nth 1 item))) (when (and string @@ -1634,9 +1625,7 @@ compilation (if necessary) of the dependencies." (while (string-match coq-require-id-regexp string start) (setq start (match-end 0)) (coq-check-module 'coq-object-hash-symbol - (match-string 1 string))))) - (setq previous-head items) - (setq items (cdr items)))))) + (match-string 1 string))))))))) (add-hook 'proof-shell-extend-queue-hook 'coq-preprocess-require-commands) diff --git a/coq/ex/test-cases/retract-completely-asserted/README b/coq/ex/test-cases/retract-completely-asserted/README index 68cca029..efdbdab0 100644 --- a/coq/ex/test-cases/retract-completely-asserted/README +++ b/coq/ex/test-cases/retract-completely-asserted/README @@ -18,3 +18,13 @@ To see that the example is indeed valid, script c.v. (For c.v you either have to switch coq-recompile-before-require to t or you have to compile modules a and b yourself with "coqc a" and "coqc b".) + +There is a bug present on 2011-01-21 09:49:36 UTC, to reproduce: +- visit a.v, do C-c C-n twice to fully assert the buffer +- kill buffer a.v, notice that there is no "coq killed" message + apprears, and that the *coq* buffer is still live and that there is + no undo command in it +- visit b.v, do C-c C-n twice to get the error "a already exists" + +See "no deactivation-hooks when killing fully asserted active buffer" +on the pg-devel list. |