]> matita.cs.unibo.it Git - helm.git/commitdiff
* binding update to recognize the new event scheme generated by
authorLuca Padovani <luca.padovani@unito.it>
Mon, 27 Jan 2003 14:21:24 +0000 (14:21 +0000)
committerLuca Padovani <luca.padovani@unito.it>
Mon, 27 Jan 2003 14:21:24 +0000 (14:21 +0000)
   gtkmathview
* some code for handling maction elements has been moved into the
  compatibility class

helm/DEVEL/lablgtkmathview/Makefile.in
helm/DEVEL/lablgtkmathview/gMathView.ml
helm/DEVEL/lablgtkmathview/gMathView.mli
helm/DEVEL/lablgtkmathview/gMathViewAux.ml
helm/DEVEL/lablgtkmathview/gMathViewAux.mli
helm/DEVEL/lablgtkmathview/gtkMathView.ml
helm/DEVEL/lablgtkmathview/ml_gtk_mathview.c
helm/DEVEL/lablgtkmathview/test/test.ml

index 7b140e0f3a7fbaf07bae2fb943d2ebb98fb1cf0f..ab9224ae8a39e868ed5bd71d24571c544476d737 100644 (file)
@@ -103,7 +103,11 @@ install:
        fi
 
 uninstall:
-       ocamlfind remove $(PACKAGE)
+       if [ "$(PREFIX)" = "" ]; then \
+               ocamlfind remove $(PACKAGE); \
+       else \
+               ocamlfind remove -destdir $(PREFIX) $(PACKAGE); \
+       fi
 
 clean:
        rm -f *.[ao] *.cm[iaxo] *.cmxa *.so
index 646d68b0a1354558006ad9db4b24c37c06aac178..d1028d189f67eae1c066d988c09573c6b06781e4 100644 (file)
@@ -32,47 +32,79 @@ exception ErrorWritingFile of string;;
 exception ErrorLoadingDOM;;
 exception NoSelection;;
 
+let option_element_of_option =
+ function
+    None -> None
+  | Some v -> Some (new Gdome.element v)
+
 class math_view_signals obj = object
   inherit GContainer.container_signals obj
