- added pack/unpack over AST of terms

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

diff --git a/helm/matita/matitaTypes.ml b/helm/matita/matitaTypes.ml
index bea4377e6112db7b4802b125d84b9baa072a3d12..cd9d34f0852e5fe9d9f3f327b5597199eb1da307 100644 (file)
--- a/helm/matita/matitaTypes.ml
+++ b/helm/matita/matitaTypes.ml
@@ -35,6 +35,10 @@ let debug_print s =
 
 exception No_proof  (** no current proof is available *)
 
+exception Cancel
+exception Unbound_identifier of string
+
+(*
 let untitled_con_uri = UriManager.uri_of_string "cic:/untitled.con"
 let untitled_def_uri = UriManager.uri_of_string "cic:/untitled.ind"
 
@@ -42,6 +46,8 @@ let unopt_uri ?(kind = `Con) = function
   | Some uri -> uri
   | None ->
       (match kind with `Con -> untitled_con_uri | `Def -> untitled_def_uri)
+*)
+let unopt_uri = function Some uri -> uri | None -> assert false
 
 class type parserr =  (* "parser" is a keyword :-( *)
   object
@@ -68,13 +74,13 @@ class type disambiguator =
       ?context:Cic.context -> ?metasenv:Cic.metasenv ->
       ?env:DisambiguateTypes.environment ->
         char Stream.t ->
-          (DisambiguateTypes.environment * Cic.metasenv * Cic.term)
+          (DisambiguateTypes.environment * Cic.metasenv * Cic.term * CicUniv.universe_graph)
       (** @param env @see disambiguateTerm above *)
     method disambiguateTermAst:
       ?context:Cic.context -> ?metasenv:Cic.metasenv ->
       ?env:DisambiguateTypes.environment ->
         DisambiguateTypes.term ->
-          (DisambiguateTypes.environment * Cic.metasenv * Cic.term)
+          (DisambiguateTypes.environment * Cic.metasenv * Cic.term * CicUniv.universe_graph) 
   end
 
 (*
@@ -123,17 +129,20 @@ class type interpreter =
     method reset: unit  (** return the interpreter to the initial state *)
 
       (** parse a single phrase contained in the input string. Additional
-      * garbage at the end of the phrase is ignored *)
-    method evalPhrase: string -> unit
+      * garbage at the end of the phrase is ignored
+      * @return true if no exception has been raised by the evaluation, false
+      * otherwise
+      *)
+    method evalPhrase: string -> bool
+
+      (** as above, evaluating a command/tactics AST *)
+    method evalAst: DisambiguateTypes.tactical -> bool
+
+      (** offset from the starting of the last string parser by evalPhrase where
+      * parsing stop.
+      * @raise Failure when no offset has been recorded *)
+    method endOffset: int
 
-(*
-      (** eval zero or more phrases contained in the input string. Additional
-      * garbage contained at the end of the last phrase is ignored.
-      * @return offset from the beginning of the string pointing to the end of
-      * the last parsed phrase. Next invocations of evalAll should start from
-      * there *)
-    method evalAll: string -> int
-*)
   end
 
 (** {2 MathML widgets} *)