X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_disambiguation%2FdisambiguatePp.ml;h=b7c1012a8dc68474e2515f567320f82a4c7bbe8d;hb=7efb15b93cf42eae8b34a12a327ee7213c1dbecc;hp=24f9ea37ea1b319f166cc17090fa4ec42564df7c;hpb=35c68efd0a44da26d4aa6ae760ee03712b33dfed;p=helm.git

diff --git a/helm/ocaml/cic_disambiguation/disambiguatePp.ml b/helm/ocaml/cic_disambiguation/disambiguatePp.ml
index 24f9ea37e..b7c1012a8 100644
--- a/helm/ocaml/cic_disambiguation/disambiguatePp.ml
+++ b/helm/ocaml/cic_disambiguation/disambiguatePp.ml
@@ -28,6 +28,7 @@ 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 =
@@ -49,30 +50,34 @@ let parse_environment str =
           Num instance,
           DisambiguateChoices.lookup_num_by_dsc desc
      in
-      environment := Environment.cons key value !environment;
+      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 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 codomain_items acc ->
-        List.fold_left
-          (fun strings (dsc, _) ->
-            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 :: strings)
-          acc codomain_items)
-      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)
+