]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/grafite_parser/grafiteDisambiguate.ml
1. Macros are now handled using an execption that is caught by matitacLib
[helm.git] / helm / ocaml / grafite_parser / grafiteDisambiguate.ml
index da72944781d5f0138b286fde5529d1778e88e40d..4be748460e26691101d2be8bf9ba3dfff4b600a7 100644 (file)
@@ -246,7 +246,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 +258,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