X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=inline;f=helm%2Fsoftware%2Fcomponents%2Fgrafite_parser%2FgrafiteDisambiguate.ml;h=9c12d1173c6c9b212e021f52b71e24b1d7ea863b;hb=8bb849acb32ab6180be4ea23dbb9fe35d7300ceb;hp=b5c08fba696b979333991ed9f1d661688d9c6fc3;hpb=e085135177f7b3b74b410d47a4f3bca1784b60b1;p=helm.git

diff --git a/helm/software/components/grafite_parser/grafiteDisambiguate.ml b/helm/software/components/grafite_parser/grafiteDisambiguate.ml
index b5c08fba6..9c12d1173 100644
--- a/helm/software/components/grafite_parser/grafiteDisambiguate.ml
+++ b/helm/software/components/grafite_parser/grafiteDisambiguate.ml
@@ -78,6 +78,7 @@ let ncic_mk_choice = function
            (NCic.Appl l)::tl -> NCic.Appl (l@tl) | l -> NCic.Appl l)
         ~term_of_uri:(fun uri ->
            fst (OCic2NCic.convert_term uri (CicUtil.term_of_uri uri)))
+        ~term_of_nref:(fun nref -> NCic.Const nref)
        name dsc
   | LexiconAst.Number_alias (_, dsc) -> 
        let desc,f = DisambiguateChoices.lookup_num_by_dsc dsc in
@@ -89,32 +90,13 @@ let ncic_mk_choice = function
   | LexiconAst.Ident_alias (name, uri) -> 
      uri, `Sym_interp 
       (fun l->assert(l = []);
-        let nuri = NUri.uri_of_string uri in
         try
-         let _,height,_,_,_ = NCicEnvironment.get_checked_obj nuri in
-          NCic.Const
-           (NReference.reference_of_spec nuri (NReference.Def height))
+         let nref = NReference.reference_of_string uri in
+          NCic.Const nref
         with
-         NCicEnvironment.ObjectNotFound _ ->
-(*
-(*
-        if String.sub uri (String.length uri - 3) 3 = "def" then
-*)
-         let nuri = NUri.uri_of_string uri in(*
-          NUri.uri_of_string (String.sub uri 0 (String.length uri -3) ^ "def")
-         in
-*)
-          NCic.Const
-           (NReference.reference_of_spec nuri (NReference.Def 0))
-)
-*)
-(*
-        else
-*)
-         let uri = UriManager.uri_of_string uri in
-          fst (OCic2NCic.convert_term uri (CicUtil.term_of_uri uri)))
-(*
-*)
+         NReference.IllFormedReference _ ->
+          let uri = UriManager.uri_of_string uri in
+           fst (OCic2NCic.convert_term uri (CicUtil.term_of_uri uri)))
 ;;
 
 
@@ -176,6 +158,23 @@ let lookup_in_library
   | DisambiguateTypes.Num instance -> mk_num_alias instance
 ;;
 
+let nlookup_in_library 
+  interactive_user_uri_choice input_or_locate_uri item 
+=
+  match item with
+  | DisambiguateTypes.Id id -> 
+     (try
+       let references = NCicLibrary.resolve id in
+        List.map
+         (fun u -> LexiconAst.Ident_alias (id,NReference.string_of_reference u)
+         ) references @
+        lookup_in_library interactive_user_uri_choice input_or_locate_uri item
+      with
+       NCicLibrary.ObjectNotFound _ ->
+        lookup_in_library interactive_user_uri_choice input_or_locate_uri item)
+  | _ -> lookup_in_library interactive_user_uri_choice input_or_locate_uri item 
+;;
+
   (** @param term not meaningful when context is given *)
 let disambiguate_term expty text prefix_len lexicon_status_ref context metasenv
 term =
@@ -205,7 +204,7 @@ let disambiguate_nterm expty lexicon_status context metasenv subst thing
         ~aliases:lexicon_status.LexiconEngine.aliases
         ~expty 
         ~universe:(Some lexicon_status.LexiconEngine.multi_aliases)
-        ~lookup_in_library
+        ~lookup_in_library:nlookup_in_library
         ~mk_choice:ncic_mk_choice
         ~mk_implicit
         ~description_of_alias:LexiconAst.description_of_alias
@@ -688,7 +687,7 @@ let disambiguate_obj lexicon_status ?baseuri metasenv (text,prefix_len,obj) =
        (try
          (match 
           NCicDisambiguate.disambiguate_obj
-           ~lookup_in_library
+           ~lookup_in_library:nlookup_in_library
            ~description_of_alias:LexiconAst.description_of_alias
            ~mk_choice:ncic_mk_choice
            ~mk_implicit
@@ -776,7 +775,7 @@ let disambiguate_nobj lexicon_status ?baseuri (text,prefix_len,obj) =
   let diff, _, _, cic =
    singleton "third"
     (NCicDisambiguate.disambiguate_obj
-      ~lookup_in_library
+      ~lookup_in_library:nlookup_in_library
       ~description_of_alias:LexiconAst.description_of_alias
       ~mk_choice:ncic_mk_choice
       ~mk_implicit
@@ -838,6 +837,7 @@ let disambiguate_command lexicon_status ?baseuri metasenv (text,prefix_len,cmd)=
    | GrafiteAst.Print _
    | GrafiteAst.Qed _
    | GrafiteAst.NQed _
+   | GrafiteAst.NUnivConstraint _
    | GrafiteAst.Set _ as cmd ->
        lexicon_status,metasenv,cmd
    | GrafiteAst.Obj (loc,obj) ->