X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_disambiguation%2FdisambiguatePp.ml;h=b7c1012a8dc68474e2515f567320f82a4c7bbe8d;hb=8539d00ff2ed0ffd9b7a08ac8e62376e88987960;hp=1d36df44d0c191346f0614b7f355f34f16b9bdf2;hpb=e20f3963028a966fc93ba0d611c4aa8341d20e2c;p=helm.git

diff --git a/helm/ocaml/cic_disambiguation/disambiguatePp.ml b/helm/ocaml/cic_disambiguation/disambiguatePp.ml
index 1d36df44d..b7c1012a8 100644
--- a/helm/ocaml/cic_disambiguation/disambiguatePp.ml
+++ b/helm/ocaml/cic_disambiguation/disambiguatePp.ml
@@ -25,23 +25,59 @@
 
 open DisambiguateTypes
 
+let parse_environment str =
+ let stream = Stream.of_string str in
+ let environment = ref Environment.empty in
+ let multiple_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;
+      multiple_environment := Environment.cons key value !multiple_environment;
+    done;
+    assert false
+  with End_of_file ->
+   !environment, !multiple_environment
+
+let aliases_of_environment env =
+  Environment.fold
+    (fun domain_item (dsc,_) acc ->
+      let s =
+        match domain_item with
+        | Id id -> GrafiteAst.Ident_alias (id, dsc)
+        | Symbol (symb, i) -> GrafiteAst.Symbol_alias (symb, i, dsc)
+        | Num i -> GrafiteAst.Number_alias (i, dsc)
+      in
+       s :: acc)
+    env []
+
+let commands_of_environment env =
+  List.map
+    (fun alias -> GrafiteAst.Alias (dummy_floc, alias))
+    (aliases_of_environment env)
+
 let pp_environment env =
-  let aliases =
-    Environment.fold
-      (fun domain_item (dsc, _) acc ->
-        let s =
-          match domain_item with
-          | Id id ->
-              GrafiteAstPp.pp_alias (GrafiteAst.Ident_alias (id, dsc)) ^ "."
-          | Symbol (symb, i) ->
-              GrafiteAstPp.pp_alias (GrafiteAst.Symbol_alias (symb, i, dsc))
-              ^ "."
-          | Num i ->
-              GrafiteAstPp.pp_alias (GrafiteAst.Number_alias (i, dsc)) ^ "."
-        in
-        s :: acc)
-      env []
+  let aliases = aliases_of_environment env in
+  let strings =
+    List.map (fun alias -> GrafiteAstPp.pp_alias alias ^ ".") aliases
   in
-  String.concat "\n" (List.sort compare aliases) ^
-   (if aliases = [] then "" else "\n")
+  String.concat "\n" (List.sort compare strings)