Re: [isabelle] Incomplete goal may cause proof methods of later goals to loop.
You seem to be describing Proof General, which is still available for Isabelle, but no longer supported.
We have to live with the problems of a radically new interaction paradigm that’s still being fleshed out. Maple, for example, offers a superficially similar document model, but you can’t tell whether what you are looking at has been evaluated or not, and even Maple itself doesn’t seem to know. That approach is efficient but has many of its own limitations.
On 23 Apr 2014, at 04:27, Yannick Duchêne (Hibou57) <yannick_duchene at yahoo.fr> wrote:
> I remember Coq has a different way to handle this: there are explicit forward and backward (in proof state) commands. The processed part of a proof is not editable and one have to go backward to edit it, then go forward again and resume up to the last proof statement. This is sometime tedious, while clean.
> That's a way too much different compared to what Isabelle users are accustomed to. Personally, it happens I think about the Coq way when I feel Isabelle process too much of invalid text during editing, while in other cases, I enjoy the reactivity of feedback from Isabelle while editing.
> May be an idea could be to have a keystroke to quickly enable/disable “Continuous checking”… a keystroke, so that this would remain handy while editing: no need to leave the keyboard to go from and to the mouse to check/uncheck the option and no need to have the theories panel always visible (otherwise needed, as the option is located on this panel).
This archive was generated by a fusion of
Pipermail (Mailman edition) and