Re: [mizar] vocabularies

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

On Wed, 7 Jan 2009, trybulec wrote:

> Freek Wiedijk wrote:
>
> > Of course you could also have a _separate_ tool that would
> > find all theorems used by your article, and then update the
> > article if necessary, by adding missing references to the
> > theorems directive.
> OK with me. You have to write new SCANNER.  If SCANNER would pass the token 
> as the file name,
> then action for PARSER is clear: take the spelling and write in on a file or 
> somewhere.

something like:
perl -e 'local $/;$_=<>; s/::.*//g; while(m/\sby\s([^;]*);/g) {@a=$1=~m/[\s,](\w*)\s*:/g; @h{@a}=()} print join(",", sort keys %h),"\n"' foo.miz

> > So having a tool that messes with your article (if only with
> > the environment) sounds a bit scary, but error messages
> > are inserted in the article as well, so it's not a very
> > big change.
> Error messages are comments, they are pruned anyway.

Automated creation of skeletons in Emacs messes the article a lot (making 
some people quite happy). It silently uses a modified Mizar parser 
(lisppars) for parsing the article into Lisp-friendly notation. An 
additional "pass" that nobody knows about :-). But I think the above Perl 
hack does the job in this case.

Josef