On Tue, 6 Jan 2009, trybulec wrote:
Piotr Rudnicki wrote:You should remember. A mispelling of a reference to a theorem more often happens than<>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).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