Re: [isabelle-dev] Feedback from a Isabelle tutorial
On Sat, 25 Jun 2011, Clemens Ballarin wrote: Quoting Makarius : In principle everything is possible, but one needs to try hard to minimize "options" and "features". Otherwise it becomes impossible to maintain robustness of the application. There are no proper automated test procedures, which means I usually play through all the important things manually (on 3 platform families). Java provides support for GUI tests through a Robot class, and there are frameworks out there since everybode has this problem. It'll sure be worth investigating automatic testing (student project?). I have heard of such things before, but have not tried anything so far. After a few years working with JVM frameworks I no longer take anything for granted by default. It always requires a lot of extra work to make things work more than half way. What did these people do in all these years with all the ? Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Feedback from a Isabelle tutorial
Quoting Makarius : In principle everything is possible, but one needs to try hard to minimize "options" and "features". Otherwise it becomes impossible to maintain robustness of the application. There are no proper automated test procedures, which means I usually play through all the important things manually (on 3 platform families). Java provides support for GUI tests through a Robot class, and there are frameworks out there since everybode has this problem. It'll sure be worth investigating automatic testing (student project?). Clemens ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Feedback from a Isabelle tutorial
On Sat, 25 Jun 2011, Lawrence Paulson wrote: Is it possible to restrict command completion to a select collection of commonly used commands? Or to make it the user-configurable? Larry On 24 Jun 2011, at 21:01, Alexander Krauss wrote: Suggestion: Simply kill completion of commands (not symbols)??? In principle everything is possible, but one needs to try hard to minimize "options" and "features". Otherwise it becomes impossible to maintain robustness of the application. There are no proper automated test procedures, which means I usually play through all the important things manually (on 3 platform families). I have already spent a lot of time looking through the existing mechanisms of Java, Swing, jEdit, and make as much sense of it as is feasible at the moment. This needs to continue, of course. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Feedback from a Isabelle tutorial
Is it possible to restrict command completion to a select collection of commonly used commands? Or to make it the user-configurable? Larry On 24 Jun 2011, at 21:01, Alexander Krauss wrote: > Suggestion: Simply kill completion of commands (not symbols)??? ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Feedback from a Isabelle tutorial
On Fri, 24 Jun 2011, Alexander Krauss wrote: Another instance, which comes up in an exploratory/teaching context, is the following scenario: lemma "x = y"-- some false conjecture try -- see if it "works" ^ -> counterexample found immediately cursor is here At this point I would like to go up and correct the lemma, but I cannot, since the editor suggests "try_methods" as a completion of "try". I have to press escape first. Of course, in an ideal world, I would not have to type "try" in the first place, but currently this is our way of working. Suggestion: Simply kill completion of commands (not symbols)??? The inlining of diagnostic commands into the text is awkward in several ways. There should be a completely different way to do it, without intruding the text area in the first place. In general the command language is designed to have completion of some form. This explains the relatively long and explicit command names, e.g. "definition", "theorem" instead of cryptic abbreviations. The physical mechanism to be used is a different question. jEdit alone has about 5 such mechanisms as part of the main editor framework or plugins, and in the greater Java/Swing world there are some more such frameworks. What you see right now is the builtin auto-completion of jEdit/Sidekick. The regular jEdit completion/abbreviation mechanism needs to be requested explicitly by certain command sequences, and it is not configured by default. One needs to make a market survey to find really good mechanisms that do not intrude the editing process (as in newer Proof General versions, for example). Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
