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 ();
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:(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 ()
- ));
+ 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#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
projects / helm.git / blobdiff