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

diff --git a/helm/ocaml/cic_disambiguation/disambiguatePp.ml b/helm/ocaml/cic_disambiguation/disambiguatePp.ml
index d6a33cfae..c3a48e409 100644
--- a/helm/ocaml/cic_disambiguation/disambiguatePp.ml
+++ b/helm/ocaml/cic_disambiguation/disambiguatePp.ml
@@ -26,8 +26,9 @@
 open DisambiguateTypes
 
 let parse_environment str =
- let stream = Stream.of_string str in
+ let stream = Ulexing.from_utf8_string str in
  let environment = ref Environment.empty in
+ let multiple_environment = ref Environment.empty in
   try
     while true do
      let alias =
@@ -50,26 +51,33 @@ let parse_environment str =
           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
+   !environment, !multiple_environment
+
+let alias_of_domain_and_codomain_items domain_item (dsc,_) =
+ 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)
+
+let aliases_of_environment env =
+  Environment.fold
+    (fun domain_item codomain_item acc ->
+      alias_of_domain_and_codomain_items domain_item codomain_item::acc
+    ) env []
+
+let aliases_of_domain_and_codomain_items_list l =
+  List.fold_left
+    (fun acc (domain_item,codomain_item) ->
+      alias_of_domain_and_codomain_items domain_item codomain_item::acc
+    ) [] l
 
 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)
+  String.concat "\n" (List.sort compare strings)