snapshot

[helm.git] / helm / matita / matitaTypes.ml

diff --git a/helm/matita/matitaTypes.ml b/helm/matita/matitaTypes.ml
index acae4c9dfe2d4d5cbd89da094823fb4c15a81d67..bfdb99904a05a7ba88c4d5dbef44e9fb49eeb151 100644 (file)
--- 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} *)