Re: Formatter questions
Josef Urban <[email protected]>
| Newsgroups | gmane.comp.mathematics.mizar |
|---|---|
| Message-ID | <[email protected]> |
On 5/12/10, Josef Urban <[email protected]> wrote: > 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. For the xml-ized files, you can get some basic information by looking up their top element at http://mizar.uwb.edu.pl/version/current/doc/xml/Mizar.html, e.g.: http://mizar.uwb.edu.pl/version/current/doc/xml/Mizar.html#Constructors Josef > >> 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? >> >