From 9776eb58e079d5e6970e41e008ff4c2bf2bc1067 Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Sun, 6 Sep 2009 15:57:47 +0000 Subject: Tweak point movement in `proof-assert-until-point' and alter meaning of `proof-only-whitespace-to-locked-region-p'; both now refer to char after point. Script elements are now stored in hash tables rather than lists. --- generic/proof-script.el | 256 +++++++++++++++++++++--------------------------- 1 file changed, 112 insertions(+), 144 deletions(-) (limited to 'generic/proof-script.el') diff --git a/generic/proof-script.el b/generic/proof-script.el index 7b624b34..d26d7571 100644 --- a/generic/proof-script.el +++ b/generic/proof-script.el @@ -27,12 +27,6 @@ ;; Local variables used by proof-script-mode ;; -;; Scripting variables - -(defvar proof-element-counters nil - "Table of (name . count) pairs, counting elements in scripting buffer.") - - ;; Buffer-local variables (deflocal proof-active-buffer-fake-minor-mode nil @@ -46,7 +40,7 @@ buffer file name to nil before running kill buffer, which breaks PG's kill buffer hook. This variable is used when buffer-file-name is nil.") (deflocal pg-script-portions nil - "Lists of symbols naming processed script portions.") + "Alist of hash tables for symbols naming processed script portions.") @@ -58,11 +52,8 @@ kill buffer hook. This variable is used when buffer-file-name is nil.") (defun proof-next-element-count (idiom) "Return count for next element of type IDIOM. This uses and updates `proof-element-counters'." - (let ((next (1+ (or (cdr-safe (assq idiom proof-element-counters)) 0)))) - (setq proof-element-counters - (cons (cons idiom next) - (assq-delete-all idiom proof-element-counters))) - next)) + (let ((tbl (cdr-safe (assq idiom pg-script-portions)))) + (if tbl (1+ (hash-table-count tbl)) 1))) (defun proof-element-id (idiom number) "Return a string identifier composed from symbol IDIOM and NUMBER." @@ -266,8 +257,8 @@ will deactivated." (if proof-active-buffer-fake-minor-mode (setq proof-active-buffer-fake-minor-mode nil)) (proof-script-delete-spans (point-min) (point-max)) - (setq pg-script-portions nil) ;; also the record of them - (proof-detach-queue) ;; remove queue and locked + (setq pg-script-portions nil) + (proof-detach-queue) (proof-detach-locked) (proof-init-segmentation))) (if (eq buffer proof-script-buffer) @@ -373,9 +364,11 @@ Works on any buffer." (eq (proof-unprocessed-begin) (point-min))) (defun proof-only-whitespace-to-locked-region-p () - "Non-nil if only whitespace between point and end of locked region. + "Non-nil if only whitespace from char-after point and end of locked region. Point expected to be after the locked region." (save-excursion + (or (eq (point) (point-max)) + (forward-char 1)) (not (proof-re-search-backward "\\S-" (proof-unprocessed-begin) t)))) @@ -466,45 +459,39 @@ This is used for cleaning `buffer-invisibility-spec' in (defun pg-clear-script-portions () "Clear record of script portion names and types from internal list. Also clear all visibility specifications." - (setq pg-script-portions nil) - (mapcar 'remove-from-invisibility-spec - pg-visibility-specs)) - -(defun pg-add-script-element (elt) - (add-to-list pg-script-portions elt)) + (dolist (idtbl pg-script-portions) + (clrhash (cdr idtbl))) + (mapc 'remove-from-invisibility-spec pg-visibility-specs)) (defun pg-remove-script-element (ns id) - (let* ((elts (cdr-safe (assq ns pg-script-portions))) - (newelts (remq id elts))) - (setq pg-script-portions - (if newelts - (cons (cons ns newelts) (assq-delete-all ns pg-script-portions)) - (assq-delete-all ns pg-script-portions))))) + "Remove the identifier ID from the script portion NS." + (let* ((elts (cdr-safe (assq ns pg-script-portions)))) + (if elts (remhash id elts)))) (defsubst pg-visname (namespace id) "Return a unique symbol made from strings NAMESPACE and unique ID." (intern (concat namespace ":" id))) -(defun pg-add-element (idiom id span &optional name) - "Add element of type IDIOM with identifier ID, referred to by SPAN. +(defun pg-add-element (idiomsym id span &optional name) + "Add element of type IDIOMSYM with identifier ID, referred to by SPAN. This records the element in `pg-script-portions' and sets span properties accordingly. -IDIOM, ID, and optional NAME are all strings. +IDIOMSYM is a symbol, whereas ID and optional NAME are strings. Identifiers must be unique for a given idiom; the optional NAME will be recorded as a textual name used instead of ID for users; NAME does not need to be unique." - (let* ((idiomsym (intern idiom)) - (idsym (intern id)) + (let* ((idsym (intern id)) (name (or name id)) - (visname (pg-visname idiom id)) + (visname (pg-visname (symbol-name idiomsym) id)) (delfn `(lambda () (pg-remove-element (quote ,idiomsym) (quote ,idsym)))) (elts (cdr-safe (assq idiomsym pg-script-portions)))) - (if elts - (if (memq id elts) - (proof-debug "Element named " name " (type " idiom ") already in buffer.") - (nconc elts (list idsym))) - (setq pg-script-portions (cons (cons idiomsym (list idsym)) - pg-script-portions))) + (unless elts + (setq pg-script-portions + (cons (cons idiomsym (setq elts (makehash))) + pg-script-portions))) + (if (gethash id elts) + (proof-debug "Element named " name " (type " idiom ") already in buffer.") + (puthash idsym t elts)) ;; Idiom and ID are stored in the span as symbols; name as a string. (span-set-property span 'idiom idiomsym) (span-set-property span 'id idsym) @@ -568,13 +555,13 @@ NAME does not need to be unique." current-prefix-arg)) (let ((elts (cdr-safe (assq (intern idiom) pg-script-portions))) (alterfn (if hide - (lambda (arg) + (lambda (key val) (pg-make-element-invisible idiom - (symbol-name arg))) - (lambda (arg) + (symbol-name key))) + (lambda (key val) (pg-make-element-visible idiom - (symbol-name arg)))))) - (mapc alterfn elts)) + (symbol-name key)))))) + (maphash alterfn elts)) (pg-redisplay-for-gnuemacs)) ;; Next two could be in pg-user.el. No key-bindings for these. @@ -591,7 +578,7 @@ NAME does not need to be unique." (defun pg-add-proof-element (name span controlspan) "Add a span proof element to SPAN with name NAME and parent CONTROLSPAN." (let ((proofid (proof-next-element-id 'proof))) - (pg-add-element "proof" proofid span name) + (pg-add-element 'proof proofid span name) ;; Set id in controlspan (span-set-property controlspan 'id (intern proofid)) ;; Make a navigable link between the two spans. @@ -756,12 +743,6 @@ proof assistant and Emacs has a modified buffer visiting the file." ;; Tell the proof assistant, if we should and if we can (if (and informprover proof-shell-inform-file-processed-cmd) (progn - ;; Markus suggests we should ask if the user wants to save - ;; the file now (presumably because the proof assistant - ;; might examine the file timestamp, or attempt to visit - ;; the file later??). - ;; Presumably it would be enough to ask about this file, - ;; not all files? (if (and proof-query-file-save-when-activating-scripting (not noquestions)) @@ -1226,86 +1207,79 @@ With ARG, turn on scripting iff ARG is positive." (defun proof-done-advancing (span) "The callback function for `assert-until-point'. Argument SPAN has just been processed." - (if (or (not (span-live-p span)) - (not (buffer-live-p (span-buffer span)))) - (proof-debug - "proof-done-advancing: hit a dead span/buffer!") - - (let ((end (span-end span)) - (cmd (span-property span 'cmd))) - - (proof-set-locked-end end) - - (if (span-live-p proof-queue-span) - (proof-set-queue-start end)) - - (cond - ;; CASE 1: Comments just get highlighted - ((eq (span-property span 'type) 'comment) - (proof-done-advancing-comment span)) - - ;; CASE 2: Save command seen, now we may amalgamate spans. - ((and (proof-string-match-safe proof-save-command-regexp cmd) - ;; FIXME: would like to get rid of proof-really-save-command-p - ;; and use nested goals mechanism instead. - (funcall proof-really-save-command-p span cmd) - (decf proof-nesting-depth) ;; [always non-nil/true] - (if proof-nested-goals-history-p - ;; For now, we only support this nesting behaviour: - ;; don't amalgamate unless the nesting depth is 0, - ;; i.e. we're in a top-level proof. - ;; This assumes prover keeps history for nested proofs. - ;; (True for Isabelle/Isar). - (eq proof-nesting-depth 0) - t)) - (proof-done-advancing-save span)) - - ;; CASE 3: Proof completed one step or more ago, non-save - ;; command seen, no nested goals allowed. - ;; - ;; We make a fake goal-save from any previous - ;; goal to the command before the present one. - ;; - ;; This allows smooth undoing in proofs which have no "qed" - ;; statements. If your proof assistant doesn't allow these - ;; "unclosed" proofs, then you can safely set - ;; proof-completed-proof-behaviour. - ((and - proof-shell-proof-completed - (or (and (eq proof-completed-proof-behaviour 'extend) - (>= proof-shell-proof-completed 0)) - (and (eq proof-completed-proof-behaviour 'closeany) - (> proof-shell-proof-completed 0)) - (and (eq proof-completed-proof-behaviour 'closegoal) - (funcall proof-goal-command-p span)))) - (proof-done-advancing-autosave span)) - - ;; CASE 4: A "Require" type of command is seen (Coq). - ;; - ((and - proof-shell-require-command-regexp - (proof-string-match proof-shell-require-command-regexp cmd)) - ;; We take additional action dependent on prover - ;; [FIXME: use same method as in proof-shell here to - ;; recompute proof-included-files and adjust it] - ;; FIXME 2: we could annotate the Require ourselves - ;; at this point to contain the buffers which are - ;; being included! Then undoing can retract them. - (funcall proof-done-advancing-require-function span cmd) - ;; But do what we would have done anyway - (proof-done-advancing-other span)) - - ;; CASE 5: Some other kind of command (or a nested goal). - (t - (proof-done-advancing-other span))) - - ;; Add the processed command to the input ring - (unless (or (not (span-live-p span)) - (eq (span-property span 'type) 'comment)) - (pg-add-to-input-history cmd))) + (let ((end (span-end span)) + (cmd (span-property span 'cmd))) + + (proof-set-locked-end end) + + (if (span-live-p proof-queue-span) + (proof-set-queue-start end)) + + (cond + ;; CASE 1: Comments just get highlighted + ((eq (span-property span 'type) 'comment) + (proof-done-advancing-comment span)) + + ;; CASE 2: Save command seen, now we may amalgamate spans. + ((and (proof-string-match-safe proof-save-command-regexp cmd) + (funcall proof-really-save-command-p span cmd) + (decf proof-nesting-depth) ;; [always non-nil/true] + (if proof-nested-goals-history-p + ;; For now, we only support this nesting behaviour: + ;; don't amalgamate unless the nesting depth is 0, + ;; i.e. we're in a top-level proof. + ;; This assumes prover keeps history for nested proofs. + ;; (True for Isabelle/Isar). + (eq proof-nesting-depth 0) + t)) + (proof-done-advancing-save span)) + + ;; CASE 3: Proof completed one step or more ago, non-save + ;; command seen, no nested goals allowed. + ;; + ;; We make a fake goal-save from any previous + ;; goal to the command before the present one. + ;; + ;; This allows smooth undoing in proofs which have no "qed" + ;; statements. If your proof assistant doesn't allow these + ;; "unclosed" proofs, then you can safely set + ;; proof-completed-proof-behaviour. + ((and + proof-shell-proof-completed + (or (and (eq proof-completed-proof-behaviour 'extend) + (>= proof-shell-proof-completed 0)) + (and (eq proof-completed-proof-behaviour 'closeany) + (> proof-shell-proof-completed 0)) + (and (eq proof-completed-proof-behaviour 'closegoal) + (funcall proof-goal-command-p span)))) + (proof-done-advancing-autosave span)) + + ;; CASE 4: A "Require" type of command is seen (Coq). + ;; + ((and + proof-shell-require-command-regexp + (proof-string-match proof-shell-require-command-regexp cmd)) + ;; We take additional action dependent on prover + ;; [FIXME: use same method as in proof-shell here to + ;; recompute proof-included-files and adjust it] + ;; FIXME 2: we could annotate the Require ourselves + ;; at this point to contain the buffers which are + ;; being included! Then undoing can retract them. + (funcall proof-done-advancing-require-function span cmd) + ;; But do what we would have done anyway + (proof-done-advancing-other span)) + + ;; CASE 5: Some other kind of command (or a nested goal). + (t + (proof-done-advancing-other span))) + + ;; Add the processed command to the input ring + (unless (or (not (span-live-p span)) + (eq (span-property span 'type) 'comment)) + (pg-add-to-input-history cmd))) ;; Finally: state of scripting may have changed now, run hooks. - (run-hooks 'proof-state-change-hook))) + (run-hooks 'proof-state-change-hook)) @@ -1323,7 +1297,7 @@ Argument SPAN has just been processed." (max 1 (length comment-end))))) (id (proof-next-element-id 'comment)) str) - (pg-add-element "comment" id bodyspan) + (pg-add-element 'comment id bodyspan) (span-set-property span 'id (intern id)) (span-set-property span 'idiom 'comment) ;; this tries to extract last output, which is wrong for comments. @@ -1346,9 +1320,7 @@ Argument SPAN has just been processed." (defun proof-done-advancing-save (span) "A subroutine of `proof-done-advancing'. Add info for save span SPAN." (unless (eq proof-shell-proof-completed 1) - ;; We expect saves to succeed only for recently completed proofs. - ;; Give a hint to the proof assistant implementor in case something - ;; odd is going on. (NB: this is normal for nested proofs, though). + ;; We expect saves to succeed only for recently completed top-level proofs. (proof-debug (format "PG: save command with proof-shell-proof-completed=%s, proof-nesting-depth=%s" @@ -1363,9 +1335,6 @@ Argument SPAN has just been processed." (cmd (span-property span 'cmd)) lev nestedundos nam next) - ;; Try to set the name of the theorem from the save - ;; (message "%s" cmd) 3.4: remove this message. - (and proof-save-with-hole-regexp (proof-string-match proof-save-with-hole-regexp cmd) ;; Give a message of a name if one can be determined @@ -1420,11 +1389,11 @@ Argument SPAN has just been processed." (proof-warning "Proof General: script management confused, couldn't find goal span for save.") - ;; If the name isn't set, try to set it from the goal, - ;; or as a final desparate attempt, set the name to - ;; proof-unnamed-theorem-name (Coq actually uses a default - ;; name for unnamed theorems, believe it or not, and issues - ;; a name-binding error for two unnamed theorems in a row!). + ;; If the name isn't set, try to set it from the goal, or as a + ;; final desparate attempt, set the name to + ;; proof-unnamed-theorem-name (Coq actually uses a default name + ;; for unnamed theorems, believe it or not, and issues a + ;; name-binding error for two unnamed theorems in a row!). (setq nam (or nam (proof-get-name-from-goal gspan) proof-unnamed-theorem-name)) @@ -1445,8 +1414,8 @@ Argument GOALEND is the end of the goal;." (span-set-property gspan 'name nam) (and nestedundos (span-set-property gspan 'nestedundos nestedundos)) (pg-set-span-helphighlights gspan) - ;; Now make a nested span covering the purported body of the - ;; proof, and add to buffer-local list of elements. + ;; Now make a nested span covering the purported body of the proof, + ;; and add to buffer-local list of elements. (let ((proofbodyspan (span-make goalend (if proof-script-integral-proofs saveend savestart)))) @@ -1974,7 +1943,6 @@ Set the callback to CALLBACK-FN or `proof-done-advancing' by default." "At end of the locked region, nothing to do to!")) (let ((semis (save-excursion (skip-chars-backward " \t\n") - (backward-char) (proof-segment-up-to-using-cache (point))))) (if (eq 'unclosed-comment (car semis)) (setq semis (cdr semis))) -- cgit v1.2.3