From 00d934e7be5c77d8f3ee92d6ee39c2e8fc2d880e Mon Sep 17 00:00:00 2001
From: Andrea Asperti <andrea.asperti@unibo.it>
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