diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2002-08-16 08:07:56 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2002-08-16 08:07:56 +0000 |
| commit | 0d61475511fbe98406991e41bd010087d8157777 (patch) | |
| tree | 16ef98179a77bf5432630b2705d37d933102cc32 /generic | |
| parent | b3a843523cad3e71113a8ac11eaa1e3b5edb4f8c (diff) | |
pg-goals -> pg-assoc
Diffstat (limited to 'generic')
| -rw-r--r-- | generic/pg-user.el | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/generic/pg-user.el b/generic/pg-user.el index 42f1e78b..1a94a52d 100644 --- a/generic/pg-user.el +++ b/generic/pg-user.el @@ -672,7 +672,7 @@ last use time, to discourage saving these into the users database." (pg-insert-output-as-comment-fn proof-shell-last-output) ;; Otherwise the default behaviour is to use comment-region (let ((beg (point)) end) - ;; pg-goals-strip-subterm-markup: should be done + ;; pg-assoc-strip-subterm-markup: should be done ;; for us in proof-fontify-region (insert proof-shell-last-output) ;; 3.4: add fontification. Questionable since comments will @@ -932,7 +932,9 @@ If NUM is negative, move upwards. Return new span." (pg-numth-span-higher-or-lower (pg-control-span-of span) 1 'noerr)))) (if (and proof-experimental-features proof-shell-theorem-dependency-list-regexp) - (proof-dependency-in-span-context-menu span)))) + (proof-dependency-in-span-context-menu span)) + (if proof-script-span-context-menu-extensions + (funcall proof-script-span-context-menu-extensions span idiom name)))) |