X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fmatita%2FmatitaGui.ml;h=6b1f24743295df187a4d625afa5822e7180b84be;hb=c0f86a886451a0df3b42a1435e21b5def9f34792;hp=de98b49b8526b0a9ce3de21eb2e86489c0e255b4;hpb=816ee790efa658355907a90f0532eed4ba6244d5;p=helm.git

diff --git a/helm/software/matita/matitaGui.ml b/helm/software/matita/matitaGui.ml
index de98b49b8..6b1f24743 100644
--- a/helm/software/matita/matitaGui.ml
+++ b/helm/software/matita/matitaGui.ml
@@ -282,86 +282,7 @@ let rec interactive_error_interp ?(all_passes=false) (source_buffer:GSourceView.
           annotated_errorll ()
          end
    in
-  let choices =
-   List.flatten
-    (List.map
-      (fun (pass,l) ->
-        List.map
-         (fun (env,diff,offset,msg,significant) ->
-           offset, [[pass], [[pass], env, diff], msg, significant]) l
-      ) errorll') in
-  (* Here we are doing a stable sort and list_uniq returns the latter
-     "equal" element. I.e. we are showing the error corresponding to the
-     most advanced disambiguation pass *)
-  let choices =
-   let choices_compare (o1,_) (o2,_) = compare o1 o2 in
-   let choices_compare_by_passes (p1,_,_,_) (p2,_,_,_) =
-    compare p1 p2 in
-   let rec uniq =
-    function
-       [] -> []
-     | h::[] -> [h]
-     | (o1,res1)::(o2,res2)::tl when o1 = o2 ->
-        let merge_by_name errors =
-         let merge_by_env errors =
-          let choices_compare_by_env (_,e1,_) (_,e2,_) = compare e1 e2 in
-          let choices_compare_by_passes (p1,_,_) (p2,_,_) =
-           compare p1 p2 in
-          let rec uniq_by_env =
-           function
-              [] -> []
-            | h::[] -> [h]
-            | (p1,e1,_)::(p2,e2,d2)::tl when e1 = e2 ->
-                uniq_by_env ((p1@p2,e2,d2) :: tl) 
-            | h1::tl -> h1 :: uniq_by_env tl
-          in
-           List.sort choices_compare_by_passes
-            (uniq_by_env (List.stable_sort choices_compare_by_env errors))
-         in
-         let choices_compare_by_msg (_,_,m1,_) (_,_,m2,_) =
-          compare (Lazy.force m1) (Lazy.force m2) in
-         let rec uniq_by_msg =
-          function
-             [] -> []
-           | h::[] -> [h]
-           | (p1,i1,m1,s1)::(p2,i2,m2,s2)::tl
-             when Lazy.force m1 = Lazy.force m2 && s1 = s2 ->
-               uniq_by_msg ((p1@p2,merge_by_env (i1@i2),m2,s2) :: tl)
-           | h1::tl -> h1 :: uniq_by_msg tl
-         in
-          List.sort choices_compare_by_msg
-           (uniq_by_msg (List.stable_sort choices_compare_by_msg errors))
-        in
-         let res = merge_by_name (res1@res2) in
-          uniq ((o1,res) :: tl)
-     | h1::tl -> h1 :: uniq tl
-   in
-   (* 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
+  let choices = MatitaExcPp.compact_disambiguation_errors all_passes errorll' in
    match choices with
       [] -> assert false
     | [loffset,[_,envs_and_diffs,msg,significant]] ->