From c7a0cca56311b8a5bd64e672b350ae587e4fc950 Mon Sep 17 00:00:00 2001 From: Paul Steckler Date: Tue, 4 Oct 2016 12:00:41 -0400 Subject: [PATCH] process all bg goal pairs, issue #35 --- coq/coq-server.el | 23 ++++++++++++++--------- 1 file changed, 14 insertions(+), 9 deletions(-) diff --git a/coq/coq-server.el b/coq/coq-server.el index d3a1412c8..052a66e33 100644 --- a/coq/coq-server.el +++ b/coq/coq-server.el @@ -14,6 +14,7 @@ (require 'coq-tq) (require 'coq-response) (require 'coq-xml) +; (require 'coq-header-line) (defvar coq-server--pending-edit-at-state-id nil "State id for an Edit_at command sent, until we get a response.") @@ -223,13 +224,12 @@ is gone and we have to close the secondary locked span." (let* ((all-goals (coq-xml-body (coq-xml-at-path xml '(value (option (goals)))))) (current-goals (coq-xml-body (nth 0 all-goals))) ;; background goals have a different, extra structure than the other ones - ;; TODO: what to do with the extra information? - (bg-goals-pair (coq-xml-body1 (nth 1 all-goals))) - (bg-goals (coq-xml-body (nth 1 (coq-xml-body bg-goals-pair)))) + (bg-goals-pairs (coq-xml-body (nth 1 all-goals))) + (bg-goals nil) ; to be extracted from bg-goals-pairs (shelved-goals (coq-xml-body (nth 2 all-goals))) (abandoned-goals (coq-xml-body (nth 3 all-goals))) goal-text) - (if (not (or current-goals bg-goals shelved-goals abandoned-goals)) + (if (not (or current-goals bg-goals-pairs shelved-goals abandoned-goals)) (progn ;; clear goals display (coq-server--clear-goals-buffer) @@ -243,9 +243,13 @@ is gone and we have to close the secondary locked span." (dolist (goal shelved-goals) (coq-server--handle-goal goal)) (setq goal-text (cons (coq-server--make-goals-string shelved-goals t 'Shelved) goal-text))) - (when bg-goals - (dolist (goal bg-goals) - (coq-server--handle-goal goal)) + (when bg-goals-pairs + (dolist (pair bg-goals-pairs) + ;; TODO : what is first elt of pair? + (let* ((pair-goal-list (nth 1 (coq-xml-body pair))) + (pair-goals (coq-xml-body pair-goal-list))) + (mapc 'coq-server--handle-goal pair-goals) + (setq bg-goals (append bg-goals pair-goals)))) (setq goal-text (cons (coq-server--make-goals-string bg-goals t 'Unfocused) goal-text))) (when current-goals (progn @@ -786,7 +790,6 @@ is gone and we have to close the secondary locked span." ;; if there's an existing colored span at point, re-use it, ;; because want most recent coloring (let ((span-processing (span-make (point) (span-end span-with-state-id)))) - ;; TODO 'type becomes 'pg-type when merged with trunk (span-set-property span-processing 'type 'pg-special-coloring) (span-set-property span-processing prop 't) (span-set-property span-processing 'face face) @@ -892,7 +895,9 @@ is gone and we have to close the secondary locked span." (`feedback (coq-server--handle-feedback xml)) (`message (coq-server--handle-message xml)) (t (proof-debug-message "Unknown coqtop response %s" xml))) - (setq xml (coq-xml-get-next-xml))))) + (setq xml (coq-xml-get-next-xml)))) + ;; (coq-header-line-update) + ) ;; process XML response from Coq (defun coq-server-process-response (response call span)