X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2FcicMathView.ml;h=8f6bd620423c8dce67bfeec6db229cbf2dbe2d23;hb=refs%2Fheads%2Fmaster;hp=d619482de46779081001caffab56a328dcd8c8ff;hpb=bfd488729e5f21cedaba0cccfa10fdb63da8a68f;p=helm.git diff --git a/matita/matita/cicMathView.ml b/matita/matita/cicMathView.ml index d619482de..8f6bd6204 100644 --- a/matita/matita/cicMathView.ml +++ b/matita/matita/cicMathView.ml @@ -25,10 +25,8 @@ 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 +172,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,14 +190,12 @@ 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); ignore(all_tag#connect#event - ~callback:(fun ~origin event pos -> + ~callback:(fun ~origin:_ event _pos -> match GdkEvent.get_type event with | `MOTION_NOTIFY -> Gdk.Window.set_cursor @@ -209,31 +205,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 + ( fun (start,stop,(_href : string)) -> 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) @@ -631,7 +637,7 @@ object (self) val mutable current_mathml = None method nload_sequent: - 'status. #ApplyTransformation.status as 'status -> NCic.metasenv -> + 'status. (#ApplyTransformation.status as 'status) -> NCic.metasenv -> NCic.substitution -> int -> unit = fun status metasenv subst metano -> let sequent = List.assoc metano metasenv in @@ -648,7 +654,7 @@ object (self) self#load_root ~root:txt method load_nobject : - 'status. #ApplyTransformation.status as 'status -> NCic.obj -> unit + 'status. (#ApplyTransformation.status as 'status) -> NCic.obj -> unit = fun status obj -> let txt = ApplyTransformation.ntxt_of_cic_object ~map_unicode_to_tex:false 80 status obj in @@ -669,7 +675,7 @@ object (self) ignore (domImpl#saveDocumentToFile ~name ~doc:mathml ()) end;*) self#load_root ~root:txt; - (*current_mathml <- Some mathml*)(*)*); + (*current_mathml <- Some mathml*)(* ) *); end (** constructors *) @@ -680,9 +686,9 @@ let cicMathView (*?auto_indent ?highlight_current_line ?indent_on_tab ?indent_wi GContainer.pack_container ~create:(fun pl -> let obj = SourceView.new_ () in 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) + 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