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 5f6512477cdde03d860482790ce5bb566a534645..a8590cfdfcffd191b3826d18c95628635a03cb6d 100644 (file)
--- 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 e85a284437cd385b11747f31ba8611da3c7193ee..c41bf6d78b1dd21a654596767d498ddc5cb4d433 100644 (file)
--- 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 eb0d83bc7cbb8cf85ca9f8c5a425be0dc4e11c2c..5200a21baf371011478d6e840da52f61d3dd74f2 100644 (file)
--- 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