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.

diff --git a/matita/matita/.depend b/matita/matita/.depend
index b8de092d1c564850c216d617f8796b1a57131f49..4b98fdf33db49bae9e7d7565ece4aa3a133322af 100644 (file)
--- 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 a6f9694544d14483e9391ec42644f7c30d5cb8b3..c51561a1a1b1a9a8bcbda7ab8706a7c05b222be6 100644 (file)
--- 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 d84203aa4dcbe0706ff77df40d177eb822ed2403..12cb9eedafac1e7a96d11e68d7711b41146603d8 100644 (file)
--- 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 03dab4c4c5edf0ed8d70fa6043499ef23e4223b7..9b2ed087c28f4bdb6cbbdb37f463867e1779b77e 100644 (file)
--- 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 a8f20aa1863c5765565618f87b8a68ace7b892dd..3c87cdca4761df195b8a8b6830e1e89fb075c717 100644 (file)
--- 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 b1064ba77e54a3437fe42fad5dd92f22f75a129d..bc5d44920390f5abffe5c2d28b8108979e1babdc 100644 (file)
--- 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 1f7c50729415d20a93466ced090ada597cea06b7..e5b80d0e883c483e3c6b41e3028205985462e475 100644 (file)
--- 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 3509f0ee7fc9b77be375d685b0d6076e290158c3..c1d19ee7e8c5feb3dba2241486d082294ddeee32 100644 (file)
--- 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