From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Fri, 8 Dec 2006 11:39:07 +0000 (+0000)
Subject: Disambiguation errors in phase 3 that are not present in phase 4 are filtered
X-Git-Tag: 0.4.95@7852~741
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=3f9fd7c83c59b8230cb349a9114e72e026ac12d0;p=helm.git

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 79962a35c..baf5998a5 100644
--- 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