X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fgrafite_parser%2FgrafiteDisambiguate.ml;h=3d6f893eeb0f35729ab2488a883dee88689f9e72;hb=2ca2baa7b345693c7684994130707fb152227931;hp=da72944781d5f0138b286fde5529d1778e88e40d;hpb=827e35d6058ebba3a4a4fa6eb3c160f0cd0fd1e8;p=helm.git

diff --git a/helm/ocaml/grafite_parser/grafiteDisambiguate.ml b/helm/ocaml/grafite_parser/grafiteDisambiguate.ml
index da7294478..3d6f893ee 100644
--- a/helm/ocaml/grafite_parser/grafiteDisambiguate.ml
+++ b/helm/ocaml/grafite_parser/grafiteDisambiguate.ml
@@ -23,6 +23,8 @@
  * http://helm.cs.unibo.it/
  *)
 
+(* $Id$ *)
+
 exception BaseUriNotSetYet
 
 let singleton = function
@@ -246,7 +248,7 @@ let disambiguate_obj lexicon_status ~baseuri metasenv obj =
   lexicon_status, metasenv, cic
   
 let disambiguate_command lexicon_status ~baseuri metasenv =
-  function
+ function
   | GrafiteAst.Coercion _
   | GrafiteAst.Default _
   | GrafiteAst.Drop _
@@ -258,3 +260,29 @@ let disambiguate_command lexicon_status ~baseuri metasenv =
       let lexicon_status,metasenv,obj =
        disambiguate_obj lexicon_status ~baseuri metasenv obj in
       lexicon_status, metasenv, GrafiteAst.Obj (loc,obj)
+
+let disambiguate_macro lexicon_status_ref metasenv context macro =
+ let disambiguate_term = disambiguate_term lexicon_status_ref in
+  match macro with
+   | GrafiteAst.WMatch (loc,term) ->
+      let metasenv,term = disambiguate_term context metasenv term in
+       metasenv,GrafiteAst.WMatch (loc,term)
+   | GrafiteAst.WInstance (loc,term) ->
+      let metasenv,term = disambiguate_term context metasenv term in
+       metasenv,GrafiteAst.WInstance (loc,term)
+   | GrafiteAst.WElim (loc,term) ->
+      let metasenv,term = disambiguate_term context metasenv term in
+       metasenv,GrafiteAst.WElim (loc,term)
+   | GrafiteAst.WHint (loc,term) ->
+      let metasenv,term = disambiguate_term context metasenv term in
+       metasenv,GrafiteAst.WHint (loc,term)
+   | GrafiteAst.Check (loc,term) ->
+      let metasenv,term = disambiguate_term context metasenv term in
+       metasenv,GrafiteAst.Check (loc,term)
+   | GrafiteAst.Hint _
+   | GrafiteAst.WLocate _ as macro ->
+      metasenv,macro
+   | GrafiteAst.Quit _
+   | GrafiteAst.Print _
+   | GrafiteAst.Search_pat _
+   | GrafiteAst.Search_term _ -> assert false