First commit with new (incomplete) disambiguation engine.

[helm.git] / matitaB / matita / matitaGui.ml

diff --git a/matitaB/matita/matitaGui.ml b/matitaB/matita/matitaGui.ml
index cb7c63bac3ab49aa0d01caf02597a9578cdf3ba9..fbf9247e210f3e509fdb588f51f1577cf9869fcd 100644 (file)
--- a/matitaB/matita/matitaGui.ml
+++ b/matitaB/matita/matitaGui.ml
@@ -377,12 +377,17 @@ let interactive_error_interp ~all_passes
                 (fun k,desc -> 
                   let alias =
                    match k with
-                   | DisambiguateTypes.Id id ->
+                   | DisambiguateTypes.Id (id,_opturi) ->
+                       (* XXX we don't have an uri to put into Ident_alias! 
+                        * then we use the description??
+                        * what does this code mean?? *)
+                       (* FIXME we are not using info from the domain_item to
+                        * fill in the alias_spec *)
                        GrafiteAst.Ident_alias (id, desc)
-                   | DisambiguateTypes.Symbol (symb, i)-> 
-                       GrafiteAst.Symbol_alias (symb, i, desc)
-                   | DisambiguateTypes.Num i ->
-                       GrafiteAst.Number_alias (i, desc)
+                   | DisambiguateTypes.Symbol (symb, _)-> 
+                       GrafiteAst.Symbol_alias (symb, None, desc)
+                   | DisambiguateTypes.Num _ ->
+                       GrafiteAst.Number_alias (None,desc)
                   in
                    GrafiteAstPp.pp_alias alias)
                 diff) ^ "\n"