From 00d934e7be5c77d8f3ee92d6ee39c2e8fc2d880e Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Thu, 23 Nov 2006 14:46:01 +0000 Subject: [PATCH] Command index added to disambiguate. -This line, and those below, will be ignored-- M grafite_parser/grafiteDisambiguate.ml --- components/grafite_parser/grafiteDisambiguate.ml | 13 +++++++++++++ 1 file changed, 13 insertions(+) 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 _ -- 2.39.2