removed spurious load of a local gTopLevel.conf.xml

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

diff --git a/helm/matita/matitaTypes.mli b/helm/matita/matitaTypes.mli
index b0830c70928b09f4b1beea6b28d6287ea3bb8b3d..b165740aade4081290fd3851568998eee98dd49b 100644 (file)
--- 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 =