From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Thu, 4 Dec 2008 12:36:44 +0000 (+0000)
Subject: Bug fixed: pretty-printing of aliases when the OK button is pressed in the
X-Git-Tag: make_still_working~4460
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=9ead65f0b6b17fc8f01ffcb977c3c252594724a9;p=helm.git

Bug fixed: pretty-printing of aliases when the OK button is pressed in the
ambiguous error window.
---

diff --git a/helm/software/components/lexicon/disambiguatePp.ml b/helm/software/components/lexicon/disambiguatePp.ml
index 5f6512477..a8590cfdf 100644
--- a/helm/software/components/lexicon/disambiguatePp.ml
+++ b/helm/software/components/lexicon/disambiguatePp.ml
@@ -27,7 +27,7 @@
 
 open DisambiguateTypes
 
-let alias_of_domain_and_codomain_items domain_item (dsc,_) =
+let alias_of_domain_and_desc domain_item dsc =
  match domain_item with
     Id id -> LexiconAst.Ident_alias (id, dsc)
   | Symbol (symb, i) -> LexiconAst.Symbol_alias (symb, i, dsc)
@@ -36,15 +36,9 @@ let alias_of_domain_and_codomain_items domain_item (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
+      alias_of_domain_and_desc domain_item (fst 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 = aliases_of_environment env in
   let strings =
diff --git a/helm/software/components/lexicon/disambiguatePp.mli b/helm/software/components/lexicon/disambiguatePp.mli
index e85a28443..c41bf6d78 100644
--- a/helm/software/components/lexicon/disambiguatePp.mli
+++ b/helm/software/components/lexicon/disambiguatePp.mli
@@ -23,9 +23,7 @@
  * http://helm.cs.unibo.it/
  *)
 
-val aliases_of_domain_and_codomain_items_list:
-  (DisambiguateTypes.domain_item * 
-   Cic.term DisambiguateTypes.codomain_item) list ->
-    LexiconAst.alias_spec list
+val alias_of_domain_and_desc:
+  DisambiguateTypes.domain_item -> string -> LexiconAst.alias_spec
 
 val pp_environment: Cic.term DisambiguateTypes.environment -> string
diff --git a/helm/software/matita/matitaGui.ml b/helm/software/matita/matitaGui.ml
index eb0d83bc7..5200a21ba 100644
--- a/helm/software/matita/matitaGui.ml
+++ b/helm/software/matita/matitaGui.ml
@@ -328,8 +328,8 @@ let rec interactive_error_interp ~all_passes
              ("" ::
                List.map
                 (fun k,desc -> 
-                  let id = DisambiguateTypes.string_of_domain_item k in
-                   LexiconAstPp.pp_alias (LexiconAst.Ident_alias (id,desc)))
+                  let alias = DisambiguatePp.alias_of_domain_and_desc k desc in
+                   LexiconAstPp.pp_alias alias)
                 diff) ^ "\n"
            in
             source_buffer#insert