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

diff --git a/helm/matita/matitaDisambiguator.ml b/helm/matita/matitaDisambiguator.ml
index 87215fba1..bb7f2807d 100644
--- a/helm/matita/matitaDisambiguator.ml
+++ b/helm/matita/matitaDisambiguator.ml
@@ -23,24 +23,16 @@
  * http://helm.cs.unibo.it/
  *)
 
+open MatitaTypes
+
 class parserr () =
   object
-    method parseTerm (stream: char Stream.t) =
-      CicTextualParser2.parse_term stream
-
-      (* TODO Zack: implements methods below *)
-    method parseTactic (_: char Stream.t) : DisambiguateTypes.tactic =
-      MatitaTypes.not_implemented "parserr.parseTactic"
-    method parseTactical (_: char Stream.t) : DisambiguateTypes.tactical =
-      MatitaTypes.not_implemented "parserr.parseTactical"
-    method parseCommand (_: char Stream.t) : DisambiguateTypes.command =
-      MatitaTypes.not_implemented "parserr.parseCommand"
-    method parseScript (_: char Stream.t) : DisambiguateTypes.script =
-      MatitaTypes.not_implemented "parserr.parseScript"
+    method parseTerm = CicTextualParser2.parse_term
+    method parseTactical = CicTextualParser2.parse_tactical
   end
 
 class disambiguator
-  ~parserr ~mqiconn ~(chooseUris: MatitaTypes.choose_uris_callback)
+  ~parserr ~dbd ~(chooseUris: MatitaTypes.choose_uris_callback)
   ~(chooseInterp: MatitaTypes.choose_interp_callback) ()
   =
   let disambiguate_term =
@@ -54,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
@@ -80,7 +72,7 @@ class disambiguator
         | Some env -> (false, env)
         | None -> (true, _env)
       in
-      match disambiguate_term mqiconn 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