X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_disambiguation%2FdisambiguatePp.ml;h=d6a33cfaedf76a1daa38daa1e1279a8d9f024d21;hb=91a095f0686ee569ba035e4e30c7d071588cb8e7;hp=decaa5f5c6e9a8b13f2ecba403a9412d2d3970a5;hpb=d83fc9accd4ba44a6296eb707b2f62900380f00a;p=helm.git

diff --git a/helm/ocaml/cic_disambiguation/disambiguatePp.ml b/helm/ocaml/cic_disambiguation/disambiguatePp.ml
index decaa5f5c..d6a33cfae 100644
--- a/helm/ocaml/cic_disambiguation/disambiguatePp.ml
+++ b/helm/ocaml/cic_disambiguation/disambiguatePp.ml
@@ -25,6 +25,36 @@
 
 open DisambiguateTypes
 
+let parse_environment str =
+ let stream = Stream.of_string str in
+ let environment = ref Environment.empty in
+  try
+    while true do
+     let alias =
+      match GrafiteParser.parse_statement stream with
+         GrafiteAst.Executable (_, GrafiteAst.Command (_, GrafiteAst.Alias (_,alias)))
+           -> alias
+       | _ -> assert false in
+     let key,value =
+      (*CSC: Warning: this code should be factorized with the corresponding
+             code in MatitaEngine *)
+      match alias with
+         GrafiteAst.Ident_alias (id,uri) ->
+          Id id,
+          (uri,(fun _ _ _-> CicUtil.term_of_uri (UriManager.uri_of_string uri)))
+       | GrafiteAst.Symbol_alias (symb,instance,desc) ->
+          Symbol (symb,instance),
+          DisambiguateChoices.lookup_symbol_by_dsc symb desc
+       | GrafiteAst.Number_alias (instance,desc) ->
+          Num instance,
+          DisambiguateChoices.lookup_num_by_dsc desc
+     in
+      environment := Environment.add key value !environment;
+    done;
+    assert false
+  with End_of_file ->
+   !environment
+
 let pp_environment env =
   let aliases =
     Environment.fold