From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Sun, 14 Dec 2008 23:03:02 +0000 (+0000)
Subject: The library is no longer automatically used during disambiguation.
X-Git-Tag: make_still_working~4397
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=2cfd3d24d73634238d5eaf40f91e12c10fe28d71;hp=2cfd3d24d73634238d5eaf40f91e12c10fe28d71;p=helm.git

The library is no longer automatically used during disambiguation.
It is used only when the user press the More button or when he selects
the library from the Debug (?????) menu!

Moreover, using the library or not using it has now a different behaviour:
1. when the library is NOT used, symbols with no preferences are no
   longer automatically looked for in the library
2. when the library IS used, only passes 5 and 6 are tried.

CONS:
1. the Debug menu voice is now necessary: move it elsewhere? always open the
   disambiguation window making it non-modal? put an hyperlink in the error
   message window?
2. when the library is used, all previous preferences are completely ignored
   for all symbols. This makes the system much more stupid than what it used
   to be.

PROS:
disambiguation is now much faster in case of error
---