From 3f9fd7c83c59b8230cb349a9114e72e026ac12d0 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Fri, 8 Dec 2006 11:39:07 +0000 Subject: [PATCH] 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. --- matita/matitaGui.ml | 27 +++++++++++++++++++++++++-- 1 file changed, 25 insertions(+), 2 deletions(-) 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 -- 2.39.2