X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fmatita%2FmatitaMathView.mli;h=8b5ca89acd1ced41d4f1aacf172244044021c260;hb=3c9c376401844c389d682ba835845443105e4b1a;hp=b7a18e920ed0b0cef08800c091979e6ad57eea8b;hpb=ac813b7e251e4bac1a8a16befa628203775771ca;p=helm.git diff --git a/helm/matita/matitaMathView.mli b/helm/matita/matitaMathView.mli index b7a18e920..8b5ca89ac 100644 --- a/helm/matita/matitaMathView.mli +++ b/helm/matita/matitaMathView.mli @@ -23,16 +23,27 @@ * http://helm.cs.unibo.it/ *) + (** multi selection gtkMathView which handle mactions and hyperlinks. Mactions + * are handled internally. Hyperlinks are handled by calling an user provided + * callback *) +class type clickable_math_view = + object + inherit GMathViewAux.multi_selection_math_view + + (** set hyperlink callback. None disable hyperlink handling *) + method set_href_callback: (UriManager.uri -> unit) option -> unit + end + class type proof_viewer = object - inherit GMathViewAux.single_selection_math_view + inherit clickable_math_view method load_proof: StatefulProofEngine.proof_status -> unit end class type sequent_viewer = object - inherit GMathViewAux.multi_selection_math_view + inherit clickable_math_view (** @return the list of selected terms. Selections which are not terms are * ignored *) @@ -53,6 +64,13 @@ class type sequents_viewer = method goto_sequent: int -> unit (* to be called _after_ load_sequents *) end +class type cicBrowser = + object + method load_uri: UriManager.uri -> unit + end + +(** {2 Constructors} *) + val proof_viewer: ?hadjustment:GData.adjustment -> ?vadjustment:GData.adjustment -> @@ -65,10 +83,6 @@ val proof_viewer: unit -> proof_viewer - (** singleton proof_viewer instance. - * Uses singleton GUI instance *) -val proof_viewer_instance: unit -> proof_viewer - val sequent_viewer: ?hadjustment:GData.adjustment -> ?vadjustment:GData.adjustment -> @@ -88,5 +102,13 @@ val sequents_viewer: unit -> sequents_viewer +val cicBrowser: unit -> cicBrowser + val mathViewer: unit -> MatitaTypes.mathViewer +(** {2 Singletons} *) + + (** singleton proof_viewer instance. + * Uses singleton GUI instance *) +val proof_viewer_instance: unit -> proof_viewer +