X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matitaB%2Fcomponents%2Fdisambiguation%2Fdisambiguate.ml;h=a65dd3e5f78b55a4825141f2a5a5003fe626576c;hb=0e3d8e00433a9a4dd72310c1e889814848a96c10;hp=5ce1386aeb0b16a9aca5a0f4abbde42270d3afe9;hpb=988cf01c5bd740d6e75767327f201a3c43d635ed;p=helm.git

diff --git a/matitaB/components/disambiguation/disambiguate.ml b/matitaB/components/disambiguation/disambiguate.ml
index 5ce1386ae..a65dd3e5f 100644
--- a/matitaB/components/disambiguation/disambiguate.ml
+++ b/matitaB/components/disambiguation/disambiguate.ml
@@ -31,9 +31,6 @@ open DisambiguateTypes
 
 module Ast = NotationPt
 
-(* the integer is an offset to be added to each location *)
-exception Ambiguous_input
-(* the integer is an offset to be added to each location *)
 exception NoWellTypedInterpretation of
  int *
  ((Stdpp.location list * string * string) list *
@@ -51,6 +48,7 @@ type 'a disambiguator_input = string * int * 'a
 type domain = domain_tree list
 and domain_tree = Node of Stdpp.location list * domain_item * domain
 
+(*
 let mono_uris_callback ~selection_mode ?ok
           ?(enable_button_for_non_vars = true) ~title ~msg ~id =
  if Helm_registry.get_opt_default Helm_registry.get_bool ~default:true
@@ -60,8 +58,8 @@ let mono_uris_callback ~selection_mode ?ok
  else
   raise Ambiguous_input
 
-let mono_interp_callback _ _ _ = raise Ambiguous_input
-let mono_disamb_callback _ = raise Ambiguous_input
+let mono_interp_callback _ _ _ = assert false
+let mono_disamb_callback _ = assert false
 
 let _choose_uris_callback = ref mono_uris_callback
 let _choose_interp_callback = ref mono_interp_callback
@@ -73,6 +71,8 @@ let set_choose_disamb_callback f = _choose_disamb_callback := f
 let interactive_user_uri_choice = !_choose_uris_callback
 let interactive_interpretation_choice interp = !_choose_interp_callback interp
 let interactive_ast_choice interp = !_choose_disamb_callback interp
+*)
+
 let input_or_locate_uri ~(title:string) ?id () = None
   (* Zack: I try to avoid using this callback. I therefore assume that
   * the presence of an identifier that can't be resolved via "locate"
@@ -730,12 +730,13 @@ let disambiguate_thing
     in
     match res with
     | [] -> raise (NoWellTypedInterpretation (0,[]))
+    (* XXX : the boolean seems not to play a role any longer *)
     | [t] -> res,false
-    | _ ->
-       let choices = List.map (fun (t,_,_,_,_) -> pp_thing t) res in
+    | _ -> res, true
+       (* let choices = List.map (fun (t,_,_,_,_) -> pp_thing t) res in
        let user_choice = interactive_ast_choice choices in
        [ List.nth res user_choice ], true
        (* let pp_thing (t,_,_,_,_,_) = prerr_endline ("interpretation: " ^ (pp_thing t)) in
-         List.iter pp_thing res; res,true *)
+         List.iter pp_thing res; res,true *) *)
 ;;