From 513c7211bb07abd4c1da842a29c05301890aa73a Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Fri, 17 Dec 2010 22:45:29 +0000 Subject: [PATCH] This commit simplifies the interfaces of the various Widget-related .mli files, so that the same inferfaces can be used both for the MathMl widget and the textual widget. Practically, it is now sufficient to switch between two implementations of matitaMathView to change between MathML/textual. --- matita/matita/.depend | 20 ++++------- matita/matita/.depend.opt | 46 ++++++++++++------------- matita/matita/matita.ml | 5 --- matita/matita/matitaGuiTypes.mli | 43 ----------------------- matita/matita/matitaMathView.ml | 44 ++++++++++++++++++++---- matita/matita/matitaMathView.mli | 58 ++++---------------------------- matita/matita/matitaTypes.ml | 2 -- matita/matita/matitaTypes.mli | 2 -- 8 files changed, 73 insertions(+), 147 deletions(-) diff --git a/matita/matita/.depend b/matita/matita/.depend index b8de092d1..4b98fdf33 100644 --- a/matita/matita/.depend +++ b/matita/matita/.depend @@ -6,14 +6,8 @@ lablGraphviz.cmo: lablGraphviz.cmi lablGraphviz.cmx: lablGraphviz.cmi matitaclean.cmo: matitaMisc.cmi matitaInit.cmi matitaclean.cmi matitaclean.cmx: matitaMisc.cmx matitaInit.cmx matitaclean.cmi -matitacLib.cmo: matitaExcPp.cmi matitaEngine.cmi matitacLib.cmi -matitacLib.cmx: matitaExcPp.cmx matitaEngine.cmx matitacLib.cmi -matitac.cmo: matitadep.cmi matitaclean.cmi matitacLib.cmi matitaMisc.cmi \ - matitaInit.cmi -matitac.cmx: matitadep.cmx matitaclean.cmx matitacLib.cmx matitaMisc.cmx \ - matitaInit.cmx -matitadep.cmo: matitaMisc.cmi matitaInit.cmi matitadep.cmi -matitadep.cmx: matitaMisc.cmx matitaInit.cmx matitadep.cmi +matitac.cmo: matitaclean.cmi matitaMisc.cmi matitaInit.cmi matitaEngine.cmi +matitac.cmx: matitaclean.cmx matitaMisc.cmx matitaInit.cmx matitaEngine.cmx matitaEngine.cmo: matitaEngine.cmi matitaEngine.cmx: matitaEngine.cmi matitaExcPp.cmo: matitaEngine.cmi matitaExcPp.cmi @@ -48,10 +42,10 @@ matita.cmo: predefined_virtuals.cmi matitaTypes.cmi matitaScript.cmi \ matita.cmx: predefined_virtuals.cmx matitaTypes.cmx matitaScript.cmx \ matitaMathView.cmx matitaInit.cmx matitaGui.cmx matitaGtkMisc.cmx \ buildTimeConf.cmx -matitaScript.cmo: virtuals.cmi matitacLib.cmi matitaTypes.cmi \ - matitaGtkMisc.cmi matitaEngine.cmi buildTimeConf.cmo matitaScript.cmi -matitaScript.cmx: virtuals.cmx matitacLib.cmx matitaTypes.cmx \ - matitaGtkMisc.cmx matitaEngine.cmx buildTimeConf.cmx matitaScript.cmi +matitaScript.cmo: virtuals.cmi matitaTypes.cmi matitaGtkMisc.cmi \ + matitaEngine.cmi buildTimeConf.cmo matitaScript.cmi +matitaScript.cmx: virtuals.cmx matitaTypes.cmx matitaGtkMisc.cmx \ + matitaEngine.cmx buildTimeConf.cmx matitaScript.cmi matitaTypes.cmo: matitaTypes.cmi matitaTypes.cmx: matitaTypes.cmi predefined_virtuals.cmo: virtuals.cmi predefined_virtuals.cmi @@ -61,8 +55,6 @@ virtuals.cmx: virtuals.cmi applyTransformation.cmi: lablGraphviz.cmi: matitaclean.cmi: -matitacLib.cmi: -matitadep.cmi: matitaEngine.cmi: matitaExcPp.cmi: matitaGtkMisc.cmi: matitaGeneratedGui.cmo diff --git a/matita/matita/.depend.opt b/matita/matita/.depend.opt index a6f969454..c51561a1a 100644 --- a/matita/matita/.depend.opt +++ b/matita/matita/.depend.opt @@ -1,23 +1,17 @@ applyTransformation.cmo: applyTransformation.cmi applyTransformation.cmx: applyTransformation.cmi +applyTransformationMml.cmo: applyTransformationMml.cmi +applyTransformationMml.cmx: applyTransformationMml.cmi buildTimeConf.cmo: buildTimeConf.cmx: lablGraphviz.cmo: lablGraphviz.cmi lablGraphviz.cmx: lablGraphviz.cmi matitaclean.cmo: matitaMisc.cmi matitaInit.cmi matitaclean.cmi matitaclean.cmx: matitaMisc.cmx matitaInit.cmx matitaclean.cmi -matitacLib.cmo: matitaMisc.cmi matitaExcPp.cmi matitaEngine.cmi \ - buildTimeConf.cmx applyTransformation.cmi matitacLib.cmi -matitacLib.cmx: matitaMisc.cmx matitaExcPp.cmx matitaEngine.cmx \ - buildTimeConf.cmx applyTransformation.cmx matitacLib.cmi -matitac.cmo: matitadep.cmi matitaclean.cmi matitacLib.cmi matitaMisc.cmi \ - matitaInit.cmi -matitac.cmx: matitadep.cmx matitaclean.cmx matitacLib.cmx matitaMisc.cmx \ - matitaInit.cmx -matitadep.cmo: matitaMisc.cmi matitaInit.cmi matitadep.cmi -matitadep.cmx: matitaMisc.cmx matitaInit.cmx matitadep.cmi -matitaEngine.cmo: applyTransformation.cmi matitaEngine.cmi -matitaEngine.cmx: applyTransformation.cmx matitaEngine.cmi +matitac.cmo: matitaclean.cmi matitaMisc.cmi matitaInit.cmi matitaEngine.cmi +matitac.cmx: matitaclean.cmx matitaMisc.cmx matitaInit.cmx matitaEngine.cmx +matitaEngine.cmo: matitaEngine.cmi +matitaEngine.cmx: matitaEngine.cmi matitaExcPp.cmo: matitaEngine.cmi matitaExcPp.cmi matitaExcPp.cmx: matitaEngine.cmx matitaExcPp.cmi matitaGeneratedGui.cmo: @@ -42,20 +36,26 @@ matitaMathView.cmx: virtuals.cmx matitaTypes.cmx matitaScript.cmx \ matitaMisc.cmx matitaGuiTypes.cmi matitaGtkMisc.cmx matitaExcPp.cmx \ lablGraphviz.cmx buildTimeConf.cmx applyTransformation.cmx \ matitaMathView.cmi +matitaMathViewMml.cmo: virtuals.cmi matitaTypes.cmi matitaScript.cmi \ + matitaMisc.cmi matitaGuiTypes.cmi matitaGtkMisc.cmi matitaExcPp.cmi \ + lablGraphviz.cmi buildTimeConf.cmx applyTransformationMml.cmi \ + applyTransformation.cmi +matitaMathViewMml.cmx: virtuals.cmx matitaTypes.cmx matitaScript.cmx \ + matitaMisc.cmx matitaGuiTypes.cmi matitaGtkMisc.cmx matitaExcPp.cmx \ + lablGraphviz.cmx buildTimeConf.cmx applyTransformationMml.cmx \ + applyTransformation.cmx matitaMisc.cmo: buildTimeConf.cmx matitaMisc.cmi matitaMisc.cmx: buildTimeConf.cmx matitaMisc.cmi matita.cmo: predefined_virtuals.cmi matitaTypes.cmi matitaScript.cmi \ matitaMathView.cmi matitaInit.cmi matitaGui.cmi matitaGtkMisc.cmi \ - buildTimeConf.cmx applyTransformation.cmi + buildTimeConf.cmx matita.cmx: predefined_virtuals.cmx matitaTypes.cmx matitaScript.cmx \ matitaMathView.cmx matitaInit.cmx matitaGui.cmx matitaGtkMisc.cmx \ - buildTimeConf.cmx applyTransformation.cmx -matitaScript.cmo: virtuals.cmi matitacLib.cmi matitaTypes.cmi \ - matitaGtkMisc.cmi matitaEngine.cmi buildTimeConf.cmx \ - applyTransformation.cmi matitaScript.cmi -matitaScript.cmx: virtuals.cmx matitacLib.cmx matitaTypes.cmx \ - matitaGtkMisc.cmx matitaEngine.cmx buildTimeConf.cmx \ - applyTransformation.cmx matitaScript.cmi + buildTimeConf.cmx +matitaScript.cmo: virtuals.cmi matitaTypes.cmi matitaGtkMisc.cmi \ + matitaEngine.cmi buildTimeConf.cmx matitaScript.cmi +matitaScript.cmx: virtuals.cmx matitaTypes.cmx matitaGtkMisc.cmx \ + matitaEngine.cmx buildTimeConf.cmx matitaScript.cmi matitaTypes.cmo: matitaTypes.cmi matitaTypes.cmx: matitaTypes.cmi predefined_virtuals.cmo: virtuals.cmi predefined_virtuals.cmi @@ -63,15 +63,15 @@ predefined_virtuals.cmx: virtuals.cmx predefined_virtuals.cmi virtuals.cmo: virtuals.cmi virtuals.cmx: virtuals.cmi applyTransformation.cmi: +applyTransformationMml.cmi: applyTransformation.cmi lablGraphviz.cmi: matitaclean.cmi: -matitacLib.cmi: -matitadep.cmi: matitaEngine.cmi: matitaExcPp.cmi: matitaGtkMisc.cmi: matitaGeneratedGui.cmx matitaGui.cmi: matitaGuiTypes.cmi -matitaGuiTypes.cmi: matitaTypes.cmi matitaGeneratedGui.cmx +matitaGuiTypes.cmi: matitaTypes.cmi matitaGeneratedGui.cmx \ + applyTransformation.cmi matitaInit.cmi: matitaMathView.cmi: matitaTypes.cmi matitaGuiTypes.cmi matitaMisc.cmi: diff --git a/matita/matita/matita.ml b/matita/matita/matita.ml index d84203aa4..12cb9eeda 100644 --- a/matita/matita/matita.ml +++ b/matita/matita/matita.ml @@ -77,13 +77,8 @@ let script = (* math viewers *) let _ = - let cic_math_view = MatitaMathView.cicMathView_instance () in let sequents_viewer = MatitaMathView.sequentsViewer_instance () in sequents_viewer#load_logo; - cic_math_view#set_href_callback - (Some (fun uri -> - let uri = `NRef (NReference.reference_of_string uri) in - (MatitaMathView.cicBrowser ())#load uri)); let browser_observer _ = MatitaMathView.refresh_all_browsers () in let sequents_observer grafite_status = sequents_viewer#reset; diff --git a/matita/matita/matitaGuiTypes.mli b/matita/matita/matitaGuiTypes.mli index 03dab4c4c..9b2ed087c 100644 --- a/matita/matita/matitaGuiTypes.mli +++ b/matita/matita/matitaGuiTypes.mli @@ -100,42 +100,6 @@ end type paste_kind = [ `Term | `Pattern ] - (** multi selection gtkMathView which handle mactions and hyperlinks. Mactions - * are handled internally. Hyperlinks are handled by calling an user provided - * callback *) -class type clickableMathView = -object - inherit GSourceView2.source_view - - method load_root : root:string -> unit - method remove_selections: unit - method set_selection: unit option -> unit - method get_selections: unit list - method set_font_size: int -> unit - - - (** set hyperlink callback. None disable hyperlink handling *) - method set_href_callback: (string -> unit) option -> unit - - method has_selection: bool - - (** @raise Failure "no selection" *) - method strings_of_selection: (paste_kind * string) list - - method update_font_size: unit -end - -class type cicMathView = -object - inherit clickableMathView - - (** load a sequent and render it into parent widget *) - method nload_sequent: - #ApplyTransformation.status -> NCic.metasenv -> NCic.substitution -> int -> unit - - method load_nobject: #ApplyTransformation.status -> NCic.obj -> unit -end - class type sequentsViewer = object method reset: unit @@ -144,16 +108,9 @@ object method nload_sequents: #GrafiteTypes.status -> unit method goto_sequent: #ApplyTransformation.status -> int -> unit (* to be called _after_ load_sequents *) - - method cicMathView: cicMathView end class type cicBrowser = object method load: MatitaTypes.mathViewer_entry -> unit - (* method loadList: string list -> MatitaTypes.mathViewer_entry -> unit *) - method loadInput: string -> unit - method mathView: clickableMathView - method win: browserWin end - diff --git a/matita/matita/matitaMathView.ml b/matita/matita/matitaMathView.ml index a8f20aa18..3c87cdca4 100644 --- a/matita/matita/matitaMathView.ml +++ b/matita/matita/matitaMathView.ml @@ -31,6 +31,41 @@ open GrafiteTypes open MatitaGtkMisc open MatitaGuiTypes +class type _clickableMathView = +object + inherit GObj.widget + + method load_root : root:string -> unit +(* + method action_toggle: Gdome.element -> bool +*) + method remove_selections: unit + method set_selection: unit (*Gdome.element*) option -> unit + method get_selections: unit (*Gdome.element*) list + method set_font_size: int -> unit + + (** set hyperlink callback. None disable hyperlink handling *) + method set_href_callback: (string -> unit) option -> unit + + method has_selection: bool + + (** @raise Failure "no selection" *) + method strings_of_selection: (paste_kind * string) list + + method update_font_size: unit +end + +class type _cicMathView = +object + inherit _clickableMathView + + (** load a sequent and render it into parent widget *) + method nload_sequent: + #ApplyTransformation.status -> NCic.metasenv -> NCic.substitution -> int -> unit + + method load_nobject: #ApplyTransformation.status -> NCic.obj -> unit +end + module Stack = Continuationals.Stack (** inherit from this class if you want to access current script *) @@ -1055,7 +1090,7 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) val mutable lastDir = "" (* last loaded "directory" *) - method mathView = (mathView :> MatitaGuiTypes.clickableMathView) + method mathView = (mathView :> _clickableMathView) method private _getSelectedUri () = match model#easy_selection () with @@ -1312,7 +1347,7 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history) let sequentsViewer ~(notebook:GPack.notebook) ~(cicMathView:cicMathView) (): MatitaGuiTypes.sequentsViewer = - new sequentsViewer ~notebook ~cicMathView () + (new sequentsViewer ~notebook ~cicMathView ():> MatitaGuiTypes.sequentsViewer) let cicBrowser () = let size = BuildTimeConf.browser_history_size in @@ -1358,9 +1393,6 @@ let mathViewer () = method show_entry ?(reuse=false) t = (self#get_browser reuse)#load t - method show_uri_list ?(reuse=false) ~entry l = - (self#get_browser reuse)#load entry - method screenshot status sequents metasenv subst (filename as ofn) = () (*MATITA 1.0 let w = GWindow.window ~title:"screenshot" () in @@ -1432,7 +1464,7 @@ let update_font_sizes () = (cicMathView_instance ())#update_font_size let get_math_views () = - ((cicMathView_instance ()) :> MatitaGuiTypes.clickableMathView) + ((cicMathView_instance ()) :> _clickableMathView) :: (List.map (fun b -> b#mathView) !cicBrowsers) let find_selection_owner () = diff --git a/matita/matita/matitaMathView.mli b/matita/matita/matitaMathView.mli index b1064ba77..bc5d44920 100644 --- a/matita/matita/matitaMathView.mli +++ b/matita/matita/matitaMathView.mli @@ -23,52 +23,14 @@ * http://helm.cs.unibo.it/ *) -(** {2 Constructors} *) - - (** meta constructor *) -type 'widget constructor = - ?hadjustment:GData.adjustment -> - ?vadjustment:GData.adjustment -> - ?font_size:int -> - ?log_verbosity:int -> - ?auto_indent:bool -> - ?highlight_current_line:bool -> - ?indent_on_tab:bool -> - ?indent_width:int -> - ?insert_spaces_instead_of_tabs:bool -> - ?right_margin_position:int -> - ?show_line_marks:bool -> - ?show_line_numbers:bool -> - ?show_right_margin:bool -> - ?smart_home_end:SourceView2Enums.source_smart_home_end_type -> - ?tab_width:int -> - ?editable:bool -> - ?cursor_visible:bool -> - ?justification:GtkEnums.justification -> - ?wrap_mode:GtkEnums.wrap_mode -> - ?accepts_tab:bool -> - ?border_width:int -> - ?width:int -> - ?height:int -> - ?packing:(GObj.widget -> unit) -> - ?show:bool -> unit -> - 'widget - -val clickableMathView: MatitaGuiTypes.clickableMathView constructor - -val cicMathView: MatitaGuiTypes.cicMathView constructor - -val sequentsViewer: - notebook:GPack.notebook -> - cicMathView:MatitaGuiTypes.cicMathView -> - unit -> - MatitaGuiTypes.sequentsViewer - +(** {2 Instances} *) 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 ... *) +(** {2 Singleton instances} *) +val sequentsViewer_instance: unit -> MatitaGuiTypes.sequentsViewer +val mathViewer: unit -> MatitaTypes.mathViewer + +(** {2 Global changes} *) val increase_font_size: unit -> unit val decrease_font_size: unit -> unit @@ -90,14 +52,6 @@ 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 - diff --git a/matita/matita/matitaTypes.ml b/matita/matita/matitaTypes.ml index 1f7c50729..e5b80d0e8 100644 --- a/matita/matita/matitaTypes.ml +++ b/matita/matita/matitaTypes.ml @@ -82,8 +82,6 @@ class type mathViewer = * opens a new one. default is false *) method show_entry: ?reuse:bool -> mathViewer_entry -> unit - method show_uri_list: - ?reuse:bool -> entry:mathViewer_entry -> NReference.reference list -> unit method screenshot: GrafiteTypes.status -> NCic.metasenv -> NCic.metasenv -> NCic.substitution -> string -> unit diff --git a/matita/matita/matitaTypes.mli b/matita/matita/matitaTypes.mli index 3509f0ee7..c1d19ee7e 100644 --- a/matita/matita/matitaTypes.mli +++ b/matita/matita/matitaTypes.mli @@ -42,8 +42,6 @@ val entry_of_string : string -> mathViewer_entry class type mathViewer = object method show_entry : ?reuse:bool -> mathViewer_entry -> unit - method show_uri_list : - ?reuse:bool -> entry:mathViewer_entry -> NReference.reference list -> unit method screenshot: GrafiteTypes.status -> NCic.metasenv -> NCic.metasenv -> NCic.substitution -> string -> unit -- 2.39.2