X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fgrafite_parser%2FgrafiteDisambiguator.ml;h=d9de808b019ea796235e551e4c33a591453f02f1;hb=c04c7b4635b43c03f305bb1feadcb89496355111;hp=2803c88f6add6484bbf1ca31da4c658d5aa1fd21;hpb=ce879c4d8bc743d1442ab7361ee7d5e3a8309212;p=helm.git

diff --git a/helm/software/components/grafite_parser/grafiteDisambiguator.ml b/helm/software/components/grafite_parser/grafiteDisambiguator.ml
index 2803c88f6..d9de808b0 100644
--- a/helm/software/components/grafite_parser/grafiteDisambiguator.ml
+++ b/helm/software/components/grafite_parser/grafiteDisambiguator.ml
@@ -37,7 +37,9 @@ exception Unbound_identifier of string
 type choose_uris_callback =
   id:string -> UriManager.uri list -> UriManager.uri list
 
-type choose_interp_callback = (string * string) list list -> int list
+type choose_interp_callback = 
+  string -> int -> 
+    (Token.flocation list * string * string) list list -> int list
 
 let mono_uris_callback ~id =
  if Helm_registry.get_opt_default Helm_registry.get_bool ~default:true
@@ -47,7 +49,7 @@ let mono_uris_callback ~id =
  else
   raise Ambiguous_input
 
-let mono_interp_callback _ = 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
@@ -63,12 +65,10 @@ module Callbacks =
     let interactive_interpretation_choice interp =
       !_choose_interp_callback interp
 
-    let input_or_locate_uri ~(title:string) ?id =
+    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 *)
-      let msg = match id with Some id -> id | _ -> "_" in
-      raise (Unbound_identifier msg)
   end
   
 module Disambiguator = Disambiguate.Make (Callbacks)
@@ -95,6 +95,8 @@ let disambiguate_thing ~aliases ~universe
       (true, multi_aliases, false);
       (true, mono_aliases, true);
       (true, multi_aliases, true);
+      (true, library, false); 
+        (* for demo to reduce the number of interpretations *)
       (true, library, true);
     ]
   in