Re: vocabularies

On Tue, 6 Jan 2009, trybulec wrote:

> Piotr Rudnicki wrote:
>
>> <>On Mon, Jan 05, 2009 at 07:48:58PM +0100, Freek Wiedijk wrote:
>> 
>> I support Freek. Is the extra pass even needed? Can the import
>> of theorems be done on the fly?
>> 
>> On the other hand, it is interesting what was the past motivation for
>> introducing the theorems directive. (With the schemes directive the
>> story is different).
>> 
> You should remember. A mispelling of a reference to a theorem more often 
> happens than
> the need of adding  the name of theorems file to the 'theorems' directive.

Side note: If you use Emacs, use Alt-/ for dynamic completion of such 
identifiers. For example, if you want to write "SQUARE_1", and have 
"SQUARE_1" already in the environment, then only type "SQ" or "SQU" and 
then press ALT-/ to complete. If there is no dynamic completion, something 
is wrong (you mistyped or the identifier is nowhere in the article yet).

One possible additional check (in Emacs) would be to watch if the added 
identifiers are in mml.lar or the current environment after entering 
"by.*;" . Probably not a big deal.

Provided that (using such mechanisms) you will never mistype here, Freek's 
complaint wins (I think his problem is fairly frequent too). But Freek's 
complaint can be also dealt with automagically in Emacs :-) (i.e. the 
environment directive appended).

> Maybe more important is that you should first run PARSER (for the Text 
> Proper), to generate
> a file for the ACCOMMODATOR (maybe incorrect) and then to run the VERIFIER. 
> Clumsy.

Just one more pass in a multipass compiler :-). If white char is strictly 
required before and after "by" and "from" (I am not sure now), then a very 
cheap pass. But I would do a check against mml.lar (plus local db) before 
running accommodator, and complain if there is a typo instead of 
accommodating.

Josef