I certainly agree, sometimes that is exactly what you want to do. Another idea is to implement sledgehammer a pop-up window tied to a particular place, which eventually will receive sledgehammer's result. Then you could continue editing the document freely, without interfering with the sledgehammer execution.
Larry On 14 Feb 2013, at 17:34, Peter Lammich <[email protected]> wrote: > On Do, 2013-02-14 at 17:22 +0000, Lawrence Paulson wrote: >> In a dream scenario, one might imagine opening a document containing a >> number of occurrences of "sorry", and each one of these occurrences would be >> given to counterexample finders and to sledgehammer, without any specific >> user intervention. Then somehow any counterexamples or proofs that were >> found would be noted somehow, and the user could inspect these. >> >> I recognise this idea isn't even half baked. But I know that you want to >> look at these problems differently from just saying, "how did it work in >> Proof General"? And the idea of having a whole bunch of gaps checked (as it >> were) simultaneously is very appealing. >> > > But both in jEdit and PG, there is one "gap" that the user is currently > interested in most, and that's the proof he's currently editing viz. the > lemma he has just typed. Unlike the document model of Isabelle/jEdit, > the user that develops a theory file only works at one place in the file > at the same time, and pays special interest to this place. > As a user who just typed in/altered a lemma, I'm interested in a > counter-example for that lemma --- without needing to type quickcheck, > sledgehammer, or sorry first (I usually want to type proof, by, or apply > there). > > > -- > Peter > > _______________________________________________ > isabelle-dev mailing list > [email protected] > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev _______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
