(* *)
(******************************************************************************)
-(** A widget to render sequents **)
+type mml_of_cic_sequent =
+ Cic.metasenv ->
+ int * Cic.context * Cic.term ->
+ Gdome.document *
+ ((Cic.id, Cic.term) Hashtbl.t *
+ (Cic.id, Cic.id option) Hashtbl.t *
+ (string, Cic.hypothesis) Hashtbl.t)
+
+type mml_of_cic_object =
+ explode_all:bool ->
+ UriManager.uri ->
+ Cic.annobj ->
+ (string, string) Hashtbl.t ->
+ (string, Cic2acic.anntypes) Hashtbl.t -> Gdome.document
-val use_stylesheets: bool ref;; (* false performs the transformations in OCaml*)
+(** A widget to render sequents **)
class sequent_viewer :
+ mml_of_cic_sequent:mml_of_cic_sequent ->
Gtk_mathview.math_view Gtk.obj ->
object
inherit GMathViewAux.multi_selection_math_view
end
val sequent_viewer :
+ mml_of_cic_sequent:mml_of_cic_sequent ->
?hadjustment:GData.adjustment ->
?vadjustment:GData.adjustment ->
?font_size:int ->
?log_verbosity:int ->
- ?border_width:int ->
?width:int ->
?height:int ->
?packing:(GObj.widget -> unit) ->
(** A widget to render proofs **)
class proof_viewer :
+ mml_of_cic_object:mml_of_cic_object ->
Gtk_mathview.math_view Gtk.obj ->
object
inherit GMathViewAux.single_selection_math_view
end
val proof_viewer :
+ mml_of_cic_object:mml_of_cic_object ->
?hadjustment:GData.adjustment ->
?vadjustment:GData.adjustment ->
?font_size:int ->
?log_verbosity:int ->
- ?border_width:int ->
?width:int ->
?height:int ->
?packing:(GObj.widget -> unit) ->
?show:bool ->
unit -> proof_viewer
+