Hi, I looked at proof-shell-insert-hook. Is there a way to send a command to the prover, capture the output and retract this one command from within proof-shell-insert-hook? The documentation says that additional prompts will confuse proofgeneral. So is there a way to interact with the prover from within proof-shell-insert-hook without confusing proofgeneral?
The background is that coq has its own load path for libraries (where a library is a compiled .v file). To find out which file needs to be checked for recompilation it would be easiest to ask coq with the Locate Library command. But this would require a synchronous communication with coq from within proof-shell-insert-hook when an Require command is detected. Using Locate Library would have the advantage that proofgeneral does not need to model coq's library finding functionality. Bye, Hendrik _______________________________________________ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
