diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2008-01-31 19:28:26 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2008-01-31 19:28:26 +0000 |
| commit | a3337953b7b77bb51f85ab9b5bdc2c2e0114044d (patch) | |
| tree | 284711d6c2d74a2a80f8d8cd414c11da98e90f37 /generic/pg-goals.el | |
| parent | b9f40e7b69a7df1751ad132179b4bc28e30b43a5 (diff) | |
Sendback commands from response buffer sent via assert-until-point, with ordinary span construction.
Diffstat (limited to 'generic/pg-goals.el')
| -rw-r--r-- | generic/pg-goals.el | 13 |
1 files changed, 8 insertions, 5 deletions
diff --git a/generic/pg-goals.el b/generic/pg-goals.el index c55c593f..60f122d1 100644 --- a/generic/pg-goals.el +++ b/generic/pg-goals.el @@ -225,8 +225,9 @@ user types by hand." "Examine the goals " (let* ((span (span-at (point) 'goalsave)) ;; goalsave means subgoal no/name (top-span (span-at (point) 'proof-top-element)) + (buf (current-buffer)) top-info) - (if (null top-span) () + (when top-span (setq top-info (span-property top-span 'proof-top-element)) (pop-to-buffer proof-script-buffer) (cond @@ -244,11 +245,13 @@ user types by hand." ;; A scripting command to change goal (proof-insert-pbp-command (format pg-goals-change-goal (cdr top-info)))) + ((and + ;; Literal command in one step, classic PBP protocol + (eq (car top-info) 'lit) + (equal buf proof-goals-buffer)) + (proof-insert-pbp-command (cdr top-info))) ((eq (car top-info) 'lit) - ;; A literal command to insert - (proof-insert-pbp-command (cdr top-info))))))) - - + (proof-insert-sendback-command (cdr top-info))))))) (defun pg-goals-get-subterm-help (spanorwin &optional obj pos) "Return a help string for subterm, called via 'help-echo property." |