DisambiguationError exceptions (that have locations inside) are now relocated

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

diff --git a/helm/matita/matitaExcPp.ml b/helm/matita/matitaExcPp.ml
index 38951713eab19127332836aa3d6f84aed11b2205..b79fea6631212e79be1374aa8041800af9c91bc2 100644 (file)
--- a/helm/matita/matitaExcPp.ml
+++ b/helm/matita/matitaExcPp.ml
@@ -61,7 +61,7 @@ let rec to_string =
      None, "Type checking error: " ^ Lazy.force msg
   | CicTypeChecker.AssertFailure msg ->
      None, "Type checking assertion failed: " ^ Lazy.force msg
-  | MatitaDisambiguator.DisambiguationError errorll ->
+  | MatitaDisambiguator.DisambiguationError (offset,errorll) ->
      let rec aux n =
       function
          [] -> ""
@@ -75,13 +75,21 @@ let rec to_string =
                    None -> ""
                  | Some floc ->
                     let (x, y) = HExtlib.loc_of_floc floc in
-                     sprintf " at %d-%d" x y
+                     sprintf " at %d-%d" (x+offset) (y+offset)
                in
                 "*Error" ^ loc_descr ^ ": " ^ Lazy.force msg) phase) ^
             "\n\n\n" in
      let loc =
       match errorll with
-         ((Some _ as loc,_)::_)::_ -> loc
+         ((Some floc,_)::_)::_ ->
+          let (x, y) = HExtlib.loc_of_floc floc in
+          let x = x + offset in
+          let y = y + offset in
+          let flocb,floce = floc in
+          let floc =
+           {flocb with Lexing.pos_cnum = x}, {floce with Lexing.pos_cnum = y}
+          in
+           Some floc
        | _ -> None
      in
       loc,