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 these: (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")
signature.asc
Description: OpenPGP digital signature
_______________________________________________ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
