X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2FmatitaGuiTypes.mli;h=ddd08caf635a113203a4ff071c0fe7fc5cf2582c;hb=39b205d12af34c0c8d6e691da2628bc386b70cf2;hp=ae0bab1c24e63abfa5f1aead2645321cde5c1786;hpb=a22f5e32e698c3874ded926bd7dabc19719098f3;p=helm.git diff --git a/matita/matita/matitaGuiTypes.mli b/matita/matita/matitaGuiTypes.mli index ae0bab1c2..ddd08caf6 100644 --- a/matita/matita/matitaGuiTypes.mli +++ b/matita/matita/matitaGuiTypes.mli @@ -109,8 +109,8 @@ object method load_root : root:string -> unit method remove_selections: unit - method set_selection: Gdome.element option -> unit - method get_selections: Gdome.element list + method set_selection: unit option -> unit + method get_selections: unit list method set_font_size: int -> unit @@ -130,12 +130,10 @@ object inherit clickableMathView (** load a sequent and render it into parent widget *) - method load_sequent: Cic.metasenv -> int -> unit method nload_sequent: - #NCicCoercion.status -> NCic.metasenv -> NCic.substitution -> int -> unit + #ApplyTransformation.status -> NCic.metasenv -> NCic.substitution -> int -> unit - method load_object: Cic.obj -> unit - method load_nobject: #NCicCoercion.status -> NCic.obj -> unit + method load_nobject: #ApplyTransformation.status -> NCic.obj -> unit end class type sequentsViewer = @@ -143,11 +141,9 @@ object method reset: unit method load_logo: unit method load_logo_with_qed: unit - method load_sequents: - #NCicCoercion.status -> GrafiteTypes.incomplete_proof -> unit method nload_sequents: #NTacStatus.tac_status -> unit method goto_sequent: - #NCicCoercion.status -> int -> unit (* to be called _after_ load_sequents *) + #ApplyTransformation.status -> int -> unit (* to be called _after_ load_sequents *) method cicMathView: cicMathView end