(* this is a shit and should be changed :-{ *)
let interactive_uri_choice
?(selection_mode:[`SINGLE|`MULTIPLE] = `MULTIPLE) ?(title = "")
(* this is a shit and should be changed :-{ *)
let interactive_uri_choice
?(selection_mode:[`SINGLE|`MULTIPLE] = `MULTIPLE) ?(title = "")
let baseuri = status#baseuri in
match script#bos, script#eos with
| true, _ -> ()
| _, true ->
GrafiteTypes.Serializer.serialize ~baseuri:(NUri.uri_of_string baseuri)
status
let baseuri = status#baseuri in
match script#bos, script#eos with
| true, _ -> ()
| _, true ->
GrafiteTypes.Serializer.serialize ~baseuri:(NUri.uri_of_string baseuri)
status
val mutable chosen_file = None
val mutable _ok_not_exists = false
val mutable _only_directory = false
val mutable chosen_file = None
val mutable _ok_not_exists = false
val mutable _only_directory = false
- (fun (key, callback) -> self#addKeyBinding key callback)
+ (fun (key, modifiers, callback) ->
+ self#addKeyBinding key ~modifiers callback)
(*
[ GdkKeysyms._F3,
toggle_win ~check:main#showProofMenuItem proof#proofWin;
GdkKeysyms._F4,
toggle_win ~check:main#showCheckMenuItem check#checkWin;
*)
(*
[ GdkKeysyms._F3,
toggle_win ~check:main#showProofMenuItem proof#proofWin;
GdkKeysyms._F4,
toggle_win ~check:main#showCheckMenuItem check#checkWin;
*)
connect_menu_item main#newMenuItem self#newScript;
connect_menu_item main#closeMenuItem self#closeCurrentScript;
connect_menu_item main#showCoercionsGraphMenuItem
connect_menu_item main#newMenuItem self#newScript;
connect_menu_item main#closeMenuItem self#closeCurrentScript;
connect_menu_item main#showCoercionsGraphMenuItem
main#hpaneScriptSequent#set_position script_w;
(* math view handling *)
connect_menu_item main#newCicBrowserMenuItem (fun () ->
main#hpaneScriptSequent#set_position script_w;
(* math view handling *)
connect_menu_item main#newCicBrowserMenuItem (fun () ->
connect_menu_item main#increaseFontSizeMenuItem
MatitaMisc.increase_font_size;
connect_menu_item main#decreaseFontSizeMenuItem
MatitaMisc.decrease_font_size;
connect_menu_item main#normalFontSizeMenuItem
MatitaMisc.reset_font_size;
connect_menu_item main#increaseFontSizeMenuItem
MatitaMisc.increase_font_size;
connect_menu_item main#decreaseFontSizeMenuItem
MatitaMisc.decrease_font_size;
connect_menu_item main#normalFontSizeMenuItem
MatitaMisc.reset_font_size;
- ignore (main#scriptNotebook#connect#switch_page
- (fun page ->
- let script = MatitaScript.at_page page in
- script#activate;
- main#saveMenuItem#misc#set_sensitive script#has_name));
+ ignore (main#scriptNotebook#connect#switch_page (fun page ->
+ self#save_page ();
+ current_page <- page;
+ let script = MatitaScript.at_page page in
+ script#activate;
+ main#saveMenuItem#misc#set_sensitive script#has_name))
let _ =
GMisc.label ~text:"" ~packing:(hbox#pack ~expand:true ~fill:true) () in
let closebutton =
GButton.button ~relief:`NONE ~packing:hbox#pack () in
let _ =
GMisc.label ~text:"" ~packing:(hbox#pack ~expand:true ~fill:true) () in
let closebutton =
GButton.button ~relief:`NONE ~packing:hbox#pack () in
closebutton#set_image image#coerce;
let script = MatitaScript.script ~parent:scrolledWindow ~tab_label () in
ignore (main#scriptNotebook#prepend_page ~tab_label:hbox#coerce
scrolledWindow#coerce);
ignore (closebutton#connect#clicked (fun () ->
closebutton#set_image image#coerce;
let script = MatitaScript.script ~parent:scrolledWindow ~tab_label () in
ignore (main#scriptNotebook#prepend_page ~tab_label:hbox#coerce
scrolledWindow#coerce);
ignore (closebutton#connect#clicked (fun () ->
- method private addKeyBinding key callback =
- List.iter (fun evbox -> add_key_binding key callback evbox)
+ method private addKeyBinding key ?modifiers callback =
+(* List.iter (fun evbox -> add_key_binding key callback evbox) *)
+ List.iter (fun evbox -> connect_key evbox#event key ?modifiers callback)