I agree with you, and it seems a mistake to expect jEdit to do all kinds of things that could very easily be done otherwise.
Larry On 14 Mar 2013, at 07:57, David Greenaway <david.greena...@nicta.com.au> wrote: > > On 08/03/13 23:46, Joachim Breitner wrote: >> Sometimes, when I’m writing apply-script style proofs, I have wanted >> a way to modify a proof method foo to “Try foo on the first goal. If >> it solves the goal, good, if it does not solve it, fail”. > [...] >> I wanted to see if I could implement such a feature myself and came up >> with the attached patch – maybe it is already sufficient? > > Sorry to raise this thread again, but what was the outcome of this > patch? > > Was the general concept of a "solve" tactical rejected, or just the > particular choice of syntax / implementation? (If so, how could it be > improved?) Or have the core developers just been busy? (I apologise if > so!) > > I know that the conversion moved on how jEdit might additionally assist > users in determining where a proof script became broken, but I didn't > come to understand why this simple patch would be mutually exclusive to > other more elaborate options. > > Cheers, > David > > > ________________________________ > > The information in this e-mail may be confidential and subject to legal > professional privilege and/or copyright. National ICT Australia Limited > accepts no liability for any damage caused by this email or its attachments. > _______________________________________________ > isabelle-dev mailing list > isabelle-...@in.tum.de > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
