]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/DEVEL/lablgtkmathview/gMathViewAux.ml
ocaml 3.09 transition
[helm.git] / helm / DEVEL / lablgtkmathview / gMathViewAux.ml
index ba12fdfdfcc46bc06f796c39919e189834eeda60..45bc5d90ce3a5df474a2d17247e57e0db36e8149 100644 (file)
@@ -1,24 +1,27 @@
-(* Copyright (C) 2000-2003, Luca Padovani <luca.padovani@cs.unibo.it>,
- *                          Claudio Sacerdoti Coen <sacerdot@cs.unibo.it>.
+(* Copyright (C) 2000-2005,
+ *    Luca Padovani          <lpadovan@cs.unibo.it>
+ *    Claudio Sacerdoti Coen  <sacerdot@cs.unibo.it>
+ *    Stefano Zacchiroli      <zacchiro@cs.unibo.it>
  *
- * This file is part of lablgtkmathview, the Ocaml binding
- * for the GtkMathView widget.
+ * 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.
+ * 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.
+ * 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.
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
+ * 02111-1307, USA.
  * 
- * For details, send a mail to the author.
+ * For details, send a mail to the authors.
  *)
 
 (* finds the common node ancestor of two nodes *)
@@ -41,7 +44,7 @@ let same_element (e1 : Gdome.element option) (e2 : Gdome.element option) =
     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
@@ -74,7 +77,8 @@ let mem (el : Gdome.element) =
 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 when (hd :> Gdome.node)#isSameNode (el :> Gdome.node) ->
+      remove_aux tl
    | hd::tl -> hd::(remove_aux tl)
    | [] -> []
  in
@@ -95,25 +99,34 @@ class single_selection_math_view obj =
    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;
-    match elem with
-       None -> ()
-     | Some e -> self#select e
+    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)
+    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" ->
+       Some ns, Some ln
+        when 
+        (ns#to_string = "http://www.w3.org/1998/Math/MathML" && ln#to_string = "maction") ||
+        (ns#to_string = "http://helm.cs.unibo.it/2003/BoxML" && ln#to_string = "action")
+       ->
         begin
          let selection_attr = Gdome.domString "selection" in
          let selection =
@@ -124,10 +137,11 @@ class single_selection_math_view obj =
          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))) ;
+          elem#setAttribute ~name:selection_attr
+           ~value:(Gdome.domString (string_of_int (selection + 1))) ;
           self#thaw ;
           true
-       end
+        end
      | _ ->
         begin
          match elem#get_parentNode with
@@ -139,72 +153,55 @@ class single_selection_math_view obj =
                GdomeInit.DOMCastException _ -> false
              end
           | None -> assert false (* every element has a parent *)
-       end
+        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
-         begin
-          self#set_selection elem ;
-          selection_changed elem
-         end ;
-        first_selected <- elem)) ;
+       (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) _ ->
+       (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))))
+              (Some
+               (new Gdome.element_of_node
+                (common_ancestor (first' :> Gdome.node) (last' :> Gdome.node))))
            | _ -> None
-        in
+         in
           if not (same_element root_selected new_selected) then
-          begin
-           self#set_selection new_selected ;
-           selection_changed new_selected
-          end)) ;
-            
+            selection_changed new_selected)) ;
+             
     ignore
      (self#connect#select_end
-       (fun (elem : Gdome.element option) _ -> first_selected <- None)) ;
+       (fun ((elem : Gdome.element option), _, _, _) -> first_selected <- None)) ;
 
     ignore
      (self#connect#select_abort
        (fun () ->
          first_selected <- None ;
-        selection_changed None)) ;
+         selection_changed None)) ;
 
-   ignore (self#connect#click (fun _ _ -> self#set_selection 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
+let single_selection_math_view ?hadjustment ?vadjustment ?font_size ?log_verbosity =
+  GtkBase.Widget.size_params ~cont:(
+  OgtkMathViewProps.pack_return
+    (fun p -> OgtkMathViewProps.set_params (new single_selection_math_view
+    (GtkMathViewProps.MathView_GMetaDOM.create p)) ~font_size ~log_verbosity)) []
 ;;
 
-class multi_selection_math_view_signals obj (set_selection_changed : (Gdome.element option -> unit) -> unit) =
+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
@@ -222,87 +219,63 @@ class multi_selection_math_view obj =
      self#unselect elem
 
    method remove_selections =
+    self#freeze ;
     List.iter (fun e -> self#unselect e) selected ;
     selected <- [] ;
-    match self#get_selection with
-       None -> ()
-     | Some e -> self#select e
+    begin
+     match self#get_selection with
+        None -> ()
+      | Some e -> self#select e
+    end ;
+    self#thaw
 
    method add_selection (elem : Gdome.element) =
+    List.iter self#unselect selected ;
     selected <- elem::(remove_descendants_of elem selected) ;
-    self#select elem
+    List.iter self#select selected
 
    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;
-    match elem with
-       None -> ()
-     | Some e -> self#select e
+    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)) ;
+       (fun (_,_,_,state) ->
+         if not (List.mem `CONTROL (Gdk.Convert.modifier state)) then
+          self#remove_selections)) ;
 
     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)) ;
+       (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))
+       (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
+let multi_selection_math_view ?hadjustment ?vadjustment ?font_size ?log_verbosity =
+  GtkBase.Widget.size_params ~cont:(
+  OgtkMathViewProps.pack_return
+    (fun p -> OgtkMathViewProps.set_params (new multi_selection_math_view
+    (GtkMathViewProps.MathView_GMetaDOM.create p)) ~font_size ~log_verbosity)) []
 ;;
-