X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fdisambiguation%2Fdisambiguate.mli;h=ffbdf884d17135de2a4ef128ce5ad9fd0fe13c94;hb=e9eda8f13045ff3d4f7b1ec93dec96e09bf65f1a;hp=5088f8a5f57e17259b586ee9c4a112f8b88c9147;hpb=9a9c5b863f68367119450ae7b806d454ba1265e3;p=helm.git

diff --git a/helm/software/components/disambiguation/disambiguate.mli b/helm/software/components/disambiguation/disambiguate.mli
index 5088f8a5f..ffbdf884d 100644
--- a/helm/software/components/disambiguation/disambiguate.mli
+++ b/helm/software/components/disambiguation/disambiguate.mli
@@ -25,6 +25,10 @@
 
 (** {2 Disambiguation interface} *)
 
+(** raised when ambiguous input is found but not expected (e.g. in the batch
+  * compiler) *)
+exception Ambiguous_input
+
 (* the integer is an offset to be added to each location *)
 (* list of located error messages, each list is a tuple:
   * - environment in string form
@@ -54,6 +58,22 @@ type ('term,'metasenv,'subst,'graph) test_result =
 
 exception Try_again of string Lazy.t
 
+val set_choose_uris_callback:
+  DisambiguateTypes.interactive_user_uri_choice_type -> unit
+
+val set_choose_interp_callback:
+  DisambiguateTypes.interactive_interpretation_choice_type -> unit
+
+(** @raise Ambiguous_input if called, default value for internal
+  * choose_uris_callback if not set otherwise with set_choose_uris_callback
+  * above *)
+val mono_uris_callback: DisambiguateTypes.interactive_user_uri_choice_type
+
+(** @raise Ambiguous_input if called, default value for internal
+  * choose_interp_callback if not set otherwise with set_choose_interp_callback
+  * above *)
+val mono_interp_callback: DisambiguateTypes.interactive_interpretation_choice_type
+
 val resolve : 
   env:'alias DisambiguateTypes.Environment.t ->
   mk_choice:('alias -> 'term DisambiguateTypes.codomain_item) ->
@@ -61,56 +81,45 @@ val resolve :
    [`Num_arg of string | `Args of 'term list] -> 'term
 
 val find_in_context: string -> string option list -> int
-val domain_of_ast_term: context:
-  string option list -> CicNotationPt.term -> domain
 val domain_of_term: context:
   string option list -> CicNotationPt.term -> domain
 val domain_of_obj: 
   context:string option list -> CicNotationPt.term CicNotationPt.obj -> domain
 
-module type Disambiguator =
-sig
-  val disambiguate_thing:
+val disambiguate_thing:
+  context:'context ->
+  metasenv:'metasenv ->
+  subst:'subst ->
+  use_coercions:bool ->
+  string_context_of_context:('context -> string option list) ->
+  initial_ugraph:'ugraph ->
+  expty: 'refined_thing option ->
+  mk_implicit:(bool -> 'alias) ->
+  description_of_alias:('alias -> string) ->
+  aliases:'alias DisambiguateTypes.Environment.t ->
+  universe:'alias list DisambiguateTypes.Environment.t option ->
+  lookup_in_library:(
+    DisambiguateTypes.interactive_user_uri_choice_type ->
+    DisambiguateTypes.input_or_locate_uri_type ->
+    DisambiguateTypes.Environment.key ->
+    'alias list) ->
+  uri:'uri ->
+  pp_thing:('ast_thing -> string) ->
+  domain_of_thing:(context: string option list -> 'ast_thing -> domain) ->
+  interpretate_thing:(
     context:'context ->
-    metasenv:'metasenv ->
-    subst:'subst ->
-    use_coercions:bool ->
-    string_context_of_context:('context -> string option list) ->
-    initial_ugraph:'ugraph ->
-    hint: 
-      ('metasenv -> 'raw_thing -> 'raw_thing) * 
-      (('refined_thing,'metasenv,'subst,'ugraph) test_result ->
-         ('refined_thing,'metasenv,'subst,'ugraph) test_result) ->
-    mk_implicit:(bool -> 'alias) ->
-    description_of_alias:('alias -> string) ->
-    aliases:'alias DisambiguateTypes.Environment.t ->
-    universe:'alias list DisambiguateTypes.Environment.t option ->
-    lookup_in_library:(
-      DisambiguateTypes.interactive_user_uri_choice_type ->
-      DisambiguateTypes.input_or_locate_uri_type ->
-      DisambiguateTypes.Environment.key ->
-      'alias list) ->
+    env:'alias DisambiguateTypes.Environment.t ->
     uri:'uri ->
-    pp_thing:('ast_thing -> string) ->
-    domain_of_thing:(context: string option list -> 'ast_thing -> domain) ->
-    interpretate_thing:(
-      context:'context ->
-      env:'alias DisambiguateTypes.Environment.t ->
-      uri:'uri ->
-      is_path:bool -> 
-      'ast_thing -> 
-      localization_tbl:'cichash -> 
-        'raw_thing) ->
-    refine_thing:(
-      'metasenv -> 'subst -> 'context -> 'uri -> use_coercions:bool ->
-      'raw_thing -> 'ugraph -> localization_tbl:'cichash -> 
-        ('refined_thing, 'metasenv,'subst,'ugraph) test_result) ->
-    localization_tbl:'cichash ->
-    string * int * 'ast_thing ->
-    ((DisambiguateTypes.Environment.key * 'alias) list * 
-     'metasenv * 'subst * 'refined_thing * 'ugraph)
-    list * bool
-end
-
-module Make (C : DisambiguateTypes.Callbacks) : Disambiguator
-
+    is_path:bool -> 
+    'ast_thing -> 
+    localization_tbl:'cichash -> 
+      'raw_thing) ->
+  refine_thing:(
+    'metasenv -> 'subst -> 'context -> 'uri -> use_coercions:bool ->
+    'raw_thing -> 'refined_thing option -> 'ugraph -> localization_tbl:'cichash -> 
+      ('refined_thing, 'metasenv,'subst,'ugraph) test_result) ->
+  mk_localization_tbl:(int -> 'cichash) ->
+  'ast_thing disambiguator_input ->
+  ((DisambiguateTypes.Environment.key * 'alias) list * 
+   'metasenv * 'subst * 'refined_thing * 'ugraph)
+  list * bool