Hi Michael,
Why I am interested in it: I have written a converter from syntax.txt to XML-file in order to get better understanding Mizar grammar.there is no automated (e.g. bison-like) connection between them and the Mizar parser.I thougt about using Elkhound (GLR parsing) http://www.cs.berkeley.edu/~smcpeak/elkhound or implementation GLR in OCaml but for now my simple toy parser (in Ocaml) is coded by hand.
Trying to reverse-engineer the Mizar parser is a bit dangerous - see e.g.http://mizar.uwb.edu.pl/forum/archive/0208/msg00043.html, http://www.uclic.ucl.ac.uk/usr/jgow/papers/parsing.ps.gz, and http://www.uclic.ucl.ac.uk/people/j.gow/papers/alcor-jar.pdf .
If you just want to parse Mizar in order to do some research about MML, it may be much more convenient to use the XML files produced by the Mizar parser itself. The currently distributed version can be processed to look like this: http://lipa.ms.mff.cuni.cz/~urban/xmlmml/html_abstr.4.67.942/card_1.html, and in the latest addition (not yet distributed) most identifiers can be reconstructed - prototype is at http://lipa.ms.mff.cuni.cz/~urban/xmlmml/html_abstr.4.67.942/00osalg_4.html.
On the other hand, I also think that having Mizar rewritten in a high-level language like OCaml would be useful. Btw., Andrzej Trybulec wrote me a month ago that "he agrees that Mizar should be open-source", so I hope it will happen soon and make such reimplementations easier.
Josef