(** {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 =