Re: [isabelle] Incomplete goal may cause proof methods of later goals to loop.



On 23.04.2014 05:27, Yannick Duchêne (Hibou57) 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.
This is the classic way of Proof General, which also was the main
Isabelle UI till ~3 years ago.
>
> 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).
In 2013-2, this is bound to C+e ENTER.

BTW, there are many actions in the Isabelle plugin which can be
potentially bound to a shortcut, but aren't by default. To see them, go to

   Utilities / Global Options / jEdit / Shortcuts

and select "Plugin: Isabelle" in the "Edit Shortcuts" dropdown.

  -- Lars




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