Command index added to disambiguate.

[helm.git] / components / grafite_parser / grafiteDisambiguate.ml

diff --git a/components/grafite_parser/grafiteDisambiguate.ml b/components/grafite_parser/grafiteDisambiguate.ml
index e9dc23328f338fb5b184552638b636bb74e27c3c..ae4eac52082e91e30f5ad602f230836b162438b3 100644 (file)
--- a/components/grafite_parser/grafiteDisambiguate.ml
+++ b/components/grafite_parser/grafiteDisambiguate.ml
@@ -157,7 +157,7 @@ let disambiguate_tactic
                     metasenv,(GrafiteAst.Type (uri, tyno) :: types)
                 | _ ->
                   raise (GrafiteDisambiguator.DisambiguationError
-                   (0,[[[],None,lazy "Decompose works only on inductive types"]])))
+                   (0,[[[],[],None,lazy "Decompose works only on inductive types"]])))
         in
         let metasenv,types =
          List.fold_left disambiguate (metasenv,[]) types
@@ -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 _