X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=helm%2FDEVEL%2Flablgtkmathview%2FgMathViewAux.ml;fp=helm%2FDEVEL%2Flablgtkmathview%2FgMathViewAux.ml;h=0000000000000000000000000000000000000000;hp=928e2196522e5981be0cc2efc98341de2a08dbcf;hb=3ef089a4c58fbe429dd539af6215991ecbe11ee2;hpb=1c7fb836e2af4f2f3d18afd0396701f2094265ff diff --git a/helm/DEVEL/lablgtkmathview/gMathViewAux.ml b/helm/DEVEL/lablgtkmathview/gMathViewAux.ml deleted file mode 100644 index 928e21965..000000000 --- a/helm/DEVEL/lablgtkmathview/gMathViewAux.ml +++ /dev/null @@ -1,329 +0,0 @@ -(* Copyright (C) 2000-2003, Luca Padovani , - * Claudio Sacerdoti Coen . - * - * This file is part of lablgtkmathview, the Ocaml binding - * for the GtkMathView widget. - * - * lablgtkmathview is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * lablgtkmathview is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with lablgtkmathview; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA 02111-1307, USA. - * - * For details, send a mail to the author. - *) - -(* finds the common node ancestor of two nodes *) -let common_ancestor (first : Gdome.node) (last : Gdome.node) = - let rec path n = - match n#get_parentNode with - None -> [n] - | Some p -> n::(path p) - in - let rec last_common = - function - _, hd1::tl1, hd2::tl2 when hd1#isSameNode hd2 -> (last_common ((Some hd1),tl1,tl2)) - | Some e, _, _ -> e - | _,_,_ -> assert false - in - (last_common (None,(List.rev (path first)),(List.rev (path last)))) - -let same_element (e1 : Gdome.element option) (e2 : Gdome.element option) = - match e1, e2 with - None, None -> true - | Some e1, Some e2 when (e1 :> Gdome.node)#isSameNode (e2 :> Gdome.node) -> true - | _ -> false - -(* true if n1 is n2 or one of n2's descendants *) -let rec descendant_of (n1 : Gdome.node) (n2 : Gdome.node) = - if n1#isSameNode n2 then true - else - match n1#get_parentNode with - None -> false - | Some n1' -> descendant_of n1' n2 - -let remove_descendants_of (el : Gdome.element) = - let rec aux = - function - [] -> [] - | hd::tl when descendant_of (hd :> Gdome.node) (el :> Gdome.node) -> aux tl - | hd::tl -> hd::(aux tl) - in - aux - -(* mem el l = true if the node n is stored in the list l *) -let mem (el : Gdome.element) = - let rec mem_aux = - function - hd::_ when (hd :> Gdome.node)#isSameNode (el :> Gdome.node) -> true - | _::tl -> mem_aux tl - | _ -> false - in - mem_aux - -(* remove el l = l' where l' has the same nodes as l except that all - * the occurrences of n have been removed *) -let remove (el : Gdome.element) = - let rec remove_aux = - function - hd::tl when (hd :> Gdome.node)#isSameNode (el :> Gdome.node) -> - remove_aux tl - | hd::tl -> hd::(remove_aux tl) - | [] -> [] - in - remove_aux - -class single_selection_math_view_signals obj (set_selection_changed : (Gdome.element option -> unit) -> unit) = - object - inherit GMathView.math_view_signals obj - method selection_changed = set_selection_changed - end -;; - -class single_selection_math_view obj = - object(self) - inherit GMathView.math_view_skel obj - val mutable first_selected = None - val mutable root_selected = None - val mutable selection_changed = (fun _ -> ()) - - method set_selection elem = - self#freeze ; - begin - match root_selected with - None -> () - | Some e -> self#unselect e - end; - root_selected <- elem ; - begin - match elem with - None -> () - | Some e -> self#select e - end ; - self#thaw - - method get_selection = root_selected - - method connect = - new - single_selection_math_view_signals obj - (function f -> selection_changed <- f) - - method action_toggle (elem : Gdome.element) = - match elem#get_namespaceURI, elem#get_localName with - Some ns, Some ln - when ns#to_string = "http://www.w3.org/1998/Math/MathML" && - ln#to_string = "maction" - -> - begin - let selection_attr = Gdome.domString "selection" in - let selection = - if elem#hasAttribute ~name:selection_attr then - int_of_string (elem#getAttribute ~name:selection_attr)#to_string - else - 1 - in - self#freeze ; - (* the widget will cast the index back into a valid range *) - elem#setAttribute ~name:selection_attr - ~value:(Gdome.domString (string_of_int (selection + 1))) ; - self#thaw ; - true - end - | _ -> - begin - match elem#get_parentNode with - Some p -> - begin - try - self#action_toggle (new Gdome.element_of_node p) - with - GdomeInit.DOMCastException _ -> false - end - | None -> assert false (* every element has a parent *) - end - - initializer - selection_changed <- self#set_selection ; - - ignore - (self#connect#select_begin - (fun (elem : Gdome.element option) _ -> - if not (same_element root_selected elem) then selection_changed elem ; - first_selected <- elem)) ; - - ignore - (self#connect#select_over - (fun (elem : Gdome.element option) _ -> - let new_selected = - match first_selected, elem with - Some first', Some last' -> - (Some - (new Gdome.element_of_node - (common_ancestor (first' :> Gdome.node) (last' :> Gdome.node)))) - | _ -> None - in - if not (same_element root_selected new_selected) then - selection_changed new_selected)) ; - - ignore - (self#connect#select_end - (fun (elem : Gdome.element option) _ -> first_selected <- None)) ; - - ignore - (self#connect#select_abort - (fun () -> - first_selected <- None ; - selection_changed None)) ; - - ignore (self#connect#click (fun _ _ -> self#set_selection None)) - end -;; - -let single_selection_math_view ?adjustmenth ?adjustmentv ?font_size ?font_manager ?border_width - ?width ?height ?packing ?show () = - let w = - GtkMathView.MathView.create - ?adjustmenth:(Gaux.may_map ~f:GData.as_adjustment adjustmenth) - ?adjustmentv:(Gaux.may_map ~f:GData.as_adjustment adjustmentv) - () - in - GtkBase.Container.set w ?border_width ?width ?height; - let mathview = - GObj.pack_return (new single_selection_math_view w) ~packing ~show - in - begin - match font_size with - | Some size -> mathview#set_font_size size - | None -> () - end; - begin - match font_manager with - | Some manager -> mathview#set_font_manager_type ~fm_type:manager - | None -> () - end; - mathview -;; - -class multi_selection_math_view_signals obj - (set_selection_changed : (Gdome.element option -> unit) -> unit) -= - object - inherit GMathView.math_view_signals obj - method selection_changed = set_selection_changed - end -;; - -class multi_selection_math_view obj = - object(self) - inherit single_selection_math_view obj - val mutable selected : Gdome.element list = [] - - method remove_selection (elem : Gdome.element) = - if mem elem selected then - selected <- remove elem selected ; - self#unselect elem - - method remove_selections = - self#freeze ; - List.iter (fun e -> self#unselect e) selected ; - selected <- [] ; - begin - match self#get_selection with - None -> () - | Some e -> self#select e - end ; - self#thaw - - method add_selection (elem : Gdome.element) = - selected <- elem::(remove_descendants_of elem selected) ; - self#select elem - - method get_selections = selected - - method set_selection elem = - self#freeze ; - begin - match root_selected with - None -> () - | Some e -> self#unselect e ; List.iter (fun e -> self#select e) selected - end; - root_selected <- elem; - begin - match elem with - None -> () - | Some e -> self#select e - end ; - self#thaw - - initializer - ignore - (self#connect#select_begin - (fun _ state -> - if not (List.mem `CONTROL (Gdk.Convert.modifier state)) then - self#remove_selections)) ; - - ignore - (self#connect#select_over - (fun _ state -> - Printf.printf "stable selections: %d\n" (List.length selected) ; - Printf.printf "select_over with state: " ; - let c = - function - `SHIFT -> "shift " - | `LOCK -> "lock " - | `CONTROL -> "control " - | `MOD1 -> "mod1 " - | _ -> "" - in - List.iter (fun x -> print_string (c x)) (Gdk.Convert.modifier state) ; - print_char '\n' ; - flush stdout)) ; - - ignore - (self#connect#select_end - (fun _ state -> - Printf.printf "select_end\n" ; flush stdout ; - if not (List.mem `CONTROL (Gdk.Convert.modifier state)) then - self#remove_selections ; - match root_selected with - None -> () - | Some e -> self#set_selection None ; self#add_selection e)) ; - - ignore - (self#connect#click - (fun _ _ -> self#remove_selections)) - end - ;; - -let multi_selection_math_view ?adjustmenth ?adjustmentv ?font_size ?font_manager ?border_width - ?width ?height ?packing ?show () = - let w = - GtkMathView.MathView.create - ?adjustmenth:(Gaux.may_map ~f:GData.as_adjustment adjustmenth) - ?adjustmentv:(Gaux.may_map ~f:GData.as_adjustment adjustmentv) - () - in - GtkBase.Container.set w ?border_width ?width ?height; - let mathview = GObj.pack_return (new multi_selection_math_view w) ~packing ~show in - begin - match font_size with - | Some size -> mathview#set_font_size size - | None -> () - end; - begin - match font_manager with - | Some manager -> mathview#set_font_manager_type ~fm_type:manager - | None -> () - end; - mathview -;; -