X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaTypes.ml;h=92fc79b7c288fb979f65d136eb510c148c04fee4;hb=e89486cad653803954662a5e543537acd49a866f;hp=4e81148c34f817e492b12f6c7d472e1c9f131b53;hpb=481992ea591bf53cba758a96e7d42e9cdce7e129;p=helm.git

diff --git a/helm/matita/matitaTypes.ml b/helm/matita/matitaTypes.ml
index 4e81148c3..92fc79b7c 100644
--- a/helm/matita/matitaTypes.ml
+++ b/helm/matita/matitaTypes.ml
@@ -36,7 +36,7 @@ let debug_print s =
 exception No_proof  (** no current proof is available *)
 
 let untitled_con_uri = UriManager.uri_of_string "cic:/untitled.con"
-let untitled_def_uri = UriManager.uri_of_string "cic:/untitled.def"
+let untitled_def_uri = UriManager.uri_of_string "cic:/untitled.ind"
 
 class type observer =
   (* "observer" pattern *)
@@ -80,12 +80,17 @@ class type disambiguator =
 
       (* TODO Zack: as long as matita doesn't support MDI inteface,
       * disambiguateTerm will return a single term *)
-      (** @param env defaults to self#env *)
+      (** @param env disambiguation environment. If this parameter is given the
+      * disambiguator act statelessly, that is internal disambiguation status
+      * want be changed but only returned. If this parameter is not given the
+      * internal one will be used and updated with the disambiguation status
+      * resulting from the disambiguation *)
     method disambiguateTerm:
       ?context:Cic.context -> ?metasenv:Cic.metasenv ->
       ?env:DisambiguateTypes.environment ->
         char Stream.t ->
           (DisambiguateTypes.environment * Cic.metasenv * Cic.term)
+      (** @param env @see disambiguateTerm above *)
     method disambiguateTermAst:
       ?context:Cic.context -> ?metasenv:Cic.metasenv ->
       ?env:DisambiguateTypes.environment ->
@@ -124,6 +129,21 @@ class type proof =
     method setStatus: proofStatus -> unit
   end
 
+type proof_handler =
+  { get_proof: unit -> proof; (* return current proof or fail *)
+    set_proof: proof option -> unit;  (* set a proof option as current proof *)
+    has_proof: unit -> bool;  (* check if a current proof is available or not *)
+    new_proof: proof -> unit; (* as a set_proof but takes care also to register
+                              observers *)
+    quit: unit -> unit
+  }
+
+  (** interpreter for toplevel phrases given via console *)
+class type interpreter =
+  object
+    method evalPhrase: string -> unit
+  end
+
 (** {2 shorthands} *)
 
 type namer = ProofEngineTypes.mk_fresh_name_type