class gui () =
(* creation order _is_ relevant for windows placement *)
let main = new mainWin () in
- let about = new aboutWin () in
let fileSel = new fileSelectionWin () in
let findRepl = new findReplWin () in
let develList = new develListWin () in
(* glade's check widgets *)
List.iter (fun w -> w#check_widgets ())
(let c w = (w :> <check_widgets: unit -> unit>) in
- [ c about; c fileSel; c main; c findRepl]);
+ [ c fileSel; c main; c findRepl]);
(* key bindings *)
List.iter (* global key bindings *)
(fun (key, callback) -> self#addKeyBinding key callback)
*)
[ ];
(* about win *)
- ignore (about#aboutWin#event#connect#delete (fun _ -> true));
- ignore (main#aboutMenuItem#connect#activate (fun _ ->
- about#aboutWin#show ()));
- connect_button about#aboutDismissButton (fun _ ->
- about#aboutWin#misc#hide ());
- about#aboutLabel#set_label (Pcre.replace ~pat:"@VERSION@"
- ~templ:BuildTimeConf.version about#aboutLabel#label);
+ let parse_txt_file file =
+ let ch = open_in (BuildTimeConf.runtime_base_dir ^ "/" ^ file) in
+ let l_rev = ref [] in
+ try
+ while true do
+ l_rev := input_line ch :: !l_rev;
+ done;
+ assert false
+ with
+ End_of_file ->
+ close_in ch;
+ List.rev !l_rev in
+ let about_dialog =
+ GWindow.about_dialog
+ ~authors:(parse_txt_file "AUTHORS")
+ (*~comments:"comments"*)
+ ~copyright:"Copyright (C) 2005, the HELM team"
+ ~license:(String.concat "\n" (parse_txt_file "LICENSE"))
+ (*?logo:GdkPixbuf.pixbuf*)
+ (*?logo_icon_name:string*)
+ ~name:"Matita"
+ ~version:BuildTimeConf.version
+ ~website:"http://helm.cs.unibo.it"
+ ()
+ in
+ ignore (main#aboutMenuItem#connect#activate
+ (fun _ -> about_dialog#present ()));
(* findRepl win *)
let show_find_Repl () =
findRepl#toplevel#misc#show ();
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
| `DELETE_EVENT -> return None));
(* menus *)
List.iter (fun w -> w#misc#set_sensitive false) [ main#saveMenuItem ];
- main#helpMenu#set_right_justified true;
(* console *)
let adj = main#logScrolledWin#vadjustment in
ignore (adj#connect#changed
(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"))
- 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
method console = console
method sourceView: GSourceView.source_view = (source_view: GSourceView.source_view)
- method about = about
method fileSel = fileSel
method findRepl = findRepl
method main = main
projects / helm.git / blobdiff