X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matitaB%2Fcomponents%2Fdisambiguation%2Fdisambiguate.mli;h=5df0bffcc435a2520bae8b95f29cd56d8b3781c9;hb=41b61472d2c475e0f69e3dfc85539da3ad2bac1e;hp=bb20ff86635ca1ec53a6b218b610c7f36b97f2a7;hpb=6d4277977478ef9bcadaffbef3d4bb04ac0250a5;p=helm.git

diff --git a/matitaB/components/disambiguation/disambiguate.mli b/matitaB/components/disambiguation/disambiguate.mli
index bb20ff866..5df0bffcc 100644
--- a/matitaB/components/disambiguation/disambiguate.mli
+++ b/matitaB/components/disambiguation/disambiguate.mli
@@ -25,24 +25,13 @@
 
 (** {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
-  * - environment patch
-  * - location
-  * - error message
-  * - significancy of the error message, if false the error is likely to be
-  *   useless for the final user ... *)
-exception NoWellTypedInterpretation of
- int *
- ((Stdpp.location list * string * string) list *
-  (DisambiguateTypes.domain_item * string) list *
-  (Stdpp.location * string) Lazy.t *
-  bool) list
+type ('alias,'ast_thing,'metasenv,'subst,'thing,'ugraph) disamb_result =
+  | Disamb_success of ('ast_thing * 'metasenv * 'subst * 'thing * 'ugraph) list 
+  | Disamb_failure of 
+      (('ast_thing * 'alias option * Stdpp.location * string) list * Stdpp.location) list
+
+exception NoWellTypedInterpretation of (Stdpp.location * string)
+
 exception PathNotWellFormed
 
 type 'a disambiguator_input = string * int * 'a
@@ -58,6 +47,7 @@ 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
 
@@ -76,6 +66,7 @@ val mono_uris_callback: DisambiguateTypes.interactive_user_uri_choice_type
   * 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:'alias1 DisambiguateTypes.InterprEnv.t ->
@@ -127,17 +118,21 @@ val disambiguate_thing:
       ('refined_thing, 'metasenv,'subst,'ugraph) test_result) ->
   visit:(pp_term:(NotationPt.term -> string) ->
          (NotationPt.term -> bool) -> 'ast_thing -> 
-        ((NotationPt.term -> 'ast_thing) * NotationPt.term) option) -> 
+        ((NotationPt.term -> 'ast_thing) * NotationPt.term * Stdpp.location) option) -> 
   mk_localization_tbl:(int -> 'cichash) ->
   'ast_thing disambiguator_input ->
-  ('ast_thing * 'metasenv * 'subst * 'refined_thing * 'ugraph) list * bool
+  (GrafiteAst.alias_spec,'ast_thing,'metasenv,'subst,'refined_thing,'ugraph) disamb_result 
+
+type 'ast marked_ast = 
+  (NotationPt.term -> 'ast) * NotationPt.term * Stdpp.location
 
 val bfvisit :
   pp_term:(NotationPt.term -> string) -> 
   (NotationPt.term -> bool) ->
-   NotationPt.term -> ((NotationPt.term -> NotationPt.term) * NotationPt.term) option
+   NotationPt.term -> (NotationPt.term marked_ast) option
 
 val bfvisit_obj :
   pp_term:(NotationPt.term -> string) -> 
   (NotationPt.term -> bool) ->
-   NotationPt.term NotationPt.obj -> ((NotationPt.term -> NotationPt.term NotationPt.obj) * NotationPt.term) option
+   NotationPt.term NotationPt.obj -> 
+  ((NotationPt.term NotationPt.obj) marked_ast) option