diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2003-06-05 10:45:12 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2003-06-05 10:45:12 +0000 |
| commit | 9c77766565cc9c29289ecf1c7d6c964d6af388ce (patch) | |
| tree | 6f63514fd2f153520142b29b72819d413502c551 | |
| parent | a9c79785fd0870121e3ab6de9b8963435c5c6548 (diff) | |
Make find-and-forget robust for proverproc regions
| -rw-r--r-- | coq/coq.el | 5 | ||||
| -rw-r--r-- | isar/isar.el | 1 | ||||
| -rw-r--r-- | lego/lego.el | 2 | ||||
| -rw-r--r-- | phox/phox-fun.el | 4 | ||||
| -rw-r--r-- | plastic/plastic.el | 1 |
5 files changed, 10 insertions, 3 deletions
@@ -267,7 +267,8 @@ toplevel \"Coq <\". Returns nil if yes. This assumes that no ;; nested proofs. -(defun coq-is-comment-p (span) (eq (span-property span 'type) 'comment)) +(defun coq-is-comment-or-proverprocp (span) + (memq (span-property span 'type) '(comment proverproc))) (defun coq-is-goalsave-p (span) (eq (span-property span 'type) 'goalsave)) (defun coq-is-module-equal-p (str) ;;cannot appear vith coq < 7.4 (and (proof-string-match "\\`\\(Declare\\s-\\)?\\s-*\\<Module\\>.*:=" str) @@ -304,7 +305,7 @@ toplevel \"Coq <\". Returns nil if yes. This assumes that no (while (and span (not ans)) (setq str (span-property span 'cmd)) (cond - ((coq-is-comment-p span)) ; do nothing + ((coq-is-comment-or-proverprocp span)) ; do nothing ;; Module <Type> T ... :=... . inside proof -> like Definition...:=... ;; (should actually be disallowed in coq) diff --git a/isar/isar.el b/isar/isar.el index 92ad071b..8b0d8327 100644 --- a/isar/isar.el +++ b/isar/isar.el @@ -423,6 +423,7 @@ proof-shell-retract-files-regexp." ;; str below) ;; FIXME: should adjust proof-nesting-depth here. ((or (eq (span-property span 'type) 'comment) + (eq (span-property span 'type) 'proverproc) (eq (span-property span 'type) 'proof); da: needed? (proof-string-match isar-undo-skip-regexp str) (proof-string-match isar-undo-ignore-regexp str))) diff --git a/lego/lego.el b/lego/lego.el index 00a32319..d5b882b9 100644 --- a/lego/lego.el +++ b/lego/lego.el @@ -208,6 +208,8 @@ Given is the first SPAN which needs to be undone." ((eq (span-property span 'type) 'comment)) + ((eq (span-property span 'type) 'proverproc)) + ((eq (span-property span 'type) 'goalsave) (unless (eq (span-property span 'name) proof-unnamed-theorem-name) (setq ans (format lego-forget-id-command (span-property span 'name))))) diff --git a/phox/phox-fun.el b/phox/phox-fun.el index d556a3c8..12dddf42 100644 --- a/phox/phox-fun.el +++ b/phox/phox-fun.el @@ -177,6 +177,8 @@ or for optional argument TABLE." ((eq (span-property span 'type) 'comment)) + ((eq (span-property span 'type) 'proverproc)) + ((eq (span-property span 'type) 'goalsave) (if (proof-string-match phox-prove-claim-regexp str) (setq ans (concat (format phox-forget-proof-command @@ -433,4 +435,4 @@ send a delete command to PhoX for the symbol whose name is under the cursor." (provide 'phox-fun) -
\ No newline at end of file + diff --git a/plastic/plastic.el b/plastic/plastic.el index 463ab4ec..c334cf53 100644 --- a/plastic/plastic.el +++ b/plastic/plastic.el @@ -244,6 +244,7 @@ Given is the first SPAN which needs to be undone." ;; so that Undo can be implemented via the tmp_cmd route.) (let (string (spans 0)) (while span + ;; FIXME da: should probably ignore comments/proverproc here? (setq string (span-property span 'cmd)) (plastic-preprocessing) ;; dynamic scope, on string |