new exception captured

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

diff --git a/helm/software/matita/matitaGui.ml b/helm/software/matita/matitaGui.ml
index eb0d83bc7cbb8cf85ca9f8c5a425be0dc4e11c2c..f68421e0cfe5483c7be23a2f989d42352852c5bc 100644 (file)
--- a/helm/software/matita/matitaGui.ml
+++ b/helm/software/matita/matitaGui.ml
@@ -328,8 +328,16 @@ 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 =
+                   match k with
+                   | DisambiguateTypes.Id id ->
+                       LexiconAst.Ident_alias (id, desc)
+                   | DisambiguateTypes.Symbol (symb, i)-> 
+                       LexiconAst.Symbol_alias (symb, i, desc)
+                   | DisambiguateTypes.Num i ->
+                       LexiconAst.Number_alias (i, desc)
+                  in
+                   LexiconAstPp.pp_alias alias)
                 diff) ^ "\n"
            in
             source_buffer#insert
@@ -1567,10 +1575,10 @@ let interactive_interp_choice () text prefix_len choices =
 
 let _ =
   (* disambiguator callbacks *)
-  MultiPassDisambiguator.set_choose_uris_callback
+  Disambiguate.set_choose_uris_callback
    (fun ~selection_mode ?ok ?(enable_button_for_non_vars=false) ~title ~msg ->
      interactive_uri_choice ~selection_mode ?ok_label:ok ~title ~msg ());
-  MultiPassDisambiguator.set_choose_interp_callback (interactive_interp_choice ());
+  Disambiguate.set_choose_interp_callback (interactive_interp_choice ());
   (* gtk initialization *)
   GtkMain.Rc.add_default_file BuildTimeConf.gtkrc_file; (* loads gtk rc *)
   GMathView.add_configuration_path BuildTimeConf.gtkmathview_conf;