X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_disambiguation%2FnGrafiteDisambiguator.ml;h=9aa41c52b97761a7eb80960aa54e57d8832811c0;hb=19e7a086a4efbb59452b10ed71f4914e92eb8986;hp=328856a0f0565bcb3d71d2863e37af60826228fe;hpb=1d212933a86f2820a151555516f7a53ab1c9f8e7;p=helm.git

diff --git a/helm/software/components/ng_disambiguation/nGrafiteDisambiguator.ml b/helm/software/components/ng_disambiguation/nGrafiteDisambiguator.ml
index 328856a0f..9aa41c52b 100644
--- a/helm/software/components/ng_disambiguation/nGrafiteDisambiguator.ml
+++ b/helm/software/components/ng_disambiguation/nGrafiteDisambiguator.ml
@@ -11,17 +11,11 @@
 
 (* $Id$ *)
 
-exception Ambiguous_input
 exception DisambiguationError of
  int *
  ((Stdpp.location list * string * string) list *
-  (DisambiguateTypes.domain_item * DisambiguateTypes.codomain_item) list *
+  (DisambiguateTypes.domain_item * string) list *
   (Stdpp.location * string) Lazy.t * bool) list list
-  (** parameters are: option name, error message *)
-type choose_uris_callback = id:string -> NUri.uri list -> NUri.uri list
-type choose_interp_callback = 
-  string -> int -> (Stdpp.location list * string * string) list list -> 
-    int list
 
 open Printf
 
@@ -29,32 +23,17 @@ let debug = false;;
 let debug_print s =
  if debug then prerr_endline (Lazy.force s);;
 
-let mono_uris_callback ~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 ~selection_mode ?ok
           ?(enable_button_for_non_vars = true) ~title ~msg ~id uris =
-              !_choose_uris_callback ~id uris
+              assert false
 
     let interactive_interpretation_choice interp =
-      !_choose_interp_callback interp
+            assert false
 
-    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 input_or_locate_uri ~(title:string) ?id () = 
+            assert false
   end
   
 module Disambiguator = NDisambiguate.Make (Callbacks)
@@ -63,8 +42,8 @@ let only_one_pass = ref false;;
 
 let disambiguate_thing ~aliases ~universe
   ~(f:?fresh_instances:bool ->
-      aliases:DisambiguateTypes.environment ->
-      universe:DisambiguateTypes.multiple_environment option ->
+      aliases:NCic.term DisambiguateTypes.environment ->
+      universe:NCic.term DisambiguateTypes.multiple_environment option ->
       'a -> 'b)
   ~(drop_aliases: ?minimize_instances:bool -> 'b -> 'b)
   ~(drop_aliases_and_clear_diff: 'b -> 'b)
@@ -126,11 +105,11 @@ let disambiguate_thing ~aliases ~universe
 type disambiguator_thing =
  { do_it :
     'a 'b.
-    aliases:DisambiguateTypes.environment ->
-    universe:DisambiguateTypes.multiple_environment option ->
+    aliases:NCic.term DisambiguateTypes.environment ->
+    universe:NCic.term DisambiguateTypes.multiple_environment option ->
     f:(?fresh_instances:bool ->
-       aliases:DisambiguateTypes.environment ->
-       universe:DisambiguateTypes.multiple_environment option ->
+       aliases:NCic.term DisambiguateTypes.environment ->
+       universe:NCic.term DisambiguateTypes.multiple_environment option ->
        'a -> 'b * bool) ->
     drop_aliases:(?minimize_instances:bool -> 'b * bool -> 'b * bool) ->
     drop_aliases_and_clear_diff:('b * bool -> 'b * bool) -> 'a -> 'b * bool
@@ -177,27 +156,27 @@ let drop_aliases ?(minimize_instances=false) (choices, user_asked) =
    in
     aux d
  in
-  (List.map (fun (d, a, b, c, e) -> minimize d, a, b, c, e) choices),
+  (List.map (fun (d, a, b, c) -> minimize d, a, b, c) choices),
   user_asked
 
 let drop_aliases_and_clear_diff (choices, user_asked) =
-  (List.map (fun (_, a, b, c, d) -> [], a, b, c, d) choices),
+  (List.map (fun (_, a, b, c) -> [], a, b, c) choices),
   user_asked
 
-let disambiguate_term ?fresh_instances ~dbd ~context ~metasenv ~subst ?goal ?initial_ugraph
+let disambiguate_term ~context ~metasenv ~subst ?goal
   ~aliases ~universe term
  =
-  assert (fresh_instances = None);
   let f =
-    Disambiguator.disambiguate_term ~dbd ~context ~metasenv ~subst ?goal ?initial_ugraph
+    Disambiguator.disambiguate_term ~context ~metasenv ~subst ?goal
+     ~lookup_in_library:(fun _ _ -> assert false)
   in
   disambiguate_thing.do_it ~aliases ~universe ~f ~drop_aliases
    ~drop_aliases_and_clear_diff term
 
-let disambiguate_obj ?fresh_instances ~dbd ~aliases ~universe ~uri obj =
+let disambiguate_obj ~aliases ~universe ~uri obj =
+        assert false (*
   assert (fresh_instances = None);
-  let f = Disambiguator.disambiguate_obj ~dbd ~uri in
+  let f = Disambiguator.disambiguate_obj ~uri ~lookup_in_library:(fun _ _ -> assert false) in
   disambiguate_thing.do_it ~aliases ~universe ~f ~drop_aliases
    ~drop_aliases_and_clear_diff obj
-
-let disambiguate_thing ~dbd = assert false 
+   *)