From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Thu, 22 Nov 2007 16:37:43 +0000 (+0000)
Subject: Bug fixed in printing of passes in error messages.
X-Git-Tag: 0.4.98@7921~9
X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=f2b44fbe63263f5ed70d251304f0df670302182f

Bug fixed in printing of passes in error messages.
---

diff --git a/matita/matitaGui.ml b/matita/matitaGui.ml
index 8eb54bb70..f4024c3cb 100644
--- a/matita/matitaGui.ml
+++ b/matita/matitaGui.ml
@@ -233,25 +233,30 @@ let rec interactive_error_interp ?(all_passes=false) (source_buffer:GSourceView.
   let errorll' =
    let remove_non_significant =
      List.filter (fun (_env,_diff,_loc,_msg,significant) -> significant) in
-   if all_passes then errorll else
+   let annotated_errorll () =
+    List.rev
+     (snd
+       (List.fold_left (fun (pass,res) item -> pass+1,(pass+1,item)::res) (0,[])
+         errorll)) in
+   if all_passes then annotated_errorll () else
      let safe_list_nth l n = try List.nth l n with Failure _ -> [] in
     (* We remove passes 1,2 and 5,6 *)
      let res =
-      []::[]
-      ::(remove_non_significant (safe_list_nth errorll 2))
-      ::(remove_non_significant (safe_list_nth errorll 3))
-      ::[]::[]
+      (1,[])::(2,[])
+      ::(3,remove_non_significant (safe_list_nth errorll 2))
+      ::(4,remove_non_significant (safe_list_nth errorll 3))
+      ::(5,[])::(6,[])::[]
      in
-      if List.flatten res <> [] then res
+      if List.flatten (List.map snd res) <> [] then res
       else
        (* all errors (if any) are not significant: we keep them *)
        let res =
-        []::[]
-        ::(safe_list_nth errorll 2)
-        ::(safe_list_nth errorll 3)
-        ::[]::[]
+        (1,[])::(2,[])
+        ::(3,(safe_list_nth errorll 2))
+        ::(4,(safe_list_nth errorll 3))
+        ::(5,[])::(6,[])::[]
        in
-        if List.flatten res <> [] then
+        if List.flatten (List.map snd res) <> [] then
 	 begin
           HLog.warn
 	   "All disambiguation errors are not significant. Showing them anyway." ;
@@ -261,18 +266,16 @@ let rec interactive_error_interp ?(all_passes=false) (source_buffer:GSourceView.
          begin
           HLog.warn
 	   "No errors in phases 2 and 3. Showing all errors in all phases" ;
-          errorll
+          annotated_errorll ()
          end
    in
   let choices =
-   let pass = ref 0 in
    List.flatten
     (List.map
-      (fun l ->
-        incr pass;
+      (fun (pass,l) ->
         List.map
          (fun (env,diff,offset,msg,significant) ->
-           offset, [[!pass], [[!pass], env, diff], msg, significant]) l
+           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