Bug in the management of substitutions into auto corrected.

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

diff --git a/helm/matita/matitaDisambiguator.ml b/helm/matita/matitaDisambiguator.ml
index 23de092bd14013c089907259bdfbb77ef5d372ff..bb7f2807dee162fe600850abe176d99dd214a773 100644 (file)
--- 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
@@ -30,7 +32,7 @@ class parserr () =
   end
 
 class disambiguator
-  ~parserr ~dbh ~(chooseUris: MatitaTypes.choose_uris_callback)
+  ~parserr ~dbd ~(chooseUris: MatitaTypes.choose_uris_callback)
   ~(chooseInterp: MatitaTypes.choose_interp_callback) ()
   =
   let disambiguate_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
@@ -70,7 +72,7 @@ class disambiguator
         | Some env -> (false, env)
         | None -> (true, _env)
       in
-      match disambiguate_term ~dbh context metasenv termAst ~aliases:env with
+      match disambiguate_term ~dbd context metasenv termAst ~aliases:env with
       | [ (env, metasenv, term) as x ] ->
           if save_state then self#setEnv env;
           x