diff options
| author | David Aspinall | 2001-08-16 15:04:40 +0000 |
|---|---|---|
| committer | David Aspinall | 2001-08-16 15:04:40 +0000 |
| commit | c7b93282ee36fdee6a4792d1b665eb454035a2cc (patch) | |
| tree | 0c92622ad945bbdcc8b7d048fcfcb7b3c43ea346 /generic | |
| parent | a36632b4ca2e6dcc2831431982512fd3820b49b6 (diff) | |
Switch back to using goalsave spans in PBP code
Diffstat (limited to 'generic')
| -rw-r--r-- | generic/proof-shell.el | 11 |
1 files changed, 7 insertions, 4 deletions
diff --git a/generic/proof-shell.el b/generic/proof-shell.el index afe3d938..94bee243 100644 --- a/generic/proof-shell.el +++ b/generic/proof-shell.el @@ -464,7 +464,10 @@ explicit yank." (save-window-excursion (save-excursion (mouse-set-point event) - (setq span (span-at (point) 'proof)) + ;; Get either the proof body or whole goalsave + (setq span (or + (span-at (point) 'proof)) + (span-at (point) 'goalsave)) (if span (copy-region-as-kill (span-start span) (span-end span))))) @@ -504,7 +507,7 @@ user types by hand." (apply 'concat (nreverse ls)))) (defun pbp-construct-command () - (let* ((span (span-at (point) 'proof)) + (let* ((span (span-at (point) 'goalsave)) (top-span (span-at (point) 'proof-top-element)) top-info) (if (null top-span) () @@ -516,7 +519,7 @@ user types by hand." (format (if (eq 'hyp (car top-info)) pbp-hyp-command pbp-goal-command) (concat (cdr top-info) (proof-expand-path - (span-property span 'proof)))))) + (span-property span 'goalsave)))))) ((eq (car top-info) 'hyp) (proof-shell-invisible-command (format pbp-hyp-command (cdr top-info)))) @@ -701,7 +704,7 @@ extents." ;; lego/example.l and FSF GNU Emacs 20.3 (setq span (make-span (car stack) op)) (set-span-property span 'mouse-face 'highlight) - (set-span-property span 'proof (car (cdr stack))) + (set-span-property span 'goalsave (car (cdr stack)));; FIXME: really goalsave? ;; Pop annotation off stack (and proof-analyse-using-stack (progn |