Re: [mizar] Re: Mizar Parser

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

On Thu, 1 Aug 2002, Grzegorz Bancerek wrote:

> In lastest versions of mizarmode (see "mizar.el" in Mizar disrtibution)
> in Mizar menu|Constr. Explanation | Verbosity  mark constructors list.
> After Run Mizar you will have places (near "by" or ";") to click.
> It is better to mark also 
>   Mizar menu|Constr. Explanation | Underline explanation points
> Then you may click them shift+mouse-2 

Actually, I think it is now shift-mouse-3 (it used to be just mouse-2, but 
I accepted prof. Rudnicky's objection about the binding, (and I will 
probably also rebind shift-mouse-2 to its original hideshow meaning)).
The translation still fails for clusters not imported from MML (i.e. 
defined in the processed article), as that information is not saved in any 
temporary file (another temporary file for Freek :-).

Josef