-  method clicked =
+  method click =
+   let module S = GtkSignal in
+    let new_click =
+     let new_marshaller f x y =
+      MathView.Signals.click.S.marshaller
+       (fun e s -> f (new Gdome.element e) s) x y
+     in
+      { S.name = "click"; S.classe = `math_view;
+        S.marshaller = new_marshaller }
+    in
+     GtkSignal.connect ~sgn:new_click obj ~after
+  method select_begin =
+   let module S = GtkSignal in
+    let new_select_begin =
+     let new_marshaller f x y =
+      MathView.Signals.select_begin.S.marshaller
+       (fun e s -> f (option_element_of_option e) s) x y
+     in
+      { S.name = "select_begin"; S.classe = `math_view;
+        S.marshaller = new_marshaller }
+    in
+     GtkSignal.connect ~sgn:new_select_begin obj ~after
+   method select_over =
+   let module S = GtkSignal in
+    let new_select_over =
+     let new_marshaller f x y =
+      MathView.Signals.select_over.S.marshaller
+       (fun e s -> f (option_element_of_option e) s) x y
+     in
+      { S.name = "select_over"; S.classe = `math_view;
+        S.marshaller = new_marshaller }
+    in
+     GtkSignal.connect ~sgn:new_select_over obj ~after
+   method select_end =
    let module S = GtkSignal in
-    let new_clicked =
+    let new_select_end =
      let new_marshaller f x y =
-      MathView.Signals.clicked.S.marshaller
-       (fun e -> f (new Gdome.element e)) x y
+      MathView.Signals.select_end.S.marshaller
+       (fun e s -> f (option_element_of_option e) s) x y
      in
-      { S.name = "clicked"; S.classe = `math_view;
+      { S.name = "select_end"; S.classe = `math_view;
         S.marshaller = new_marshaller }
     in
-     GtkSignal.connect ~sgn:new_clicked obj ~after
-  method press_move =
+     GtkSignal.connect ~sgn:new_select_end obj ~after
+   method select_abort =
    let module S = GtkSignal in
-    let new_press_move =
+    let new_select_abort =
      let new_marshaller f x y =
-      MathView.Signals.press_move.S.marshaller
-       (fun x y ->
-         let option_element_of_option v =
-         match v with
-            None -> None
-          | Some v' -> Some (new Gdome.element v')
-        in
-         f (option_element_of_option x) (option_element_of_option y)) x y
+      MathView.Signals.select_abort.S.marshaller
+       (fun () -> f ()) x y
      in
-      { S.name = "press_move"; S.classe = `math_view;
+      { S.name = "select_abort"; S.classe = `math_view;
         S.marshaller = new_marshaller }
     in
-     GtkSignal.connect ~sgn:new_press_move obj ~after
-  method element_changed =
+     GtkSignal.connect ~sgn:new_select_abort obj ~after
+  method element_over =
    let module S = GtkSignal in
-    let new_element_changed =
+    let new_element_over =
      let new_marshaller f x y =
-      MathView.Signals.element_changed.S.marshaller
-       (function None -> f None | Some e -> f (Some (new Gdome.element e))) x y
+      MathView.Signals.element_over.S.marshaller
+       (fun e s -> f (option_element_of_option e) s) x y
      in
-      { S.name = "element_changed"; S.classe = `math_view;
+      { S.name = "element_over"; S.classe = `math_view;
         S.marshaller = new_marshaller }
     in
-     GtkSignal.connect ~sgn:new_element_changed obj ~after
+     GtkSignal.connect ~sgn:new_element_over obj ~after
 end
 
 class math_view_skel obj = object
index 0c380ad60a94ac018577df4441192e51f4ec2e7d..e52a7a484c7d0a6cecc0bf9cc961492addf92ace 100644 (file)
@@ -30,11 +30,17 @@ class math_view_signals :
   object ('a)
     inherit GContainer.container_signals
     val obj: 'b Gtk.obj
-    method clicked : callback:(Gdome.element -> unit) -> GtkSignal.id
-    method element_changed :
-      callback:(Gdome.element option -> unit) -> GtkSignal.id
-    method press_move :
-      callback:(Gdome.element option -> Gdome.element option -> unit) -> GtkSignal.id
+    method click : callback:(Gdome.element -> int -> unit) -> GtkSignal.id
+    method element_over :
+      callback:(Gdome.element option -> int -> unit) -> GtkSignal.id
+    method select_begin :
+      callback:(Gdome.element option -> int -> unit) -> GtkSignal.id
+    method select_over :
+      callback:(Gdome.element option -> int -> unit) -> GtkSignal.id
+    method select_end :
+      callback:(Gdome.element option -> int -> unit) -> GtkSignal.id
+    method select_abort :
+      callback:(unit -> unit) -> GtkSignal.id
   end
 
 class math_view_skel :
index 9fe2c80a5d782ba2dfc6d95c020c7e53c3d6961d..d23ce2d1cc42f210452d5de71a0ce76f00ad9457 100644 (file)
@@ -43,6 +43,15 @@ let rec descendant_of (n1 : Gdome.node) (n2 : Gdome.node) =
      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 =
@@ -74,36 +83,85 @@ class single_selection_math_view_signals obj (set_selection_changed : (Gdome.ele
 class single_selection_math_view obj =
   object(self)
    inherit GMathView.math_view_skel obj
-   val mutable root_selection = None
+   val mutable first_selected = None
+   val mutable root_selected = None
    val mutable selection_changed = (fun _ -> ())
 
-   method set_selection root_selection' =
+   method set_selection elem =
     begin
-     match root_selection with
+     match root_selected with
         None -> ()
       | Some e -> self#unselect e
     end;
-    root_selection <- root_selection';
-    match root_selection' with
+    root_selected <- elem;
+    match elem with
        None -> ()
      | Some e -> self#select e
 
-   method get_selection = root_selection
+   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
     ignore
-     (self#connect#press_move
-       (fun (first: Gdome.element option) (last: Gdome.element option) ->
-         match first, last with
+     (self#connect#select_begin
+       (fun (elem : Gdome.element option) _ ->
+         if not (elem = root_selected) then selection_changed elem ;
+        first_selected <- elem)) ;
+
+    ignore
+     (self#connect#select_over
+       (fun (elem : Gdome.element option) _ ->
+         match first_selected, elem with
             None, _
           | _, None -> selection_changed None
           | Some first', Some last' ->
              selection_changed
              (Some (new Gdome.element_of_node (common_ancestor (first' :> Gdome.node) (last' :> Gdome.node)))))) ;
-    ignore (self#connect#clicked (fun _ -> self#set_selection None))
+            
+    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
 ;;
 
@@ -149,27 +207,62 @@ class multi_selection_math_view obj =
 
    method remove_selections =
     List.iter (fun e -> self#unselect e) selected ;
-    selected <- []
+    selected <- [] ;
+    match self#get_selection with
+       None -> ()
+     | Some e -> self#select e
 
    method add_selection (elem : Gdome.element) =
-    if not (mem elem selected) then
-     selected <- elem::selected ;
-     self#select elem
+    selected <- elem::(remove_descendants_of elem selected) ;
+    self#select elem
 
    method get_selections = selected
 
-   method set_selection root_selection' =
+   method set_selection elem =
     begin
-     match root_selection with
+     match root_selected with
         None -> ()
       | Some e -> self#unselect e ; List.iter (fun e -> self#select e) selected
     end;
-    root_selection <- root_selection';
-    match root_selection' with
+    root_selected <- elem;
+    match elem with
        None -> ()
      | Some e -> self#select e
-  end
-;;
+
+   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))
+
+   end
+ ;;
 
 let multi_selection_math_view ?adjustmenth ?adjustmentv ?font_size ?font_manager ?border_width
  ?width ?height ?packing ?show () =
index abbe54493d7bc901813b2d919ecb06eb8a51419f..e63c41173a41586d8e71dbb7a210596dd33741f9 100644 (file)
@@ -35,6 +35,7 @@ class single_selection_math_view :
     method connect : single_selection_math_view_signals
     method get_selection : Gdome.element option
     method set_selection : Gdome.element option -> unit
+    method action_toggle : Gdome.element -> bool
   end
 
 val single_selection_math_view :
index ef2df07224f1b11ed4e256a046f0102f562da3f9..dbb1463b7b825095078e9957f7957c7241969b32 100644 (file)
@@ -108,32 +108,62 @@ module MathView = struct
   module Signals = struct
     open GtkSignal
 
-    let clicked : ([>`math_view],_) t =
-     let marshal_clicked f _ =
+    let click : ([>`math_view],_) t =
+     let marshal_click f _ =
       function
-         [GtkArgv.POINTER element] -> f (gdome_element_of_boxed_option element)
-       | _ -> invalid_arg "GtkMathView.MathView.Signals.marshal_clicked"
+         [GtkArgv.POINTER element; GtkArgv.INT state] ->
+          f (gdome_element_of_boxed_option element) state
+       | _ -> invalid_arg "GtkMathView.MathView.Signals.marshal_click"
      in
-      { name = "clicked"; classe = `math_view; marshaller = marshal_clicked }
+      { name = "click"; classe = `math_view; marshaller = marshal_click }
 
-    let press_move : ([>`math_view],_) t =
-     let marshal_press_move f _ =
+    let element_over : ([>`math_view],_) t =
+     let marshal_element_over f _ =
       function
-         [GtkArgv.POINTER first; GtkArgv.POINTER last] ->
-          f (gdome_element_option_of_boxed_option first)
-            (gdome_element_option_of_boxed_option last)
-       | _ -> invalid_arg "GtkMathView.MathView.Signals.marshal_press_move"
+         [GtkArgv.POINTER element; GtkArgv.INT state] ->
+          f (gdome_element_option_of_boxed_option element) state
+       | _ -> invalid_arg "GtkMathView.MathView.Signals.marshal_element_over"
      in
-      { name = "press_move"; classe = `math_view;
-        marshaller = marshal_press_move }
+      { name = "element_over"; classe = `math_view;
+        marshaller = marshal_element_over }
 
-    let element_changed : ([>`math_view],_) t =
-     let marshal_element_changed f _ =
+    let select_begin : ([>`math_view],_) t =
+     let marshal_select_begin f _ =
       function
-         [GtkArgv.POINTER element] -> f (gdome_element_option_of_boxed_option element)
-       | _ -> invalid_arg "GtkMathView.MathView.Signals.marshal_element_changed"
+         [GtkArgv.POINTER element; GtkArgv.INT state] ->
+          f (gdome_element_option_of_boxed_option element) state
+       | _ -> invalid_arg "GtkMathView.MathView.Signals.marshal_select_begin"
      in
-      { name = "element_changed"; classe = `math_view;
-        marshaller = marshal_element_changed }
+      { name = "select_begin"; classe = `math_view;
+        marshaller = marshal_select_begin }
+
+    let select_over : ([>`math_view],_) t =
+     let marshal_select_over f _ =
+      function
+         [GtkArgv.POINTER element; GtkArgv.INT state] ->
+          f (gdome_element_option_of_boxed_option element) state
+       | _ -> invalid_arg "GtkMathView.MathView.Signals.marshal_select_over"
+     in
+      { name = "select_over"; classe = `math_view;
+        marshaller = marshal_select_over }
+
+    let select_end : ([>`math_view],_) t =
+     let marshal_select_end f _ =
+      function
+         [GtkArgv.POINTER element; GtkArgv.INT state] ->
+          f (gdome_element_option_of_boxed_option element) state
+       | _ -> invalid_arg "GtkMathView.MathView.Signals.marshal_select_end"
+     in
+      { name = "select_end"; classe = `math_view;
+        marshaller = marshal_select_end }
+
+    let select_abort : ([>`math_view],_) t =
+     let marshal_select_abort f _ =
+      function
+         [] -> f ()
+       | _ -> invalid_arg "GtkMathView.MathView.Signals.marshal_select_abort"
+     in
+      { name = "select_abort"; classe = `math_view;
+        marshaller = marshal_select_abort }
   end
 end
index 96278f2b8e1334fbba5779d9724836d8badde17c..2c3d80c8112a86aec568d818b0c52a5048015e95 100644 (file)
@@ -154,7 +154,7 @@ value ml_gtk_math_view_gdome_element_of_boxed_option (value arg1)
    if (arg1==Val_int(0)) {
       assert(0);
    } else {
-      nr = (GdomeElement*) Field(Field(arg1,0), 1);
+      nr = (GdomeElement*) Field(Field(arg1,0),1);
    }
    res = Val_Element(nr);
    if (res==Val_int(0)) {
index 2bbdbb0b43f56eb5cd143bc110378daf44d9f59f..76b2856d30e5e5f2a8a99f975e66bfdfeef5a61a 100644 (file)
@@ -40,10 +40,10 @@ let selection_changed mathview (element : Gdome.element option) =
  flush stdout
 ;;
 
-let element_changed mathview (element : Gdome.element option) =
- print_endline ("element_changed: " ^
+let element_over mathview (element : Gdome.element option) _ =
+ print_endline ("element_over: " ^
   (match element with
-      None -> "element_changed on nothing"
+      None -> "element_over on nothing"
     | Some element -> element#get_tagName#to_string
   )
  ) ;
@@ -102,10 +102,10 @@ let rec action mathview (element : Gdome.element) =
        end
      | None -> assert false (* every element has a parent *)
 
-let clicked mathview (element : Gdome.element) =
+let click mathview (element : Gdome.element) _ =
  let module G = Gdome in
   if not (jump element) then
-  if not (action mathview element) then
+  if not (mathview#action_toggle element) then
   (*
    match mathview#get_action with
       Some n ->
@@ -409,9 +409,9 @@ ignore(button_t1#connect#clicked (activate_t1 mathview)) ;
 ignore(button_get_font_manager_type#connect#clicked (get_font_manager_type mathview)) ;
 ignore(button_get_transparency#connect#clicked (get_transparency mathview)) ;
 ignore(button_set_transparency#connect#clicked (set_transparency mathview)) ;
-ignore(mathview#connect#clicked (clicked mathview)) ;
+ignore(mathview#connect#click (click mathview)) ;
 ignore(mathview#connect#selection_changed (selection_changed mathview));
-ignore(mathview#connect#element_changed (element_changed mathview)) ;
+ignore(mathview#connect#element_over (element_over mathview)) ;
 ignore(button_load_dom#connect#clicked (load_doc mathview)) ;
 (* Main Loop *)
 main_window#show () ;