X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2FmatitaGui.ml;h=6b1f24743295df187a4d625afa5822e7180b84be;hb=3a5b9647787e1402f6886d41824f664db290963f;hp=f4024c3cbad5a72cece6c125a721184efe3e17fc;hpb=25e80c6f83850854ed8e8e922fff4e467f8b9924;p=helm.git

diff --git a/helm/software/matita/matitaGui.ml b/helm/software/matita/matitaGui.ml
index f4024c3cb..6b1f24743 100644
--- a/helm/software/matita/matitaGui.ml
+++ b/helm/software/matita/matitaGui.ml
@@ -227,8 +227,21 @@ class interpErrorModel =
     end
 
 
-let rec interactive_error_interp ?(all_passes=false) (source_buffer:GSourceView.source_buffer) notify_exn offset errorll
+let rec interactive_error_interp ?(all_passes=false) (source_buffer:GSourceView.source_buffer) notify_exn offset errorll script_fname
 = 
+  (* hook to save a script for each disambiguation error *)
+  if false then
+   (let text =
+     source_buffer#get_text ~start:source_buffer#start_iter
+      ~stop:source_buffer#end_iter () in
+    let md5 = Digest.to_hex (Digest.string text) in
+    let filename = match script_fname with Some s -> s | None -> "unnamed.ma" in
+    let filename =
+     Filename.chop_extension filename ^ ".error." ^ md5 ^ ".ma"  in
+    let ch = open_out filename in
+     output_string ch text;
+    close_out ch
+   );
   assert (List.flatten errorll <> []);
   let errorll' =
    let remove_non_significant =
@@ -269,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]] ->
@@ -432,8 +366,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);
+          interactive_error_interp ~all_passes:true source_buffer notify_exn
+           offset errorll script_fname);
        connect_button dialog#disambiguationErrorsCancelButton fail;
        dialog#disambiguationErrors#show ();
        GtkThread.main ()
@@ -778,7 +712,7 @@ class gui () =
            | GrafiteDisambiguator.DisambiguationError (offset,errorll) ->
               (try
                 interactive_error_interp source_buffer notify_exn offset
-                 errorll
+                 errorll script_fname
                with
                 exc -> notify_exn exc);
               unlock_world ()