On 08/12/10 16:47, Pierre Courtieu wrote: > David, I am not sure coq-shell-insert-hook is the good entry point for > this kind of things. Is it?
I cannot find coq-shell-insert-hook. Did you mean proof-shell-insert-hook? > A command "Require f" is about to be sent to coq, but *before that* we > want to perform the following: > 1) send "Locate Library f" > 2) wait for the answer of coq: "path/to/f" . > 3) send "make -C ... path/to/f.vo" > 4) wait until make finished its job > 5) finally send the "Require f" to coq if everything went well (error > otherwise). If it is not possible to communicate with the prover from within proof-shell-insert-hook, then I consider the following approach: - when commands are added to proof-action-list I insert a special command before every "Require" command. The special command is "Locate Library" with a special callback. - The special callback has the task to analyze the answer of coq to the "Locate Library" command and to start the recompilation process. - This can only work if the following "Require" command is _not_ sent to the prover before the special callback has finished its task. In order to achieve this one has to modify proof-shell-exec-loop, to run some callbacks before sending the next input to the prover. The special commands that are inserted in proof-action-list do not directly represent any source code. Therefore they probably get an empty span. Will this cause any trouble? I briefly looked at how callbacks are called: They get the span as argument, but not the prover output. The documentation says that the prover output is available in the variable proof-shell-last-output. Will this contain only the output from the last command, or can it happen, that it contains the output from, say, the last three commands? Bye, Hendrik _______________________________________________ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
