On-going porting to lablgtk3

[helm.git] / matita / matita / cicMathView.ml

diff --git a/matita/matita/cicMathView.ml b/matita/matita/cicMathView.ml
index d619482de46779081001caffab56a328dcd8c8ff..ceb2e1f0df193b19d96ce856e895390c421419e0 100644 (file)
--- a/matita/matita/cicMathView.ml
+++ b/matita/matita/cicMathView.ml
@@ -28,7 +28,7 @@ open Printf
 open GrafiteTypes
 open MatitaGtkMisc
 open MatitaGuiTypes
-open GtkSourceView2
+open GtkSourceView3
 
 let matita_script_current = ref (fun _ -> (assert false : < advance: ?statement:string -> unit -> unit; status: GrafiteTypes.status >));;
 let register_matita_script_current f = matita_script_current := f;;
@@ -174,9 +174,9 @@ let string_of_dom_node node =
 *)
 
 class clickableMathView obj =
-let text_width = 80 in
+(*let text_width = 80 in*)
 object (self)
-  inherit GSourceView2.source_view obj
+  inherit GSourceView3.source_view obj
 
   method strings_of_selection = (assert false : (paste_kind * string) list)
 
@@ -192,9 +192,7 @@ object (self)
          (Cic.id, Cic.id option) Hashtbl.t * ('a, 'b) Hashtbl.t * 'c option)*) option -> unit)
   (* dal widget di Luca *)
   method load_root ~root:(hyperlinks,text) =
-    self#buffer#delete ~start:(self#buffer#get_iter `START)
-    ~stop:(self#buffer#get_iter `END);
-    self#buffer#insert text;
+    self#buffer#set_text text;
     let all_tag = self#buffer#create_tag [] in
     self#buffer#apply_tag all_tag ~start:(self#buffer#get_iter `START)
      ~stop:(self#buffer#get_iter `END);
@@ -209,31 +207,41 @@ object (self)
               href_statusbar_msg;
              false
          | _ -> false));
+     let hyperlink_tag = self#buffer#create_tag [] in
+     ignore(hyperlink_tag#connect#event
+       ~callback:(fun ~origin event pos ->
+         let offset = (new GText.iter pos)#offset in
+         let _,_,href =
+          try
+           List.find
+            (fun (start,stop,href) -> start <= offset && offset <= stop
+            ) hyperlinks
+          with
+           Not_found -> assert false
+         in
+         match GdkEvent.get_type event with
+            `BUTTON_PRESS -> 
+              (match href_callback with
+                  None -> ()
+                | Some f -> f href);
+              true
+          | `MOTION_NOTIFY -> 
+              Gdk.Window.set_cursor
+               (match self#get_window `TEXT with None -> assert false | Some x -> x)
+               (Gdk.Cursor.create `HAND1);
+              let ctxt = (MatitaMisc.get_gui ())#main#statusBar#new_context ~name:"href" in
+              let msg = ctxt#push href in
+              href_statusbar_msg <- Some (ctxt, msg);
+              false
+          | _ -> false));
      List.iter
       ( fun (start,stop,(href : string)) ->
-         let hyperlink_tag = self#buffer#create_tag [] in
           self#buffer#apply_tag hyperlink_tag
            ~start:(self#buffer#get_iter_at_char start)
            ~stop:(self#buffer#get_iter_at_char (stop+1));
-          ignore(hyperlink_tag#connect#event
-            ~callback:(fun ~origin event pos ->
-              match GdkEvent.get_type event with
-                 `BUTTON_PRESS -> 
-                   (match href_callback with
-                       None -> ()
-                     | Some f -> f href);
-                   true
-               | `MOTION_NOTIFY -> 
-                   Gdk.Window.set_cursor
-                    (match self#get_window `TEXT with None -> assert false | Some x -> x)
-                    (Gdk.Cursor.create `HAND1);
-                   let ctxt = (MatitaMisc.get_gui ())#main#statusBar#new_context ~name:"href" in
-                   let msg = ctxt#push href in
-                   href_statusbar_msg <- Some (ctxt, msg);
-                   false
-               | _ -> false));
       ) hyperlinks
 
+
   method action_toggle = (fun _ -> assert false : document_element -> bool)
   method remove_selections = (() : unit)
   method set_selection = (fun _ -> () : document_element option -> unit)
@@ -682,7 +690,7 @@ let cicMathView (*?auto_indent ?highlight_current_line ?indent_on_tab ?indent_wi
         Gobject.set_params (Gobject.try_cast obj "GtkSourceView") pl;
         new _cicMathView obj)(*)) ?auto_indent ?highlight_current_line ?indent_on_tab ?indent_width ?insert_spaces_instead_of_tabs ?right_margin_position ?show_line_marks ?show_line_numbers ?show_right_margin ?smart_home_end ?tab_width ?editable ?cursor_visible ?justification ?wrap_mode ?accepts_tab ?border_width*) [] ?width ?height ?packing ?show () :> cicMathView)
 
-let screenshot status sequents metasenv subst (filename as ofn) =
+let screenshot status sequents metasenv subst (filename (*as ofn*)) =
  () (*MATITA 1.0
   let w = GWindow.window ~title:"screenshot" () in
   let width = 500 in