This will be very useful for quite a few users, in particular those
willing to interact with Coq from an editor context.
Things integrate pretty well, and petanque can demand Flèche to
build documents, etc...
Note that we can still improve the codebase a bit, in particular:
we should share the generic handling code between controller and
petanque.
note also the lack of uniformity w.r.t. the cancellation token and
Rq.serve, in particular Rq.Immediate and Rq.query with result
Now should do the same.
This will be very useful for quite a few users, in particular those willing to interact with Coq from an editor context.
Things integrate pretty well, and
petanque
can demandFlèche
to build documents, etc...Note that we can still improve the codebase a bit, in particular:
we should share the generic handling code between
controller
andpetanque
.note also the lack of uniformity w.r.t. the cancellation token and Rq.serve, in particular
Rq.Immediate
andRq.query
with resultNow
should do the same.