X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaMathView.mli;h=cdc9a8d65ead9e96fbb9eafadad7cea346b397ce;hb=eac74259f5a0aaa8056791876284c897a6827c24;hp=8b5ca89acd1ced41d4f1aacf172244044021c260;hpb=e3c0cc9893402419e363ad6616a599f194438273;p=helm.git diff --git a/helm/matita/matitaMathView.mli b/helm/matita/matitaMathView.mli index 8b5ca89ac..cdc9a8d65 100644 --- a/helm/matita/matitaMathView.mli +++ b/helm/matita/matitaMathView.mli @@ -34,13 +34,6 @@ class type clickable_math_view = method set_href_callback: (UriManager.uri -> unit) option -> unit end -class type proof_viewer = - object - inherit clickable_math_view - - method load_proof: StatefulProofEngine.proof_status -> unit - end - class type sequent_viewer = object inherit clickable_math_view @@ -64,14 +57,10 @@ 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: + (** meta constructor *) +type 'widget constructor = ?hadjustment:GData.adjustment -> ?vadjustment:GData.adjustment -> ?font_size:int -> @@ -81,19 +70,11 @@ val proof_viewer: ?packing:(GObj.widget -> unit) -> ?show:bool -> unit -> - proof_viewer + 'widget -val sequent_viewer: - ?hadjustment:GData.adjustment -> - ?vadjustment:GData.adjustment -> - ?font_size:int -> - ?log_verbosity:int -> - ?width:int -> - ?height:int -> - ?packing:(GObj.widget -> unit) -> - ?show:bool -> - unit -> - sequent_viewer +val clickable_math_view: clickable_math_view constructor + +val sequent_viewer: sequent_viewer constructor val sequents_viewer: notebook:GPack.notebook -> @@ -102,13 +83,15 @@ val sequents_viewer: unit -> sequents_viewer -val cicBrowser: unit -> cicBrowser - -val mathViewer: unit -> MatitaTypes.mathViewer +val cicBrowser: + disambiguator:MatitaTypes.disambiguator -> + unit -> + MatitaTypes.cicBrowser -(** {2 Singletons} *) +val refresh_all_browsers: unit -> unit - (** singleton proof_viewer instance. - * Uses singleton GUI instance *) -val proof_viewer_instance: unit -> proof_viewer +val mathViewer: + disambiguator:MatitaTypes.disambiguator -> + unit -> + MatitaTypes.mathViewer