X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fdisambiguation%2FmultiPassDisambiguator.ml;h=63bcaa587197b08da14e9b211f2cb4688085016e;hb=4573f1fecaf83f4706f39702555d5319d132477b;hp=039fdd57a0518f0c06912e64f108fece9b2b0498;hpb=9a9c5b863f68367119450ae7b806d454ba1265e3;p=helm.git

diff --git a/helm/software/components/disambiguation/multiPassDisambiguator.ml b/helm/software/components/disambiguation/multiPassDisambiguator.ml
index 039fdd57a..63bcaa587 100644
--- a/helm/software/components/disambiguation/multiPassDisambiguator.ml
+++ b/helm/software/components/disambiguation/multiPassDisambiguator.ml
@@ -31,8 +31,6 @@ let debug = false;;
 let debug_print s =
  if debug then prerr_endline (Lazy.force s);;
 
-exception Ambiguous_input
-(* the integer is an offset to be added to each location *)
 exception DisambiguationError of
  int *
  ((Stdpp.location list * string * string) list *
@@ -40,52 +38,24 @@ exception DisambiguationError of
   (Stdpp.location * string) Lazy.t * bool) list list
   (** parameters are: option name, error message *)
 
-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
-      "matita.auto_disambiguation"
- then
-  function l -> l
- else
-  raise Ambiguous_input
-
-let mono_interp_callback _ _ _ = raise Ambiguous_input
-
-let _choose_uris_callback = ref mono_uris_callback
-let _choose_interp_callback = ref mono_interp_callback
-let set_choose_uris_callback f = _choose_uris_callback := f
-let set_choose_interp_callback f = _choose_interp_callback := f
-
-module Callbacks =
-  struct
-    let interactive_user_uri_choice = !_choose_uris_callback
-
-    let interactive_interpretation_choice interp =
-      !_choose_interp_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"
-      * query is a syntax error *)
-  end
-  
-module Disambiguator = Disambiguate.Make (Callbacks)
-
 (* implement module's API *)
 
 let only_one_pass = ref false;;
+let use_library = ref false;;
 
 let passes () = (* <fresh_instances?, aliases, coercions?> *)
  if !only_one_pass then
   [ (true, `Mono, false) ]
+ else if !use_library then
+  [ (true, `Library, false); 
+      (* for demo to reduce the number of interpretations *)
+    (true, `Library, true);
+  ]
  else
   [ (true, `Mono, false);
     (true, `Multi, false);
     (true, `Mono, true);
     (true, `Multi, true);
-    (true, `Library, false); 
-      (* for demo to reduce the number of interpretations *)
-    (true, `Library, true);
   ]
 ;;
 
@@ -175,16 +145,15 @@ let disambiguate_thing ~description_of_alias ~passes ~aliases ~universe ~f thing
 let disambiguate_thing ~passes ~freshen_thing ~context ~metasenv ~subst
   ~string_context_of_context ~initial_ugraph ~hint ~mk_implicit
   ~description_of_alias ~aliases ~universe ~lookup_in_library ~uri ~pp_thing
-  ~domain_of_thing ~interpretate_thing ~refine_thing ~localization_tbl thing
+  ~domain_of_thing ~interpretate_thing ~refine_thing ~mk_localization_tbl thing
  =
   let f ~fresh_instances ~aliases ~universe ~use_coercions (txt,len,thing) =
-    let thing = if fresh_instances then freshen_thing thing else thing
-    in
-     Disambiguator.disambiguate_thing
+    let thing = if fresh_instances then freshen_thing thing else thing in
+     Disambiguate.disambiguate_thing
       ~context ~metasenv ~subst ~use_coercions ~string_context_of_context
       ~initial_ugraph ~hint ~mk_implicit ~description_of_alias
       ~aliases ~universe ~lookup_in_library 
       ~uri ~pp_thing ~domain_of_thing ~interpretate_thing ~refine_thing 
-      ~localization_tbl (txt,len,thing)
+      ~mk_localization_tbl (txt,len,thing)
   in
   disambiguate_thing ~description_of_alias ~passes ~aliases ~universe ~f thing