Disambiguation errors in phase 3 that are not present in phase 4 are filtered

out. Explanation: if they are only in phase 3, it means that in phase 4 they
are not significative. Thus we conclude that phase 3 is not significative.
There is a drawback: equality over errors is not very well defined because
of Metas in error messages. Thus it could be the case that we remove the error
in phase 3 when the same error is still there in phase 4.

diff --git a/matita/matitaGui.ml b/matita/matitaGui.ml
index 79962a35cd86169f625acd0bf2597a7afcf59d77..baf5998a5371a8f3f535aa35fc877dbba1093287 100644 (file)
--- a/matita/matitaGui.ml
+++ b/matita/matitaGui.ml
@@ -301,8 +301,31 @@ let rec interactive_error_interp ?(all_passes=false) (source_buffer:GSourceView.
           uniq ((o1,res) :: tl)
      | h1::tl -> h1 :: uniq tl
    in
-    List.map (fun o,l -> o,List.sort choices_compare_by_passes l)
-     (uniq (List.stable_sort choices_compare choices))
+   (* Errors in phase 3 that are not also in phase 4 are filtered out *)
+   let filter_phase_3 choices =
+    if all_passes then choices
+    else
+     let filter =
+      HExtlib.filter_map
+       (function
+           (loffset,messages) ->
+              let filtered_messages =
+               HExtlib.filter_map
+                (function
+                    [3],_,_,_ -> None
+                  | item -> Some item
+                ) messages
+              in
+               if filtered_messages = [] then
+                None
+               else
+                Some (loffset,filtered_messages))
+     in
+      filter choices
+   in
+    filter_phase_3
+     (List.map (fun o,l -> o,List.sort choices_compare_by_passes l)
+       (uniq (List.stable_sort choices_compare choices)))
   in
    match choices with
       [] -> assert false