]> matita.cs.unibo.it Git - helm.git/blob - helm/DEVEL/lablgtkmathview/gMathViewAux.ml
Added universes handling. The PRE_UNIVERSES tag may help ;)
[helm.git] / helm / DEVEL / lablgtkmathview / gMathViewAux.ml
1 (* Copyright (C) 2000-2003, Luca Padovani <luca.padovani@cs.unibo.it>,
2  *                          Claudio Sacerdoti Coen <sacerdot@cs.unibo.it>.
3  *
4  * This file is part of lablgtkmathview, the Ocaml binding
5  * for the GtkMathView widget.
6  * 
7  * lablgtkmathview is free software; you can redistribute it and/or
8  * modify it under the terms of the GNU General Public License
9  * as published by the Free Software Foundation; either version 2
10  * of the License, or (at your option) any later version.
11  *
12  * lablgtkmathview is distributed in the hope that it will be useful,
13  * but WITHOUT ANY WARRANTY; without even the implied warranty of
14  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
15  * GNU General Public License for more details.
16  *
17  * You should have received a copy of the GNU General Public License
18  * along with lablgtkmathview; if not, write to the Free Software
19  * Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA  02111-1307, USA.
20  * 
21  * For details, send a mail to the author.
22  *)
23
24 (* finds the common node ancestor of two nodes *)
25 let common_ancestor (first : Gdome.node) (last : Gdome.node) =
26  let rec path n =
27   match n#get_parentNode with
28      None -> [n]
29    | Some p -> n::(path p)
30  in
31   let rec last_common =
32    function
33       _, hd1::tl1, hd2::tl2 when hd1#isSameNode hd2 -> (last_common ((Some hd1),tl1,tl2))
34     | Some e, _, _ -> e
35     | _,_,_ -> assert false
36   in
37    (last_common (None,(List.rev (path first)),(List.rev (path last))))
38  
39 let same_element (e1 : Gdome.element option) (e2 : Gdome.element option) =
40  match e1, e2 with
41     None, None -> true
42   | Some e1, Some e2 when (e1 :> Gdome.node)#isSameNode (e2 :> Gdome.node) -> true
43   | _ -> false
44         
45 (* true if n1 is n2 or one of n2's descendants *)
46 let rec descendant_of (n1 : Gdome.node) (n2 : Gdome.node) =
47  if n1#isSameNode n2 then true
48  else
49   match n1#get_parentNode with
50      None -> false
51    | Some n1' -> descendant_of n1' n2
52
53 let remove_descendants_of (el : Gdome.element) =
54  let rec aux =
55   function
56      [] -> []
57    | hd::tl when descendant_of (hd :> Gdome.node) (el :> Gdome.node) -> aux tl
58    | hd::tl -> hd::(aux tl)
59  in
60   aux
61
62 (* mem el l = true if the node n is stored in the list l *)
63 let mem (el : Gdome.element) =
64  let rec mem_aux =
65   function
66      hd::_ when (hd :> Gdome.node)#isSameNode (el :> Gdome.node) -> true
67    | _::tl -> mem_aux tl
68    | _ -> false
69  in
70   mem_aux
71
72 (* remove el l = l' where l' has the same nodes as l except that all
73  * the occurrences of n have been removed *)
74 let remove (el : Gdome.element) =
75  let rec remove_aux =
76   function
77      hd::tl when (hd :> Gdome.node)#isSameNode (el :> Gdome.node) ->
78       remove_aux tl
79    | hd::tl -> hd::(remove_aux tl)
80    | [] -> []
81  in
82   remove_aux
83
84 class single_selection_math_view_signals obj (set_selection_changed : (Gdome.element option -> unit) -> unit) =
85  object
86   inherit GMathView.math_view_signals obj
87   method selection_changed = set_selection_changed
88  end
89 ;;
90
91 class single_selection_math_view obj =
92   object(self)
93    inherit GMathView.math_view_skel obj
94    val mutable first_selected = None
95    val mutable root_selected = None
96    val mutable selection_changed = (fun _ -> ())
97
98    method set_selection elem =
99     self#freeze ;
100     begin
101      match root_selected with
102         None -> ()
103       | Some e -> self#unselect e
104     end;
105     root_selected <- elem ;
106     begin
107      match elem with
108         None -> ()
109       | Some e -> self#select e
110     end ;
111     self#thaw
112
113    method get_selection = root_selected
114
115    method connect =
116     new
117      single_selection_math_view_signals obj
118       (function f -> selection_changed <- f)
119
120    method action_toggle (elem : Gdome.element) =
121     match elem#get_namespaceURI, elem#get_localName with
122        Some ns, Some ln
123         when 
124          (ns#to_string = "http://www.w3.org/1998/Math/MathML" && ln#to_string = "maction") ||
125          (ns#to_string = "http://helm.cs.unibo.it/2003/BoxML" && ln#to_string = "action")
126        ->
127         begin
128          let selection_attr = Gdome.domString "selection" in
129          let selection =
130           if elem#hasAttribute ~name:selection_attr then
131            int_of_string (elem#getAttribute ~name:selection_attr)#to_string
132           else
133            1
134          in
135           self#freeze ;
136           (* the widget will cast the index back into a valid range *)
137           elem#setAttribute ~name:selection_attr
138            ~value:(Gdome.domString (string_of_int (selection + 1))) ;
139           self#thaw ;
140           true
141         end
142      | _ ->
143         begin
144          match elem#get_parentNode with
145             Some p ->
146              begin
147               try
148                self#action_toggle (new Gdome.element_of_node p)
149               with
150                GdomeInit.DOMCastException _ -> false
151              end
152           | None -> assert false (* every element has a parent *)
153         end
154      
155    initializer
156     selection_changed <- self#set_selection ;
157
158     ignore
159      (self#connect#select_begin
160        (fun ((elem : Gdome.element option), _, _, _) ->
161          if not (same_element root_selected elem) then selection_changed elem ;
162          first_selected <- elem)) ;
163
164     ignore
165      (self#connect#select_over
166        (fun ((elem : Gdome.element option), _, _, _) ->
167          let new_selected =
168           match first_selected, elem with
169              Some first', Some last' ->
170               (Some
171                (new Gdome.element_of_node
172                 (common_ancestor (first' :> Gdome.node) (last' :> Gdome.node))))
173            | _ -> None
174          in
175           if not (same_element root_selected new_selected) then
176             selection_changed new_selected)) ;
177              
178     ignore
179      (self#connect#select_end
180        (fun ((elem : Gdome.element option), _, _, _) -> first_selected <- None)) ;
181
182     ignore
183      (self#connect#select_abort
184        (fun () ->
185          first_selected <- None ;
186          selection_changed None)) ;
187
188     ignore (self#connect#click (fun _ -> self#set_selection None))
189   end
190 ;;
191
192 let single_selection_math_view ?hadjustment ?vadjustment ?font_size ?log_verbosity =
193   GtkBase.Widget.size_params ~cont:(
194   OgtkMathViewProps.pack_return
195     (fun p -> OgtkMathViewProps.set_params (new single_selection_math_view
196     (GtkMathViewProps.MathView_GMetaDOM.create p)) ~font_size ~log_verbosity)) []
197 ;;
198
199 class multi_selection_math_view_signals obj
200  (set_selection_changed : (Gdome.element option -> unit) -> unit)
201 =
202  object
203   inherit GMathView.math_view_signals obj
204   method selection_changed = set_selection_changed
205  end
206 ;;
207
208 class multi_selection_math_view obj =
209   object(self)
210    inherit single_selection_math_view obj
211    val mutable selected : Gdome.element list = []
212
213    method remove_selection (elem : Gdome.element) =
214     if mem elem selected then
215      selected <- remove elem selected ;
216      self#unselect elem
217
218    method remove_selections =
219     self#freeze ;
220     List.iter (fun e -> self#unselect e) selected ;
221     selected <- [] ;
222     begin
223      match self#get_selection with
224         None -> ()
225       | Some e -> self#select e
226     end ;
227     self#thaw
228
229    method add_selection (elem : Gdome.element) =
230     List.iter self#unselect selected ;
231     selected <- elem::(remove_descendants_of elem selected) ;
232     List.iter self#select selected
233
234    method get_selections = selected
235
236    method set_selection elem =
237     self#freeze ;
238     begin
239      match root_selected with
240         None -> ()
241       | Some e -> self#unselect e ; List.iter (fun e -> self#select e) selected
242     end;
243     root_selected <- elem;
244     begin
245      match elem with
246         None -> ()
247       | Some e -> self#select e
248     end ;
249     self#thaw
250
251    initializer
252     ignore
253      (self#connect#select_begin
254        (fun (_,_,_,state) ->
255          if not (List.mem `CONTROL (Gdk.Convert.modifier state)) then
256           self#remove_selections)) ;
257
258     ignore
259      (self#connect#select_over
260        (fun (_,_,_,state) ->
261          let c = 
262           function
263              `SHIFT -> "shift "
264            | `LOCK -> "lock "
265            | `CONTROL -> "control "
266            | `MOD1 -> "mod1 "
267            | _ -> ""
268          in
269           List.iter (fun x -> print_string (c x)) (Gdk.Convert.modifier state) ;
270           print_char '\n' ;
271           flush stdout)) ;
272
273     ignore
274      (self#connect#select_end
275        (fun (_,_,_,state) ->
276          if not (List.mem `CONTROL (Gdk.Convert.modifier state)) then
277           self#remove_selections ;
278          match root_selected with
279             None -> ()
280          | Some e -> self#set_selection None ; self#add_selection e)) ;
281
282     ignore
283      (self#connect#click
284        (fun _ -> self#remove_selections))
285    end
286  ;;
287
288 let multi_selection_math_view ?hadjustment ?vadjustment ?font_size ?log_verbosity =
289   GtkBase.Widget.size_params ~cont:(
290   OgtkMathViewProps.pack_return
291     (fun p -> OgtkMathViewProps.set_params (new multi_selection_math_view
292     (GtkMathViewProps.MathView_GMetaDOM.create p)) ~font_size ~log_verbosity)) []
293 ;;