Matitaweb: added preliminary support for interactive disambiguation.

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

diff --git a/matitaB/matita/matitaGui.ml b/matitaB/matita/matitaGui.ml
index 7a05e13ff6fd1492be3e5a1015a19cc7c414770c..759ffa5ff2c3290671e88e6f5a10d3ecab28e35a 100644 (file)
--- a/matitaB/matita/matitaGui.ml
+++ b/matitaB/matita/matitaGui.ml
@@ -1273,11 +1273,11 @@ let interactive_ast_choice () ts =
 
 let _ =
   (* disambiguator callbacks *)
-  Disambiguate.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 ());
   Disambiguate.set_choose_interp_callback (interactive_interp_choice ());
-  Disambiguate.set_choose_disamb_callback (interactive_ast_choice ());
+  Disambiguate.set_choose_disamb_callback (interactive_ast_choice ());*)
   (* gtk initialization *)
   GtkMain.Rc.add_default_file BuildTimeConf.gtkrc_file; (* loads gtk rc *)
   ignore (GMain.Main.init ())