snapshot, notably:

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

diff --git a/helm/matita/matitaTypes.ml b/helm/matita/matitaTypes.ml
index cd9d34f0852e5fe9d9f3f327b5597199eb1da307..4631fa351a23749905cd36e1f03eab5bd8b032ab 100644 (file)
--- a/helm/matita/matitaTypes.ml
+++ b/helm/matita/matitaTypes.ml
@@ -55,6 +55,15 @@ class type parserr =  (* "parser" is a keyword :-( *)
     method parseTactical: char Stream.t -> DisambiguateTypes.tactical
   end
 
+  (* subset of MatitaConsole.console methods needed by MatitaInterpreter *)
+class type console =
+  object
+    method echo_message   : string -> unit
+    method echo_error     : string -> unit
+    method clear          : unit -> unit
+    method wrap_exn       : (unit -> unit) -> bool
+  end
+
 class type disambiguator =
   object
     method parserr: parserr
@@ -81,6 +90,16 @@ class type disambiguator =
       ?env:DisambiguateTypes.environment ->
         DisambiguateTypes.term ->
           (DisambiguateTypes.environment * Cic.metasenv * Cic.term * CicUniv.universe_graph) 
+
+      (** as disambiguateTermAst, but disambiguate a list of ASTs at once. All
+      * AST should be closed hence no context param is permitted on this method
+      *)
+    method disambiguateTermAsts:
+      ?metasenv:Cic.metasenv ->
+      ?env:DisambiguateTypes.environment ->
+      DisambiguateTypes.term list ->
+          (DisambiguateTypes.environment * Cic.metasenv * Cic.term list *
+          CicUniv.universe_graph)
   end
 
 (*