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

diff --git a/helm/software/components/disambiguation/disambiguate.ml b/helm/software/components/disambiguation/disambiguate.ml
index 348ca7c099fbacb707f8b84d55386573a2e746d3..44498d08830b5b7c266f5573739ef119cf772f43 100644 (file)
--- 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 becf2a41229c18b0b3259a1f2d453a05d0e716c7..63bcaa587197b08da14e9b211f2cb4688085016e 100644 (file)
--- 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 0151f8d3dd7e8a8aef4d4a573b2622a519164424..21818816ca6d405d9fd8ce06d552b4744a6d29f2 100644 (file)
--- 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 7db4d5af12bcb3a5bbf8074f69a09282d41d5e60..ed5582a16addba81466f650b03db99cbe9164afc 100644 (file)
--- 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;