Re: [PG-devel] PG and Coq ideslave mode

That sounds right (but could lead to confusion!). What I did was to fork a version of PG and cut it down to something fairly minimal. - D. On 06/05/2016 14:34, Paul A. Steckler wrote: The proof-shell mode comes with a lot of associated state, like regexps, buffers, etc. Some bits of that

Re: [PG-devel] PG and Coq ideslave mode

On 2016-05-06 09:34, Paul A. Steckler wrote: > If I load two .v files in emacs, it seems I can only work on one at a > time using Proof General, and there's only one proof-shell mode window > active. That's correct. signature.asc Description: OpenPGP digital signature

Re: [PG-devel] PG and Coq ideslave mode

The proof-shell mode comes with a lot of associated state, like regexps, buffers, etc. Some bits of that state would be useful in the new mode I'm creating, others not. I'm thinking that I can share the same state variables for the new mode, because I'll never have an active proof shell mode and

Re: [PG-devel] PG and Coq ideslave mode

I did something like this once to support PGIP, which was a sort of pre-cursor of PIDE based on exchanging XML messages. You can find the source in the CVS repo PG Kit repo (Kit/src/pgemacs). But it probably isn't useful: it's about 10 years old and the case we wanted to allow was input coming

Re: [PG-devel] PG and Coq ideslave mode

Proof General defines a shell mode, proof-shell, and an associated message filter. My thought now is to define an alternate-universe shell mode, proof-shell-noprompt and an associated message filter. -- Paul On Fri, May 6, 2016 at 1:27 AM, Pierre Courtieu wrote: > I

[PG-devel] Last Call for Papers: Workshop on User Interfaces for Theorem Provers (UITP 2016 @ IJCAR), Coimbra, Portugal, Deadline May 17th *NEW* (was May 9th, 2016)

Subject: [Stp] Last Call for Papers: Workshop on User Interfaces for Theorem Provers (UITP 2016 @ IJCAR), Coimbra, Portugal, Deadline May 17th *NEW* (was May 9th, 2016) Date: Fri, 6 May 2016 06:40:13 + From: Grov, Gudmund To: s...@macs.hw.ac.uk ,