Re: [isabelle] Continuing with a proof after a failed 'done'



On 02/08/16 16:48, Lars Hupel wrote:
> Hi Andreas,
> 
>> Just insert a "sorry" after the failing "done" and you can go on.
> 
> of course, that's a possibility, but I don't understand why 'done' and
> 'by' behave differently there in the first place.

After so many years, PIDE document editing still lacks substructural
error-recovery.

The 'by' command is based on a special trick, using
Proof.future_terminal_proof: it pretends to be finished on the toplevel
and forks the actual work.

The 'sorry' and '\<proof>' commands always finish, imitating the same
behaviour.

All other proof commands just work sequentially on the surface.


Only recently, I have started to introduce some formal source structure
for indentation in the editor. More will come eventually, and error
handling in continuous checking should somehow participate.


	Makarius





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