Experimental localization of errors during refinement and disambiguation.

[helm.git] / helm / matita / matitaExcPp.ml

diff --git a/helm/matita/matitaExcPp.ml b/helm/matita/matitaExcPp.ml
index 2d0f60c9e6e4ec7fc749a99aee76e661918606d7..38951713eab19127332836aa3d6f84aed11b2205 100644 (file)
--- a/helm/matita/matitaExcPp.ml
+++ b/helm/matita/matitaExcPp.ml
@@ -69,10 +69,22 @@ let rec to_string =
           aux (n+1) tl ^
            "***** Errors obtained during phase " ^ string_of_int n ^": *****\n"^
             String.concat "\n\n"
-             (List.map (fun msg -> "*Error: " ^ Lazy.force msg) phase) ^
-            "\n\n\n"
+             (List.map (fun (floc,msg) ->
+               let loc_descr =
+                match floc with
+                   None -> ""
+                 | Some floc ->
+                    let (x, y) = HExtlib.loc_of_floc floc in
+                     sprintf " at %d-%d" x y
+               in
+                "*Error" ^ loc_descr ^ ": " ^ Lazy.force msg) phase) ^
+            "\n\n\n" in
+     let loc =
+      match errorll with
+         ((Some _ as loc,_)::_)::_ -> loc
+       | _ -> None
      in
-      None,
+      loc,
        "********** DISAMBIGUATION ERRORS: **********\n" ^
         aux 1 errorll
   | exn -> None, "Uncaught exception: " ^ Printexc.to_string exn