- (string, string) Hashtbl.t ->
- (string, Cic2acic.anntypes) Hashtbl.t -> Gdome.document
-
-class type sequent_viewer =
- object
- inherit GMathViewAux.multi_selection_math_view
-
- (** @return the list of selected terms. Selections which are not terms are
- * ignored *)
- method get_selected_terms: Cic.term list
-
- (** @return the list of selected hypothese. Selections which are not
- * hypotheses are ignored *)
- method get_selected_hypotheses: Cic.hypothesis list
-
- (** load a sequent and render it into parent widget *)
- method load_sequent: Cic.metasenv -> Cic.conjecture -> unit
- end
-
-class type proof_viewer =
- object
- inherit GMathViewAux.single_selection_math_view
-
- (** @return the annotated cic term and the ids_to_inner_types and
- * ids_to_inner_sorts maps *)
- method load_proof :
- UriManager.uri -> Cic.obj ->
- Cic.annobj * (Cic.id, Cic2acic.anntypes) Hashtbl.t *
- (Cic.id, string) Hashtbl.t
-
- end
-
-(** {2 shorthands} *)