On 2016-05-07 13:44, Paul A. Steckler wrote:
> OK, you'll need to explain the binding between plug-ins and PG to me.

I think this connects to my previous email. Company-coq uses PG as an interface 
to Coq (thus very little in it depends on how PG communicates with Coq, and I 
could fix anything that does: it only depends on the interface that PG 
exposes). In terms of functions, the only ones that it uses from PG itself are 

  (fun proof-shell-invisible-command "ext:proof-shell.el" cmd)
  (fun proof-shell-available-p "ext:proof-shell.el")
  (fun proof-shell-live-buffer "ext:proof-shell.el")
  (fun proof-shell-ready-prover "ext:proof-shell.el")
  (fun proof-unprocessed-begin "ext:proof-script.el")
  (fun proof-goto-point "ext:pg-user.el")

Attachment: signature.asc
Description: OpenPGP digital signature

ProofGeneral-devel mailing list

Reply via email to