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

diff --git a/helm/matita/matitaDisambiguator.ml b/helm/matita/matitaDisambiguator.ml
index 01e85e0c4..5b95f4192 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
@@ -70,12 +72,20 @@ class disambiguator
         | Some env -> (false, env)
         | None -> (true, _env)
       in
-      match disambiguate_term ~dbd context metasenv termAst ~aliases:env with
-      | [ (env, metasenv, term) as x ] ->
+      match disambiguate_term ~initial_ugraph:CicUniv.empty_ugraph 
+	~dbd context metasenv termAst ~aliases:env with
+      | [ (env, metasenv, term,ugraph) as x ] ->
           if save_state then self#setEnv env;
           x
       | _ -> assert false
 
+    method disambiguateTermAsts ?(metasenv = []) ?env asts =
+      let ast = CicAst.pack asts in
+      let (env, metasenv, term, ugraph) =
+        self#disambiguateTermAst ~context:[] ~metasenv ?env ast
+      in
+      (env, metasenv, CicUtil.unpack term, ugraph)
+
     method disambiguateTerm ?context ?metasenv ?env stream =
       self#disambiguateTermAst ?context ?metasenv ?env
         (parserr#parseTerm stream)