diff options
| author | David Aspinall | 2002-08-08 09:56:10 +0000 |
|---|---|---|
| committer | David Aspinall | 2002-08-08 09:56:10 +0000 |
| commit | 0d884890e6c75cf93e3f647bf40d399345088c71 (patch) | |
| tree | eec63cedb0645165ce0134378aa69e41d78d269d /generic/proof-script.el | |
| parent | 3292453208c2e2e20ff84ab7f90c7d52cd96afc2 (diff) | |
Prevent proof spans being duplicated.
Diffstat (limited to 'generic/proof-script.el')
| -rw-r--r-- | generic/proof-script.el | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/generic/proof-script.el b/generic/proof-script.el index 56df3624..75381b38 100644 --- a/generic/proof-script.el +++ b/generic/proof-script.el @@ -503,6 +503,8 @@ NAME does not need to be unique." (set-span-property span 'name name) (set-span-property span 'span-delete-action delfn) (set-span-property span 'invisible visname) + ;; Bad behaviour if span gets copied: unique ID shouldn't be duplicated. + (set-span-property span 'duplicable nil) ;; Nice behaviour in with isearch: open invisible regions temporarily. (set-span-property span 'isearch-open-invisible 'pg-open-invisible-span) @@ -585,7 +587,6 @@ NAME does not need to be unique." (set-span-property span 'controlspan controlspan) (set-span-property controlspan 'children (cons span (span-property controlspan 'children))) - (set-span-property span 'duplicable t) ;; (set-span-property span 'context-menu (pg-proof-element-menu name)) (pg-set-span-helphighlights span 'nohighlight) (if proof-disappearing-proofs |