I think you just want two (well four, with the control channel) `make-network-process'es, actually :)
You can `cl-define-struct' a pair of network process (and possibly wrap relevant function to work on pairs of half-channels) for convenience, too. Interestingly, you probably don't need a filter function on the two Emacs-> Coq ones. Clément. On 2016-05-11 10:09, Paul A. Steckler wrote: > You're comparing make-network-process, then, with start-process? > > When using sockets, coqtop works in a funny way, using two half-duplex > sockets. So if you used make-network-process, I think you'd get just > one of those sockets, and have to use Elisp's other network facilities > to manage the other socket, ugh. That reinforces the idea that pipes > would be the way to go. > > There are also the "command channels" used by coqtop. I think those > would have to be manually-managed network sockets. > > -- Paul > > > > On Wed, May 11, 2016 at 3:40 PM, Stefan Monnier > <monn...@iro.umontreal.ca> wrote: >>> You mean here the pipes that are created when running Elisp's start-process? >> >> Yes. In either case, the Elisp code will start Coq and get a an Elisp >> process object in return. This is the only part that should >> be different. After that, whether you're using a pipe or a socket won't >> affect your Elisp code. >> >>> It looks like you'd setup a filter function for the Coq process to get >>> its output, and use process-send-string to send input to Coq. >> >> Yes, and that applies to either case. >> >> >> Stefan > _______________________________________________ > ProofGeneral-devel mailing list > ProofGeneral-devel@inf.ed.ac.uk > http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel >
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
