Re: Formatter questions

Josef Urban <[email protected]>
Newsgroups gmane.comp.mathematics.mizar
Message-ID <[email protected]>
Hi Daniel,

On 5/11/10, Daniel Matichuk <[email protected]> wrote:
> I have a few questions about Mizar with regards to the formatter that I'm
> working on:
>
> 1) Is there a comprehensive list of the meanings of all the intermediate
> files that are generated for an article?

Probably not.

> I have some vague ideas like "parx"
> seems to be related to tokenization, but really I'd like a list of what each
> of these is for.

.parx is a very new thing - an attempt to gradually xml-ize the
Parser's output. It is a moving target and probably should not be
relied upon in its current state.

>
> 2) Related to 1), is there an intermediate file that is an abstract syntax
> tree,

To various degree the .par and .xml files.

Best,
Josef

> or is it possible to have Mizar generate and abstract syntax tree for
> an article? Ideally for formatting you'd just like an AST annotated with
> identifiers.
>
> 3) Is the grammar posted at
> http://mizar.uwb.edu.pl/version/current/doc/syntax.txt up-to-date?
>
lmpx.com only provides a reader for public news (NNTP) servers. It is not affiliated with the servers or forums shown here and is not responsible for the content of articles, which is written by their respective authors.