Re: [isabelle] Automating the auto-tools



On Sat, 21 Jul 2012, Gottfried Barrow wrote:

I guess the general rule is that if some code can be seen in a jEdit view, then the continuous prover will work on the file up to that point.

To belabor the point, I suppose if I had 10 jEdit views open of 10 different .thy files, the continuous prover would try to work on all of them up to the code that could be seen in each view.

Yes. It also means that a lot of editor views on different spots in some library can cost a lot of performance for continous checking.

You can also control the range of checking a little bit: the Prover Session panel has a "Check" button, which tells to prover to check the whole of the current buffer, until you "Cancel" or recommence normal editing.


	Makarius





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