X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fmatita%2FmatitaTypes.ml;h=bfdb99904a05a7ba88c4d5dbef44e9fb49eeb151;hb=cc465115cdeea9819f43a5ad219b07c4f928c43a;hp=acae4c9dfe2d4d5cbd89da094823fb4c15a81d67;hpb=26cace1b5a8a80b83d6a974c222ef1a07d561c30;p=helm.git

diff --git a/helm/matita/matitaTypes.ml b/helm/matita/matitaTypes.ml
index acae4c9df..bfdb99904 100644
--- a/helm/matita/matitaTypes.ml
+++ b/helm/matita/matitaTypes.ml
@@ -32,7 +32,6 @@ let error s = raise (Failure s)
 let warning s = prerr_endline ("MATITA WARNING: " ^ s)
 
 exception No_proof  (** no current proof is available *)
-exception No_choice (** no choice was made by the user *)
 
 class type observer =
   (* "observer" pattern *)
@@ -71,16 +70,22 @@ class type disambiguator =
     method parserr: parserr
     method setParserr: parserr -> unit
 
+    method env: DisambiguateTypes.environment
+    method setEnv: DisambiguateTypes.environment -> unit
+
+      (* TODO Zack: as long as matita doesn't support MDI inteface,
+      * disambiguateTerm will return a single term *)
+      (** @param env defaults to self#env *)
     method disambiguateTerm:
-      context:Cic.context -> metasenv:Cic.metasenv ->
+      ?context:Cic.context -> ?metasenv:Cic.metasenv ->
       ?env:DisambiguateTypes.environment ->
         char Stream.t ->
-          (DisambiguateTypes.environment * Cic.metasenv * Cic.term) list
+          (DisambiguateTypes.environment * Cic.metasenv * Cic.term)
     method disambiguateTermAst:
-      context:Cic.context -> metasenv:Cic.metasenv ->
+      ?context:Cic.context -> ?metasenv:Cic.metasenv ->
       ?env:DisambiguateTypes.environment ->
         DisambiguateTypes.term ->
-          (DisambiguateTypes.environment * Cic.metasenv * Cic.term) list
+          (DisambiguateTypes.environment * Cic.metasenv * Cic.term)
   end
 
 (** {2 shorthands} *)