Main result for e.

[helm.git] / helm / software / matita / matitaGui.ml

diff --git a/helm/software/matita/matitaGui.ml b/helm/software/matita/matitaGui.ml
index de98b49b8526b0a9ce3de21eb2e86489c0e255b4..99b623b0f00c037d768b7b8d8033b99ba65d788b 100644 (file)
--- a/helm/software/matita/matitaGui.ml
+++ b/helm/software/matita/matitaGui.ml
@@ -33,6 +33,8 @@ open MatitaMisc
 
 exception Found of int
 
+let all_disambiguation_passes = ref false
+
 let gui_instance = ref None
 
 class type browserWin =
@@ -227,7 +229,7 @@ class interpErrorModel =
     end
 
 
-let rec interactive_error_interp ?(all_passes=false) (source_buffer:GSourceView.source_buffer) notify_exn offset errorll script_fname
+let rec interactive_error_interp ~all_passes (source_buffer:GSourceView.source_buffer) notify_exn offset errorll script_fname
 = 
   (* hook to save a script for each disambiguation error *)
   if false then
@@ -282,86 +284,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]] ->
@@ -445,8 +368,8 @@ let rec interactive_error_interp ?(all_passes=false) (source_buffer:GSourceView.
         );
        connect_button dialog#disambiguationErrorsMoreErrors
         (fun _ -> return () ;
-          interactive_error_interp ~all_passes:true source_buffer notify_exn
-           offset errorll script_fname);
+          interactive_error_interp ~all_passes:true source_buffer
+           notify_exn offset errorll script_fname);
        connect_button dialog#disambiguationErrorsCancelButton fail;
        dialog#disambiguationErrors#show ();
        GtkThread.main ()
@@ -790,8 +713,8 @@ class gui () =
           with
            | GrafiteDisambiguator.DisambiguationError (offset,errorll) ->
               (try
-                interactive_error_interp source_buffer notify_exn offset
-                 errorll script_fname
+                interactive_error_interp ~all_passes:!all_disambiguation_passes source_buffer
+                 notify_exn offset errorll script_fname
                with
                 exc -> notify_exn exc);
               unlock_world ()