]> matita.cs.unibo.it Git - helm.git/commit
The library is no longer automatically used during disambiguation.
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Sun, 14 Dec 2008 23:03:02 +0000 (23:03 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Sun, 14 Dec 2008 23:03:02 +0000 (23:03 +0000)
commit2cfd3d24d73634238d5eaf40f91e12c10fe28d71
treea4b031365317952d7cccda97e3c6af4c00d8417e
parent426005acf6fb05116de5bae20591eefe55a4df00
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
helm/software/components/disambiguation/disambiguate.ml
helm/software/components/disambiguation/multiPassDisambiguator.ml
helm/software/components/disambiguation/multiPassDisambiguator.mli
helm/software/matita/matitaGui.ml