[isabelle] Make quickcheck/nitpick/sledgehammer run in background in jEdit?




Dear all Isabelle users,


I am using Isabelle/HOL for teaching "formal development) and we rely a lot on nitpick/quickcheck for students to debug their specifications. Many of them use the jEdit interface... but I find it surprising for each nitpick/quickcheck to be blocking.

I have seen that there is a similar demand for sledgehammer...
Would it be possible to add nitpick/quickcheck on the same item of the TODO list? Or is it fundamentally different?

Thanks in advance,

Thomas
--
Thomas Genet
ISTIC/IRISA
Campus de Beaulieu, 35042 Rennes cedex, France
Tél: +33 (0) 2 99 84 73 44 E-mail: genet at irisa.fr
http://www.irisa.fr/celtique/genet




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