[Date Prev][Date Next] [Chronological] [Thread] [Top]

Re: [mizar] vocabularies

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. 


You could then add that to mizf at the start.  So mizf then
would be:

(1) run that tool
(2) continue with the current mizf


Better change the name. I would like to use old mizf


Maybe it's in some sense clumsy to do it like this, but
getting irritated now and again (in my case: quite often) by
having to change the theorems directive when in the middle
of working on my formalization is clumsy too.  (I have to
go to the environment, change stuff there, reflow the lines
if necessary to get under the 80 column limit, and then
somehow get back to where I was working.  It's distracting.
And, as I said, often I forget about the theorems directive,
and get irritated by the error message as well.)
I rather welcome an opportunity to rest, to do a routine job. Maybe I am too lazy. 


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.

Regards,
Andrzej