DisambiguationError exceptions (that have locations inside) are now relocated

[helm.git] / helm / matita / matitaDisambiguator.mli

diff --git a/helm/matita/matitaDisambiguator.mli b/helm/matita/matitaDisambiguator.mli
index 64cd5563b1d691d6035b54c03f03607f35b976fb..4cd1bd0dde0fc798544ff21cfe09996e57927fc5 100644 (file)
--- a/helm/matita/matitaDisambiguator.mli
+++ b/helm/matita/matitaDisambiguator.mli
@@ -28,8 +28,9 @@ open MatitaTypes
 (** raised when ambiguous input is found but not expected (e.g. in the batch
   * compiler) *)
 exception Ambiguous_input
+(* the integer is an offset to be added to each location *)
 exception DisambiguationError of
- (Token.flocation option * string Lazy.t) list list
+ int * (Token.flocation option * string Lazy.t) list list
 
 type choose_uris_callback = id:string -> UriManager.uri list -> UriManager.uri list
 type choose_interp_callback = (string * string) list list -> int list