snapshot

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

diff --git a/helm/matita/matitaTypes.ml b/helm/matita/matitaTypes.ml
index 4e81148c34f817e492b12f6c7d472e1c9f131b53..27783ec675daab8b6732c9f113b2b3c9f3d6b0b1 100644 (file)
--- 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,12 @@ class type proof =
     method setStatus: proofStatus -> unit
   end
 
+  (** 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