I've already mentioned the issue described below to Clément Pit-Claudel and Pierre Courtieu, maybe others on this list have thoughts on it.
Proof General is welded to a model of receiving prompts from a prover. After it's received a prompt, PG can send something back to the prover. The ideslave (politically incorrectly-named) mode in Coq, developed for CoqIDE abandons that model. In that mode, Coq just waits for XML from an IDE, without first offering a prompt. In ideslave mode, it seems that Coq sends back responses wrapped in <value> tags, so you can use that as a pseudo-prompt. Hmm, I think the prompt regexp would have to look for both the closing tag, and the single-tag version, <value ... />. Even with that, there's still a bootstrapping issue, because there's no prompt to s start with. I could probably modify PG to not look for that first prompt. Is there some good way to handle this? -- Paul _______________________________________________ ProofGeneral-devel mailing list ProofGeneral-devel@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
