Hi Freek,
I think that I myself only will like the solution if it's "backward compatible". If I won't be able to write my terms the way I can now because the mechanism will be more restrictive, for me it won't be a good solution. In that case the solution will be worse than the problem.
I probably don't understand. You lose "backward compatibility" with each MML revision, and have to write terms/formulas/types differently. MML revision can (and does) restrict you every now and then in your notation, unless you do not use the revised part of MML. You said yourself that you are going to order the notation directives in the MML order (I quite agree with that), which means that _you_ are now making the existing mechanism more restrictive for yourself. And if you attempt with the current mechanisms to have "stability under merging of directives", then you'll end up with something even more restrictive.
Sometimes the users will probably end up with something like a "constructors missing" error,But now they will get exactly that same error too, at exactly the same moment in writing the formalization. So that is not a difference with the current situation.
Yes, that's why I also think that the "half-way automation" of this would be an improvement. One more argument against this could be that the accommodation will be triggered more often this way (when you temporarily remove/comment all references to theorems from some article, but don't really mean it in the long run). But I don't think this will cause any
visible slowdown.
I am not sure that there is a good separation between the header problems and the overloading problems.Of course there is separation! Of my three requests, only the second one seems to have some interaction with your overloading doubts (because it's not clear how the different notations imports flow together). The "everything" proposal and the "theorems" proposal are not _at all_ unclear because of the strangeness of how overloading currently works.
OK, I did not mean there by "header problems" the "theorems automation", but you are right to count it among them. As with "extends", I am not sure, how the "everything" proposal should interact with the rest of current directives (and the "extends" directive), and that question would not be asked if overloading would not be now order-sensitive.
I still thing the environ mechanism can be a lot easier already without having to find out in what way it really is "right".
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.
Josef