From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Thu, 23 Nov 2006 14:46:01 +0000 (+0000)
Subject: Command index added to disambiguate.
X-Git-Tag: 0.4.95@7852~787
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=00d934e7be5c77d8f3ee92d6ee39c2e8fc2d880e;p=helm.git

Command index added to disambiguate.
-This line, and those below, will be ignored--

M    grafite_parser/grafiteDisambiguate.ml
---

diff --git a/components/grafite_parser/grafiteDisambiguate.ml b/components/grafite_parser/grafiteDisambiguate.ml
index 9a4cb472d..ae4eac520 100644
--- a/components/grafite_parser/grafiteDisambiguate.ml
+++ b/components/grafite_parser/grafiteDisambiguate.ml
@@ -363,6 +363,19 @@ let disambiguate_obj lexicon_status ~baseuri metasenv (text,prefix_len,obj) =
   
 let disambiguate_command lexicon_status ~baseuri metasenv (text,prefix_len,cmd)=
   match cmd with
+   | GrafiteAst.Index(loc,key,uri) ->
+       let lexicon_status_ref = ref lexicon_status in 
+       let disambiguate_term =
+	 disambiguate_term text prefix_len lexicon_status_ref [] in
+       let disambiguate_term_option metasenv =
+	 function
+             None -> metasenv,None
+	   | Some t ->
+               let metasenv,t = disambiguate_term metasenv t in
+		 metasenv, Some t
+       in
+       let metasenv,key = disambiguate_term_option metasenv key in
+       !lexicon_status_ref, metasenv,GrafiteAst.Index(loc,key,uri)
    | GrafiteAst.Coercion _
    | GrafiteAst.Default _
    | GrafiteAst.Drop _