X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaDisambiguator.ml;h=325e290a74f4636d231d136b2b2f2995808cc597;hb=78d6c353f0288a1b3b86aeb43b22a483c34822d9;hp=0f4dc67db6b9fafc977d414b3f7e85f5a79b729e;hpb=b881e38c03d5ecf26267a47d7e4208bd31ebc33d;p=helm.git

diff --git a/helm/matita/matitaDisambiguator.ml b/helm/matita/matitaDisambiguator.ml
index 0f4dc67db..325e290a7 100644
--- a/helm/matita/matitaDisambiguator.ml
+++ b/helm/matita/matitaDisambiguator.ml
@@ -28,7 +28,9 @@ open Printf
 open MatitaTypes
 
 exception Ambiguous_input
-exception DisambiguationError of string Lazy.t list list
+(* the integer is an offset to be added to each location *)
+exception DisambiguationError of
+ int * (Token.flocation option * string Lazy.t) list list
 
 type choose_uris_callback =
   id:string -> UriManager.uri list -> UriManager.uri list
@@ -109,12 +111,12 @@ let disambiguate_thing ~aliases ~universe
     | [ pass ] ->
         (try
           set_aliases pass (try_pass pass)
-         with Disambiguate.NoWellTypedInterpretation newerrors ->
-          raise (DisambiguationError (errors @ [newerrors])))
+         with Disambiguate.NoWellTypedInterpretation (offset,newerrors) ->
+          raise (DisambiguationError (offset, errors @ [newerrors])))
     | hd :: tl ->
         (try
           set_aliases hd (try_pass hd)
-        with Disambiguate.NoWellTypedInterpretation newerrors ->
+        with Disambiguate.NoWellTypedInterpretation (_offset,newerrors) ->
          aux (errors @ [newerrors]) tl)
     | [] -> assert false
   in