[ ];
(* about win *)
let parse_txt_file file =
- let ch = open_in file in
+ let ch = open_in (BuildTimeConf.runtime_base_dir ^ "/" ^ file) in
let l_rev = ref [] in
try
while true do
let clipboard =
let atom = Gdk.Atom.clipboard in
GData.clipboard atom in
+ ignore(self#main#editMenu#connect#activate
+ ~callback:
+ (fun () ->
+ let something_selected =
+ (source_buffer#get_iter_at_mark `INSERT)#compare
+ (source_buffer#get_iter_at_mark `SEL_BOUND) <> 0
+ in
+ self#main#cutMenuItem#misc#set_sensitive something_selected;
+ self#main#copyMenuItem#misc#set_sensitive something_selected;
+ self#main#deleteMenuItem#misc#set_sensitive something_selected;
+ self#main#pasteMenuItem#misc#set_sensitive (clipboard#text <> None)
+ ));
ignore(self#main#cutMenuItem#connect#activate
~callback:(fun () -> source_view#buffer#cut_clipboard clipboard));
ignore(self#main#copyMenuItem#connect#activate
(MatitaScript.instance ())#clean_dirty_lock));
ignore(self#main#deleteMenuItem#connect#activate
~callback:(fun () -> ignore (source_view#buffer#delete_selection ())));
+ ignore(self#main#selectAllMenuItem#connect#activate
+ ~callback:(fun () ->
+ source_buffer#move_mark `INSERT source_buffer#start_iter;
+ source_buffer#move_mark `SEL_BOUND source_buffer#end_iter));
ignore(self#main#findReplMenuItem#connect#activate
~callback:show_find_Repl);
ignore (findRepl#findEntry#connect#activate ~callback:find_forward);
(* interface lockers *)
let lock_world _ =
main#buttonsToolbar#misc#set_sensitive false;
+ develList#buttonsHbox#misc#set_sensitive false;
source_view#set_editable false
in
let unlock_world _ =
main#buttonsToolbar#misc#set_sensitive true;
+ develList#buttonsHbox#misc#set_sensitive true;
source_view#set_editable true
in
let locker f =
fun () ->
lock_world ();
- try f ();unlock_world () with exc -> unlock_world (); raise exc
- in
+ try f ();unlock_world () with exc -> unlock_world (); raise exc in
+ let keep_focus f =
+ fun () ->
+ try
+ f (); source_view#misc#grab_focus ()
+ with
+ exc -> source_view#misc#grab_focus (); raise exc in
(* developments win *)
let model =
new MatitaGtkMisc.multiStringListModel
| [[name;_]] -> MatitamakeLib.development_for_name name
| _ -> assert false
in
+ let refresh () =
+ while Glib.Main.pending () do
+ ignore(Glib.Main.iteration false);
+ done
+ in
connect_button develList#newButton
(fun () ->
next_devel_must_contain <- None;
newDevel#toplevel#misc#show());
connect_button develList#deleteButton
- (fun () ->
+ (locker (fun () ->
(match get_devel_selected () with
| None -> ()
- | Some d -> MatitamakeLib.destroy_development d);
- refresh_devels_win ());
- let refresh () =
- while Glib.Main.pending () do
- ignore(Glib.Main.iteration false);
- done
- in
+ | Some d -> MatitamakeLib.destroy_development_in_bg refresh d);
+ refresh_devels_win ()));
connect_button develList#buildButton
- (fun () ->
+ (locker (fun () ->
match get_devel_selected () with
| None -> ()
| Some d ->
let build = locker
(fun () -> MatitamakeLib.build_development_in_bg refresh d)
in
- ignore(build ()));
+ ignore(build ())));
connect_button develList#cleanButton
- (fun () ->
+ (locker (fun () ->
match get_devel_selected () with
| None -> ()
| Some d ->
let clean = locker
(fun () -> MatitamakeLib.clean_development_in_bg refresh d)
in
- ignore(clean ()));
+ ignore(clean ())));
connect_button develList#closeButton
(fun () -> develList#toplevel#misc#hide());
ignore(develList#toplevel#event#connect#delete
(tac_w_term (A.Transitivity (loc, hole)));
connect_button tbar#assumptionButton (tac (A.Assumption loc));
connect_button tbar#cutButton (tac_w_term (A.Cut (loc, None, hole)));
- connect_button tbar#autoButton (tac (A.Auto (loc,None,None)));
+ connect_button tbar#autoButton (tac (A.Auto (loc,None,None,None))); (* ALB *)
MatitaGtkMisc.toggle_widget_visibility
~widget:(self#main#tacticsButtonsHandlebox :> GObj.widget)
~check:self#main#tacticsBarMenuItem;
script#reset ();
script#assignFileName f;
source_view#source_buffer#begin_not_undoable_action ();
- script#loadFromFile ();
+ script#loadFromFile f;
source_view#source_buffer#end_not_undoable_action ();
console#message ("'"^f^"' loaded.\n");
self#_enableSaveTo f
in
let cursor () =
source_buffer#place_cursor
- (source_buffer#get_iter_at_mark (`NAME "locked"));
- source_view#misc#grab_focus ()
- in
+ (source_buffer#get_iter_at_mark (`NAME "locked")) in
let advance _ = (MatitaScript.instance ())#advance (); cursor () in
let retract _ = (MatitaScript.instance ())#retract (); cursor () in
let top _ = (MatitaScript.instance ())#goto `Top (); cursor () in
let bottom _ = (MatitaScript.instance ())#goto `Bottom (); cursor () in
let jump _ = (MatitaScript.instance ())#goto `Cursor (); cursor () in
- let advance = locker advance in
- let retract = locker retract in
- let top = locker top in
- let bottom = locker bottom in
- let jump = locker jump in
+ let advance = locker (keep_focus advance) in
+ let retract = locker (keep_focus retract) in
+ let top = locker (keep_focus top) in
+ let bottom = locker (keep_focus bottom) in
+ let jump = locker (keep_focus jump) in
let connect_key sym f =
connect_key self#main#mainWinEventBox#event
~modifiers:[`CONTROL] ~stop:true sym f;
let script = MatitaScript.instance () in
script#reset ();
script#assignFileName file;
- if not (Sys.file_exists file) then
- begin
- let oc = open_out file in
- let template = MatitaMisc.input_file BuildTimeConf.script_template in
- output_string oc template;
- close_out oc
- end;
- source_view#source_buffer#begin_not_undoable_action ();
- script#loadFromFile ();
- source_view#source_buffer#end_not_undoable_action ();
- console#message ("'"^file^"' loaded.");
- self#_enableSaveTo file
+ let content =
+ if Sys.file_exists file then file
+ else BuildTimeConf.script_template
+ in
+ source_view#source_buffer#begin_not_undoable_action ();
+ script#loadFromFile content;
+ source_view#source_buffer#end_not_undoable_action ();
+ console#message ("'"^file^"' loaded.");
+ self#_enableSaveTo file
method setStar name b =
let l = main#scriptLabel in
projects / helm.git / blobdiff