Re: [isabelle] the sound of a sledgehammer



On Thu, 14 Feb 2013, Lawrence Paulson wrote:

The entire internal architecture supports this background execution, so it should be possible.

Which version of the architecture do you mean? Fabian Immler and myself rewrote most of it from scratch in 2008, to make it work without Unix process fork, and thus on Cygwin for the first time. Later Jasmin also rewrote it again.

All of that is for the TTY loop, though. It has to be re-integrated into the native Isabelle document model, and this is where I am stuck for several years for no particular technical reasons, just social ones.


	Makarius





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.