X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matitaB%2Fmatita%2FmatitaGui.ml;h=759ffa5ff2c3290671e88e6f5a10d3ecab28e35a;hb=b0c6bbd5db69489a5ebd1b36de6685fa6de441b3;hp=cb7c63bac3ab49aa0d01caf02597a9578cdf3ba9;hpb=cacbe3c6493ddce76c4c13379ade271d8dd172e8;p=helm.git

diff --git a/matitaB/matita/matitaGui.ml b/matitaB/matita/matitaGui.ml
index cb7c63bac..759ffa5ff 100644
--- a/matitaB/matita/matitaGui.ml
+++ b/matitaB/matita/matitaGui.ml
@@ -378,11 +378,16 @@ let interactive_error_interp ~all_passes
                   let alias =
                    match k with
                    | DisambiguateTypes.Id id ->
+                       (* 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"
@@ -1250,12 +1255,29 @@ let interactive_interp_choice () text prefix_len choices =
  in
   classify example_interp [] enumerated_choices
 
+let interactive_ast_choice () ts =
+  let choice =
+    interactive_string_choice
+     "" 0 ~title:"Ambiguous input"
+     ~msg:("Choose an interpretation") () ~id:"" [] ts
+  in
+  let choice = match choice with
+  | [c] -> c
+  | _ -> assert false
+  in
+  let rec posn x = function
+  | [] -> assert false
+  | he::tl -> if he = x then 0 else 1 + posn x tl
+  in
+  posn 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 ());*)
   (* gtk initialization *)
   GtkMain.Rc.add_default_file BuildTimeConf.gtkrc_file; (* loads gtk rc *)
   ignore (GMain.Main.init ())