X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaMathView.mli;h=ea0c077d842ef2c7ca9731df7f4d4395b79fb277;hb=aa0d60227b785da3355b31519ba11cb4fbd2c925;hp=0ed1a4573725e0cc0336a0a8eca8bbe2b5870bc6;hpb=fd96ce8e13f4f9adbeef2d9feb32f94dfcfaadad;p=helm.git diff --git a/helm/matita/matitaMathView.mli b/helm/matita/matitaMathView.mli index 0ed1a4573..ea0c077d8 100644 --- a/helm/matita/matitaMathView.mli +++ b/helm/matita/matitaMathView.mli @@ -1,4 +1,4 @@ -(* Copyright (C) 2004, HELM Team. +(* Copyright (C) 2004-2005, HELM Team. * * This file is part of HELM, an Hypertextual, Electronic * Library of Mathematics, developed at the Computer Science @@ -23,19 +23,10 @@ * http://helm.cs.unibo.it/ *) -val proof_viewer: - ?hadjustment:GData.adjustment -> - ?vadjustment:GData.adjustment -> - ?font_size:int -> - ?log_verbosity:int -> - ?width:int -> - ?height:int -> - ?packing:(GObj.widget -> unit) -> - ?show:bool -> - unit -> - MatitaTypes.proof_viewer +(** {2 Constructors} *) -val sequent_viewer: + (** meta constructor *) +type 'widget constructor = ?hadjustment:GData.adjustment -> ?vadjustment:GData.adjustment -> ?font_size:int -> @@ -45,11 +36,52 @@ val sequent_viewer: ?packing:(GObj.widget -> unit) -> ?show:bool -> unit -> - MatitaTypes.sequent_viewer + 'widget -val sequents_viewer: +val clickableMathView: MatitaGuiTypes.clickableMathView constructor + +val cicMathView: MatitaGuiTypes.cicMathView constructor + +val sequentsViewer: notebook:GPack.notebook -> - sequent_viewer:MatitaTypes.sequent_viewer -> + cicMathView:MatitaGuiTypes.cicMathView -> unit -> - MatitaTypes.sequents_viewer + MatitaGuiTypes.sequentsViewer + +val cicBrowser: unit -> MatitaGuiTypes.cicBrowser + +(** {2 MathView wide functions} *) +(* TODO ZACK consider exporting here a single function which return a list of + * MatitaGuiTypes.clickableMathView and act on them externally ... *) + +val increase_font_size: unit -> unit +val decrease_font_size: unit -> unit +val reset_font_size: unit -> unit + +val refresh_all_browsers: unit -> unit (** act on all cicBrowsers *) +val update_font_sizes: unit -> unit + + (** {3 Clipboard & Selection handling} *) + +val has_selection: unit -> bool + + (** fills the clipboard with the current selection + * @raise Failure "no selection" *) +val copy_selection: unit -> unit +val has_clipboard: unit -> bool (** clipboard is not empty *) +val empty_clipboard: unit -> unit (** empty the clipboard *) + + (** @raise Failure "empty clipboard" *) +val paste_clipboard: MatitaGuiTypes.paste_kind -> string + +(** {2 Singleton instances} *) + +val cicMathView_instance: unit -> MatitaGuiTypes.cicMathView +val sequentsViewer_instance: unit -> MatitaGuiTypes.sequentsViewer + +val mathViewer: unit -> MatitaTypes.mathViewer + +(** {2 Initialization} *) + +val set_gui: MatitaGuiTypes.gui -> unit