Re: vocabullaries
Freek Wiedijk <[email protected]>
| Newsgroups | gmane.comp.mathematics.mizar |
|---|---|
| Message-ID | <[email protected]> |
Hi Adam, >I think the 'vocabulary' (in singular) part would >only be used when writing the article - after submission >it could be transferred into mml.vct and removed from >the article. Why remove it? It shouldn't hurt to keep the article intact. Of course you also should have the mml.vct file. But it can be a _copy,_ can it? I like the idea that if somewhere on an old disk you would find an old mml directory full of *.miz files, that it would be self-contained. I even think I would like the vocabulary to also be part of the .abs files. >This procedure, however, would require importing (by >default) a vocabulary named like the processed article, >provided it exists in mml.vct. Keeping that part in the >article seems useles as it's easier to use findvoc/listvoc >to check the contents of a vocaulary rather than searching >*.miz files. Again, you can easily have it in _both_ places. I like the idea that you can easily see the article together with its vocabulary, even if it's "frozen" in the MML. >One minor disadvantage of keeping *.mi and *.voc as one >file would be when working with a local library - at the >moment several articles can share a local vocabulary and >the change would require copying the 'vocabulary' stuff >into several files. I don't know about implementation issues, but doesn't it seem natural to just have the name of one of them in the "vocabulary" directive of the others? To make that work you would need to generate a "local" version of mml.vct to supplement the real mml.vct when running miz2prel. I guess. Freek