helm/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 ;;