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));
- self#newScript ()
+ 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))
- method private newScript () =
+ method private save_page () =
+ if current_page >= 0 then
+ let old_script = MatitaScript.at_page current_page in
+ save_moo0 ~do_clean:false old_script old_script#status
+
+ method newScript () =
+ self#save_page ();
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)