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 ();
connect_button findRepl#cancelButton (fun _ -> hide_find_Repl ());
ignore(findRepl#toplevel#event#connect#delete
~callback:(fun _ -> hide_find_Repl ();true));
- ignore(self#main#undoMenuItem#connect#activate
- ~callback:(fun () ->
- (* phase 1: we save the actual status of the marks and we undo *)
- let locked_mark = `MARK ((MatitaScript.instance ())#locked_mark) in
- let locked_iter = source_view#buffer#get_iter_at_mark locked_mark in
- let locked_iter_offset = locked_iter#offset in
- let mark2 =
- `MARK
- (source_view#buffer#create_mark ~name:"lock_point"
- ~left_gravity:true locked_iter) in
+ let safe_undo =
+ fun () ->
+ (* phase 1: we save the actual status of the marks and we undo *)
+ let locked_mark = `MARK ((MatitaScript.instance ())#locked_mark) in
+ let locked_iter = source_view#buffer#get_iter_at_mark locked_mark in
+ let locked_iter_offset = locked_iter#offset in
+ let mark2 =
+ `MARK
+ (source_view#buffer#create_mark ~name:"lock_point"
+ ~left_gravity:true locked_iter) in
+ source_view#source_buffer#undo ();
+ (* phase 2: we save the cursor position and we redo, restoring
+ the previous status of all the marks *)
+ let cursor_iter = source_view#buffer#get_iter_at_mark `INSERT in
+ let mark =
+ `MARK
+ (source_view#buffer#create_mark ~name:"undo_point"
+ ~left_gravity:true cursor_iter)
+ in
+ source_view#source_buffer#redo ();
+ let mark_iter = source_view#buffer#get_iter_at_mark mark in
+ let mark2_iter = source_view#buffer#get_iter_at_mark mark2 in
+ let mark2_iter = mark2_iter#set_offset locked_iter_offset in
+ source_view#buffer#move_mark locked_mark ~where:mark2_iter;
+ source_view#buffer#delete_mark mark;
+ source_view#buffer#delete_mark mark2;
+ (* phase 3: if after the undo the cursor was in the locked area,
+ then we move it there again and we perform a goto *)
+ if mark_iter#offset < locked_iter_offset then
+ begin
+ source_view#buffer#move_mark `INSERT ~where:mark_iter;
+ (MatitaScript.instance ())#goto `Cursor ();
+ end;
+ (* phase 4: we perform again the undo. This time we are sure that
+ the text to undo is not locked *)
source_view#source_buffer#undo ();
- (* phase 2: we save the cursor position and we redo, restoring
- the previous status of all the marks *)
- let cursor_iter = source_view#buffer#get_iter_at_mark `INSERT in
- let mark =
- `MARK
- (source_view#buffer#create_mark ~name:"undo_point"
- ~left_gravity:true cursor_iter)
- in
- source_view#source_buffer#redo ();
- let mark_iter = source_view#buffer#get_iter_at_mark mark in
- let mark2_iter = source_view#buffer#get_iter_at_mark mark2 in
- let mark2_iter = mark2_iter#set_offset locked_iter_offset in
- source_view#buffer#move_mark locked_mark ~where:mark2_iter;
- source_view#buffer#delete_mark mark;
- source_view#buffer#delete_mark mark2;
- (* phase 3: if after the undo the cursor was in the locked area,
- then we move it there again and we perform a goto *)
- if mark_iter#offset < locked_iter_offset then
- begin
- source_view#buffer#move_mark `INSERT ~where:mark_iter;
- (MatitaScript.instance ())#goto `Cursor ();
- end;
- (* phase 4: we perform again the undo. This time we are sure that
- the text to undo is not locked *)
- source_view#source_buffer#undo ();
- source_view#misc#grab_focus ()
- ));
+ source_view#misc#grab_focus () in
+ let safe_redo =
+ fun () ->
+ (* phase 1: we save the actual status of the marks, we redo and
+ we undo *)
+ let locked_mark = `MARK ((MatitaScript.instance ())#locked_mark) in
+ let locked_iter = source_view#buffer#get_iter_at_mark locked_mark in
+ let locked_iter_offset = locked_iter#offset in
+ let mark2 =
+ `MARK
+ (source_view#buffer#create_mark ~name:"lock_point"
+ ~left_gravity:true locked_iter) in
+ source_view#source_buffer#redo ();
+ source_view#source_buffer#undo ();
+ (* phase 2: we save the cursor position and we restore
+ the previous status of all the marks *)
+ let cursor_iter = source_view#buffer#get_iter_at_mark `INSERT in
+ let mark =
+ `MARK
+ (source_view#buffer#create_mark ~name:"undo_point"
+ ~left_gravity:true cursor_iter)
+ in
+ let mark_iter = source_view#buffer#get_iter_at_mark mark in
+ let mark2_iter = source_view#buffer#get_iter_at_mark mark2 in
+ let mark2_iter = mark2_iter#set_offset locked_iter_offset in
+ source_view#buffer#move_mark locked_mark ~where:mark2_iter;
+ source_view#buffer#delete_mark mark;
+ source_view#buffer#delete_mark mark2;
+ (* phase 3: if after the undo the cursor is in the locked area,
+ then we move it there again and we perform a goto *)
+ if mark_iter#offset < locked_iter_offset then
+ begin
+ source_view#buffer#move_mark `INSERT ~where:mark_iter;
+ (MatitaScript.instance ())#goto `Cursor ();
+ end;
+ (* phase 4: we perform again the redo. This time we are sure that
+ the text to redo is not locked *)
+ source_view#source_buffer#redo ();
+ source_view#misc#grab_focus ()
+ in
+ ignore(self#main#undoMenuItem#connect#activate ~callback:safe_undo);
ignore(source_view#source_buffer#connect#can_undo
~callback:self#main#undoMenuItem#misc#set_sensitive);
- ignore(self#main#redoMenuItem#connect#activate
- ~callback:source_view#source_buffer#redo);
+ ignore(self#main#redoMenuItem#connect#activate ~callback:safe_redo);
ignore(source_view#source_buffer#connect#can_redo
~callback:self#main#redoMenuItem#misc#set_sensitive);
+ ignore(source_view#connect#after#populate_popup
+ ~callback:(fun pre_menu ->
+ let menu = new GMenu.menu pre_menu in
+ let menuItems = menu#children in
+ let undoMenuItem, redoMenuItem =
+ match menuItems with
+ [undo;redo;sep1;cut;copy;paste;delete;sep2;
+ selectall;sep3;inputmethod;insertunicodecharacter] -> undo,redo
+ | _ -> assert false in
+ let new_undoMenuItem =
+ GMenu.image_menu_item
+ ~image:(GMisc.image ~stock:`UNDO ())
+ ~use_mnemonic:true
+ ~label:"_Undo"
+ ~packing:(menu#insert ~pos:0) () in
+ new_undoMenuItem#misc#set_sensitive
+ (undoMenuItem#misc#get_flag `SENSITIVE);
+ menu#remove (undoMenuItem :> GMenu.menu_item);
+ ignore(new_undoMenuItem#connect#activate ~callback:safe_undo);
+ let new_redoMenuItem =
+ GMenu.image_menu_item
+ ~image:(GMisc.image ~stock:`REDO ())
+ ~use_mnemonic:true
+ ~label:"_Redo"
+ ~packing:(menu#insert ~pos:1) () in
+ new_redoMenuItem#misc#set_sensitive
+ (redoMenuItem#misc#get_flag `SENSITIVE);
+ menu#remove (redoMenuItem :> GMenu.menu_item);
+ ignore(new_redoMenuItem#connect#activate ~callback:safe_redo);
+ ));
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
+ 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 -> 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 () ->
+ (locker (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
| `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
- 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
+ (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 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
- 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