(* *)
(******************************************************************************)
+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))
+
(** 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 :
- ?adjustmenth:GData.adjustment ->
- ?adjustmentv:GData.adjustment ->
+ mml_of_cic_sequent:mml_of_cic_sequent ->
+ ?hadjustment:GData.adjustment ->
+ ?vadjustment:GData.adjustment ->
?font_size:int ->
- ?font_manager:[ `font_manager_gtk | `font_manager_t1] ->
- ?border_width:int ->
+ ?log_verbosity: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 :
- ?adjustmenth:GData.adjustment ->
- ?adjustmentv:GData.adjustment ->
+ mml_of_cic_object:mml_of_cic_object ->
+ ?hadjustment:GData.adjustment ->
+ ?vadjustment:GData.adjustment ->
?font_size:int ->
- ?font_manager:[ `font_manager_gtk | `font_manager_t1] ->
- ?border_width:int ->
+ ?log_verbosity:int ->
?width:int ->
?height:int ->
?packing:(GObj.widget -> unit) ->
?show:bool ->
unit -> proof_viewer
+