Re: [PG-devel] State button for Coq, needed?

OK, I've left the State button in, and it's working with the XML protocol. I moved it over a few positions, so that the new Check button is always visible. Thanks for all the feedback. -- Paul On Tue, Aug 9, 2016 at 3:58 AM, Hendrik Tews wrote: > Hi, > > "Paul A.

Re: [PG-devel] State button for Coq, needed?

Hi, "Paul A. Steckler" writes: > Well, the current goal should always be shown, unless there's a bug. What if the user deletes the emacs window containing the current goal because he temporarily wants to use that screen space for something else? I used to do this quite

[PG-devel] State button for Coq, needed?

I've made some fair headway in getting Proof General working with the coqtop XMLish protocol. So now I'm working on some of the less-central bits for that port. There's a PG button, State, which in the REPL version of PG, sends "Show." to coqtop to request the current goal. I'm thinking this