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 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 ();
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;
+ source_view#set_editable false
+ in
+ let unlock_world _ =
+ main#buttonsToolbar#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
(* developments win *)
let model =
new MatitaGtkMisc.multiStringListModel
(fun () ->
match get_devel_selected () with
| None -> ()
- | Some d -> ignore(MatitamakeLib.build_development_in_bg refresh d));
+ | Some d ->
+ let build = locker
+ (fun () -> MatitamakeLib.build_development_in_bg refresh d)
+ in
+ ignore(build ()));
connect_button develList#cleanButton
(fun () ->
match get_devel_selected () with
| None -> ()
- | Some d -> ignore(MatitamakeLib.clean_development_in_bg refresh d));
+ | Some d ->
+ let clean = locker
+ (fun () -> MatitamakeLib.clean_development_in_bg refresh d)
+ in
+ ignore(clean ()));
connect_button develList#closeButton
(fun () -> develList#toplevel#misc#hide());
ignore(develList#toplevel#event#connect#delete
source_buffer#place_cursor
(source_buffer#get_iter_at_mark (`NAME "locked"))
in
- let lock_world _ =
- main#buttonsToolbar#misc#set_sensitive false;
- source_view#set_editable false
- in
- let unlock_world _ =
- main#buttonsToolbar#misc#set_sensitive true;
- source_view#set_editable true
- 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 locker f =
- fun () ->
- lock_world ();
- try f ();unlock_world () with exc -> unlock_world (); raise exc
- in
let advance = locker advance in
let retract = locker retract in
let top = locker top 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