Re: [mizar] Errors recovery

[Josef Urban <urban@ktilinux.ms.mff.cuni.cz>]

Hi,

On Sun, 8 Feb 2004, Piotr Rudnicki wrote:

> I propose that there is a standard macro
> in Mizar distribution that 
> 
> 	- stops after finding parsing errors (at least 1 and no more than say 10),  
> 	- stops after the analyzer if there were any errors.

That should be options to verifier, something like
verifier -P10 -A1 -C30 blah.miz .

It could be done even now in Emacs by watching the verifier's output, but 
it would be quite clumsy - having the options is simpler.

Best,
Josef