]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/matita/matitaMathView.mli
fixed whelp bar
[helm.git] / helm / matita / matitaMathView.mli
index da187a7c5988d340890e2e1511c4167988b47ecb..aa9d38ded1db2a0522b72d2a838081c5b5b7f6dd 100644 (file)
@@ -59,16 +59,12 @@ class type sequentsViewer =
 
 exception Browser_failure of string
 
-type term_source =
-  [ `Ast of DisambiguateTypes.term
-  | `Cic of Cic.term * Cic.metasenv
-  | `String of string
-  ]
 
 class type cicBrowser =
 object
-  method loadUri: string -> unit
-  method loadTerm: term_source -> unit
+  method load: MatitaTypes.mathViewer_entry -> unit
+  (* method loadList: string list -> MatitaTypes.mathViewer_entry -> unit *)
+  method loadInput: string -> unit
 end
 
 (** {2 Constructors} *)
@@ -105,3 +101,5 @@ val refresh_all_browsers: unit -> unit
 val sequentViewer_instance: unit -> sequentViewer
 val sequentsViewer_instance: unit -> sequentsViewer
 
+val mathViewer: unit -> MatitaTypes.mathViewer
+