]> matita.cs.unibo.it Git - helm.git/commitdiff
Command index added to disambiguate.
authorAndrea Asperti <andrea.asperti@unibo.it>
Thu, 23 Nov 2006 14:46:01 +0000 (14:46 +0000)
committerAndrea Asperti <andrea.asperti@unibo.it>
Thu, 23 Nov 2006 14:46:01 +0000 (14:46 +0000)
-This line, and those below, will be ignored--

M    grafite_parser/grafiteDisambiguate.ml

helm/software/components/grafite_parser/grafiteDisambiguate.ml

index 9a4cb472d75517b3742b956a3b2a2ec9c0580d28..ae4eac52082e91e30f5ad602f230836b162438b3 100644 (file)
@@ -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 _