snapshot, notably:

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

diff --git a/helm/matita/matitaTypes.ml b/helm/matita/matitaTypes.ml
index c49bce0040049595cbcceda5b405559dc4bb713b..5d6b8e99d1c83a7e2d8a2ec45448f82a1ef74af4 100644 (file)
--- a/helm/matita/matitaTypes.ml
+++ b/helm/matita/matitaTypes.ml
@@ -43,6 +43,8 @@ let explain = function
   | CicTextualParser2.Parse_error (floc, msg) ->
       let (x, y) = CicAst.loc_of_floc floc in
       sprintf "parse error at character %d-%d: %s" x y msg
+  | CicEnvironment.Object_not_found uri ->
+      sprintf "object not found: %s" (UriManager.string_of_uri uri)
   | exn -> sprintf "Uncaught exception: %s" (Printexc.to_string exn)
 
 exception No_proof
@@ -132,11 +134,21 @@ class type interpreter =
     method reset : unit
   end
 
+type term_source =
+  [ `Ast of DisambiguateTypes.term
+  | `Cic of Cic.term
+  | `String of string
+  ]
+
 class type mathViewer =
   object
-    method checkTerm: Cic.conjecture -> Cic.metasenv -> unit
-    method unload: unit -> unit
-    method set_href_callback: (UriManager.uri -> unit) option -> unit
+    method checkTerm: term_source -> unit
+  end
+
+class type cicBrowser =
+  object
+    method loadUri: string -> unit
+    method loadTerm: term_source -> unit
   end
 
 type mml_of_cic_sequent =