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