Re: vocabularies
Josef Urban <[email protected]>
| Newsgroups | gmane.comp.mathematics.mizar |
|---|---|
| Message-ID | <[email protected]> |
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