X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaTypes.mli;h=b165740aade4081290fd3851568998eee98dd49b;hb=51971de8dfcf257680cf38f01f9bf53d9912a498;hp=b0830c70928b09f4b1beea6b28d6287ea3bb8b3d;hpb=d0991ea0c7c83c100b2d223644cb2f11a8554fa1;p=helm.git

diff --git a/helm/matita/matitaTypes.mli b/helm/matita/matitaTypes.mli
index b0830c709..b165740aa 100644
--- a/helm/matita/matitaTypes.mli
+++ b/helm/matita/matitaTypes.mli
@@ -153,11 +153,21 @@ class type interpreter =
 
 (** {2 MathML widgets} *)
 
+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 =