X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaDisambiguator.ml;h=bb7f2807dee162fe600850abe176d99dd214a773;hb=e09713d333183e929f108ff8bb8fbe2a25bfcac7;hp=01e85e0c45c0f4ba42bffa85c6d29902c955a275;hpb=afd3b379d4959e4a18c1f26f25e4a9c14997866f;p=helm.git

diff --git a/helm/matita/matitaDisambiguator.ml b/helm/matita/matitaDisambiguator.ml
index 01e85e0c4..bb7f2807d 100644
--- a/helm/matita/matitaDisambiguator.ml
+++ b/helm/matita/matitaDisambiguator.ml
@@ -23,6 +23,8 @@
  * http://helm.cs.unibo.it/
  *)
 
+open MatitaTypes
+
 class parserr () =
   object
     method parseTerm = CicTextualParser2.parse_term
@@ -44,12 +46,12 @@ class disambiguator
             ~nonvars_button:enable_button_for_non_vars uris
 
         let interactive_interpretation_choice = chooseInterp
-        let input_or_locate_uri ~(title:string) =
-          (* TODO Zack: I try to avoid using this callback. I therefore assume
-           * that the presence of an identifier that can't be resolved via
-           * "locate" query is a syntax error *)
-          MatitaTypes.not_implemented
-            "MatitaDisambiguator: input_or_locate_uri callback"
+        let input_or_locate_uri ~(title:string) ?id =
+          (* Zack: I try to avoid using this callback. I therefore assume that
+          * the presence of an identifier that can't be resolved via "locate"
+          * query is a syntax error *)
+          let msg = match id with Some id -> id | _ -> "" in
+          raise (Unbound_identifier msg)
       end
     in
     let module Disambiguator = Disambiguate.Make (Callbacks) in