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;;
*)
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)
- method set_href_callback = (function _ -> () : (string -> unit) option -> unit)
+
+ val mutable href_callback: (string -> unit) option = None
+ method set_href_callback f = href_callback <- f
+
+ val mutable href_statusbar_msg:
+ (GMisc.statusbar_context * Gtk.statusbar_message) option = None
+ (* <statusbar ctxt, statusbar msg> *)
+
method private set_cic_info = (function _ -> () : unit (*(Cic.conjecture option * (Cic.id, Cic.term) Hashtbl.t *
(Cic.id, Cic.hypothesis) Hashtbl.t *
(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;
- let hyperlink_tag = self#buffer#create_tag [`FOREGROUND "green"] in
+ 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 ->
+ match GdkEvent.get_type event with
+ | `MOTION_NOTIFY ->
+ Gdk.Window.set_cursor
+ (match self#get_window `TEXT with None -> assert false | Some x -> x)
+ (Gdk.Cursor.create `ARROW);
+ HExtlib.iter_option (fun (ctxt, msg) -> ctxt#remove msg)
+ 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)) ->
- self#buffer#apply_tag hyperlink_tag
- ~start:(self#buffer#get_iter (`OFFSET start))
- ~stop:(self#buffer#get_iter (`OFFSET stop))
+ ( 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));
) hyperlinks
+
+
method action_toggle = (fun _ -> assert false : document_element -> bool)
method remove_selections = (() : unit)
method set_selection = (fun _ -> () : document_element option -> unit)
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
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
ignore (domImpl#saveDocumentToFile ~name ~doc:mathml ())
end;*)
self#load_root ~root:txt;
- (*current_mathml <- Some mathml*)(*)*);
+ (*current_mathml <- Some mathml*)(* ) *);
end
(** constructors *)
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
projects / helm.git / blobdiff