(* *)
(******************************************************************************)
-(** A widget to render sequents **)
+type mml_of_cic_sequent =
+ Cic.metasenv ->
+ int * Cic.context * Cic.term ->
+ Gdome.document *
+ (Cic.annconjecture *
+ ((Cic.id, Cic.term) Hashtbl.t *
+ (Cic.id, Cic.id option) Hashtbl.t *
+ (string, Cic.hypothesis) Hashtbl.t *
+ (Cic.id, string) Hashtbl.t))
+
+
+type mml_of_cic_object =
+ Cic.obj ->
+ Gdome.document *
+ (Cic.annobj *
+ ((Cic.id, Cic.term) Hashtbl.t *
+ (Cic.id, Cic.id option) Hashtbl.t *
+ (Cic.id, Cic.conjecture) Hashtbl.t *
+ (Cic.id, Cic.hypothesis) Hashtbl.t *
+ (Cic.id, string) Hashtbl.t *
+ (Cic.id, Cic2acic.anntypes) Hashtbl.t))
-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
(* load_proof also returns the annotated cic term and the *)
(* ids_to_inner_types and ids_to_inner_sorts maps. *)
method load_proof :
- UriManager.uri -> Cic.obj ->
+ Cic.obj ->
Cic.annobj * (Cic.id, Cic2acic.anntypes) Hashtbl.t *
(Cic.id, string) Hashtbl.t
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
+