Re: [mizar] Re: Mizar Parser

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

On Thu, 1 Aug 2002, Grzegorz Bancerek wrote:

> Grzegorz Bancerek wrote:

> I was deceived by mizarmode ;-) which writes "No more errors!!"
> if the cursor is in far position.

The "error movement" of cursor after verification can be set in the menu 
"Show error", default is "next", which means going to the first error 
after cursor (and really results in "No more errors!!" message if the 
cursor is after the last error). I can fix the goto-error functions, not 
to give the message if called in the verifing ("mizar-it") function, but I 
do not know whether the users want it or not (in some cases, the message 
can be useful, and you have the output window anyway). 

Josef