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

diff --git a/helm/matita/matitaTypes.mli b/helm/matita/matitaTypes.mli
index cc91486d6..b165740aa 100644
--- a/helm/matita/matitaTypes.mli
+++ b/helm/matita/matitaTypes.mli
@@ -153,10 +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 checkTerm: term_source -> unit
+  end
+
+class type cicBrowser =
+  object
+    method loadUri: string -> unit
+    method loadTerm: term_source -> unit
   end
 
 type mml_of_cic_sequent =