[mizar] Environment Declaration

[Andrzej Trybulec <trybulec@asuka.cs.shinshu-u.ac.jp>]

I have changed the subject because most of the messages with the subject 
"local DB" have nothing to do with local DB.

Josef Urban wrote:

> Actually one thing that is a bit similar to the "theorems" solution 
> would be to try to automatically construct the "vocabularies" 
> directive from available "notations". The problem with that is that 
> the parser now really needs to know the set of "symbols" beforehand 
> (also for the notation newly defined in the article). Question is, 
> whether that again could not be replaced by some initial shallow scan 
> (possibly with some small syntax modification, making such scan 
> easier). I wonder how much is it actually used in current MML to "cut 
> off" some notation because its symbol is not mentioned in the 
> "vocabularies" (and how easy would it be to fix such situations). Then 
> only "notations","constructors","registrations" and "definitions" 
> would remain.

I do not know the statistics, probably some modification of ACCOM may be 
used to get it. It happened few times that I have got the error #830 
(nothing imported from notations not because constructors were missing 
in the environment but because the lack if an vocabulary. It was very 
confusing, I had kept adding the file names to the 'constructors' 
directive, but of course nothing changed. Eventually I make a discovery 
, oh probably a vocabulary needed. It is confusing because it is so rare.

Andrzej