From 2cfd3d24d73634238d5eaf40f91e12c10fe28d71 Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Sun, 14 Dec 2008 23:03:02 +0000
Subject: [PATCH] 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
---
 .../components/disambiguation/disambiguate.ml |  5 +----
 .../disambiguation/multiPassDisambiguator.ml  |  9 ++++++---
 .../disambiguation/multiPassDisambiguator.mli |  1 +
 helm/software/matita/matitaGui.ml             | 20 +++++++++++++++----
 4 files changed, 24 insertions(+), 11 deletions(-)

diff --git a/helm/software/components/disambiguation/disambiguate.ml b/helm/software/components/disambiguation/disambiguate.ml
index 348ca7c09..44498d088 100644
--- a/helm/software/components/disambiguation/disambiguate.ml
+++ b/helm/software/components/disambiguation/disambiguate.ml
@@ -443,10 +443,7 @@ let disambiguate_thing
               | item -> item
             in
             Environment.find item e
-          with Not_found -> 
-            lookup_in_library 
-              interactive_user_uri_choice 
-              input_or_locate_uri item)
+          with Not_found -> [])
    in
 (*
       (* <benchmark> *)
diff --git a/helm/software/components/disambiguation/multiPassDisambiguator.ml b/helm/software/components/disambiguation/multiPassDisambiguator.ml
index becf2a412..63bcaa587 100644
--- a/helm/software/components/disambiguation/multiPassDisambiguator.ml
+++ b/helm/software/components/disambiguation/multiPassDisambiguator.ml
@@ -41,18 +41,21 @@ exception DisambiguationError of
 (* implement module's API *)
 
 let only_one_pass = ref false;;
+let use_library = ref false;;
 
 let passes () = (* <fresh_instances?, aliases, coercions?> *)
  if !only_one_pass then
   [ (true, `Mono, false) ]
+ else if !use_library then
+  [ (true, `Library, false); 
+      (* for demo to reduce the number of interpretations *)
+    (true, `Library, true);
+  ]
  else
   [ (true, `Mono, false);
     (true, `Multi, false);
     (true, `Mono, true);
     (true, `Multi, true);
-    (true, `Library, false); 
-      (* for demo to reduce the number of interpretations *)
-    (true, `Library, true);
   ]
 ;;
 
diff --git a/helm/software/components/disambiguation/multiPassDisambiguator.mli b/helm/software/components/disambiguation/multiPassDisambiguator.mli
index 0151f8d3d..21818816c 100644
--- a/helm/software/components/disambiguation/multiPassDisambiguator.mli
+++ b/helm/software/components/disambiguation/multiPassDisambiguator.mli
@@ -33,6 +33,7 @@ exception DisambiguationError of
 
 (** initially false; for debugging only (???) *)
 val only_one_pass: bool ref
+val use_library: bool ref
 
 val passes : unit -> (bool * [> `Library | `Mono | `Multi ] * bool) list
 
diff --git a/helm/software/matita/matitaGui.ml b/helm/software/matita/matitaGui.ml
index 7db4d5af1..ed5582a16 100644
--- a/helm/software/matita/matitaGui.ml
+++ b/helm/software/matita/matitaGui.ml
@@ -201,6 +201,7 @@ class interpErrorModel =
         tree_store#get ~row:iter ~column:interp_no_col
     end
 
+exception UseLibrary;;
 
 let rec interactive_error_interp ~all_passes
   (source_buffer:GSourceView.source_buffer) notify_exn offset errorll filename
@@ -347,9 +348,7 @@ let rec interactive_error_interp ~all_passes
             return ()
         );
        connect_button dialog#disambiguationErrorsMoreErrors
-        (fun _ -> return () ;
-          interactive_error_interp ~all_passes:true source_buffer
-           notify_exn offset errorll filename);
+        (fun _ -> return () ; raise UseLibrary);
        connect_button dialog#disambiguationErrorsCancelButton fail;
        dialog#disambiguationErrors#show ();
        GtkThread.main ()
@@ -702,8 +701,11 @@ class gui () =
        let thread_main =
         fun () -> 
           lock_world ();
+          let saved_use_library= !MultiPassDisambiguator.use_library in
           try
+           MultiPassDisambiguator.use_library := !all_disambiguation_passes;
            f ();
+           MultiPassDisambiguator.use_library := saved_use_library;
            unlock_world ()
           with
            | MultiPassDisambiguator.DisambiguationError (offset,errorll) ->
@@ -712,7 +714,17 @@ class gui () =
                  ~all_passes:!all_disambiguation_passes source_buffer
                  notify_exn offset errorll (s())#filename
                with
-                exc -> notify_exn exc);
+                | UseLibrary ->
+                   MultiPassDisambiguator.use_library := true;
+                   (try f ()
+                    with
+                    | MultiPassDisambiguator.DisambiguationError (offset,errorll) ->
+                       interactive_error_interp ~all_passes:true source_buffer
+                        notify_exn offset errorll (s())#filename
+                    | exc ->
+                       notify_exn exc);
+                | exc -> notify_exn exc);
+              MultiPassDisambiguator.use_library := saved_use_library;
               unlock_world ()
            | exc ->
               notify_exn exc;
-- 
2.39.2