]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/DEVEL/lablgtkmathview/gMathViewAux.ml
This commit was manufactured by cvs2svn to create branch 'moogle'.
[helm.git] / helm / DEVEL / lablgtkmathview / gMathViewAux.ml
diff --git a/helm/DEVEL/lablgtkmathview/gMathViewAux.ml b/helm/DEVEL/lablgtkmathview/gMathViewAux.ml
deleted file mode 100644 (file)
index d59732c..0000000
+++ /dev/null
@@ -1,289 +0,0 @@
-(* Copyright (C) 2000-2003, Luca Padovani <luca.padovani@cs.unibo.it>,
- *                          Claudio Sacerdoti Coen <sacerdot@cs.unibo.it>.
- *
- * 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 ?hadjustment ?vadjustment ?font_size ?log_verbosity =
-  GtkBase.Container.make_params ~cont:(
-  OgtkMathViewProps.pack_return
-    (fun p -> OgtkMathViewProps.set_params (new single_selection_math_view (GtkMathViewProps.MathView.create p)) ~font_size ~log_verbosity)) []
-;;
-
-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 ->
-         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 ->
-         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 ?hadjustment ?vadjustment ?font_size ?log_verbosity =
-  GtkBase.Container.make_params ~cont:(
-  OgtkMathViewProps.pack_return
-    (fun p -> OgtkMathViewProps.set_params (new multi_selection_math_view (GtkMathViewProps.MathView.create p)) ~font_size ~log_verbosity)) []
-;;