Skip to content

Use temp buffer for XML parsing #341

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
wants to merge 1 commit into
base: async
Choose a base branch
from
Open

Use temp buffer for XML parsing #341

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
49 changes: 24 additions & 25 deletions coq/coq-server.el
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1011,37 +1011,36 @@ after closing focus")
(defun coq-server--xml-parse (response call span)
;; claimed invariant: response is well-formed XML
(when response
(insert response)
(coq-xml-unescape-buffer)
(setq coq-server--current-call call)
(setq coq-server--current-span span)
(let ((xml (coq-xml-get-next-xml)))
(run-hook-with-args coq-server-response-hook xml)
(pcase (coq-xml-tag xml)
;; feedbacks are most common, so put first here
(`feedback (coq-server--handle-feedback xml))
(`value (coq-server--handle-value xml span))
(`message (coq-server--handle-message xml))
(t (proof-debug-message "Unknown coqtop response %s" xml))))
(when (> (buffer-size) 0)
;; since current reponse invalid, don't send anything more
(coq-tq-flush coq-server-transaction-queue)
(message "*** Ill-formed XML:\n%s\n*** End of ill-formed XML" (buffer-string))
(erase-buffer)
(let ((warning "Warning: received ill-formed XML from Coq.")
(advice "Goto an earlier good point in the script to resync.")
(cmd "To help diagnose the issue, enable logging with \"M-x proof-server-enable-logging\"."))
(message-box "%s\n\n%s\n\n%s" warning advice cmd)))))
(with-temp-buffer
(insert response)
(coq-xml-unescape-buffer)
(setq coq-server--current-call call)
(setq coq-server--current-span span)
(let ((xml (coq-xml-get-next-xml)))
(run-hook-with-args coq-server-response-hook xml)
(pcase (coq-xml-tag xml)
;; feedbacks are most common, so put first here
(`feedback (coq-server--handle-feedback xml))
(`value (coq-server--handle-value xml span))
(`message (coq-server--handle-message xml))
(t (proof-debug-message "Unknown coqtop response %s" xml))))
(when (> (buffer-size) 0)
;; since current reponse invalid, don't send anything more
(coq-tq-flush coq-server-transaction-queue)
(message "*** Ill-formed XML:\n%s\n*** End of ill-formed XML" (buffer-string))
(erase-buffer)
(let ((warning "Warning: received ill-formed XML from Coq.")
(advice "Goto an earlier good point in the script to resync.")
(cmd "To help diagnose the issue, enable logging with \"M-x proof-server-enable-logging\"."))
(message-box "%s\n\n%s\n\n%s" warning advice cmd))))))

;; process XML response from Coq
(defun coq-server-process-response (response call span)
(with-current-buffer coq-xml-response-buffer
(coq-server--xml-parse response call span)))
(coq-server--xml-parse response call span))

;; process OOB response from Coq
(defun coq-server-process-oob (_closure oob call span)
(with-current-buffer coq-xml-oob-buffer
(coq-server--xml-parse oob call span)))
(coq-server--xml-parse oob call span))

(defun coq-server-handle-tq-response (special-processor response call span)
;; if there's a special processor, use that
Expand Down
11 changes: 0 additions & 11 deletions coq/coq-xml.el
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -399,17 +399,6 @@ to write out the traversal code by hand each time."
(insert s)
(libxml-parse-xml-region (point-min) (point-max))))

;; buffer for gluing coqtop responses into XML
;; leading space makes buffer invisible, for the most part
(defvar coq-xml--response-buffer-name " *coq-responses*")
(defvar coq-xml-response-buffer (get-buffer-create coq-xml--response-buffer-name))

;; buffer for gluing coqtop out-of-band responses into XML
;; this is separate from ordinary response buffer because these
;; OOB responses may occur while processing ordinary responses
(defvar coq-xml--oob-buffer-name " *coq-oob-responses*")
(defvar coq-xml-oob-buffer (get-buffer-create coq-xml--oob-buffer-name))

;;; functions for XML received from coqtop
;;; these assume that current-buffer is a response buffer
;;; though not the *response* buffer seen by user
Expand Down