+ (* findRepl win *)
+ let show_find_Repl () =
+ findRepl#toplevel#misc#show ();
+ findRepl#toplevel#misc#grab_focus ()
+ in
+ let hide_find_Repl () = findRepl#toplevel#misc#hide () in
+ let find_forward _ =
+ let highlight start end_ =
+ source_buffer#move_mark `INSERT ~where:start;
+ source_buffer#move_mark `SEL_BOUND ~where:end_;
+ source_view#scroll_mark_onscreen `INSERT
+ in
+ let text = findRepl#findEntry#text in
+ let iter = source_buffer#get_iter `SEL_BOUND in
+ match iter#forward_search text with
+ | None ->
+ (match source_buffer#start_iter#forward_search text with
+ | None -> ()
+ | Some (start,end_) -> highlight start end_)
+ | Some (start,end_) -> highlight start end_
+ in
+ let replace _ =
+ let text = findRepl#replaceEntry#text in
+ let ins = source_buffer#get_iter `INSERT in
+ let sel = source_buffer#get_iter `SEL_BOUND in
+ if ins#compare sel < 0 then
+ begin
+ ignore(source_buffer#delete_selection ());
+ source_buffer#insert text
+ end
+ in
+ connect_button findRepl#findButton find_forward;
+ connect_button findRepl#findReplButton replace;
+ connect_button findRepl#cancelButton (fun _ -> hide_find_Repl ());
+ ignore(findRepl#toplevel#event#connect#delete
+ ~callback:(fun _ -> hide_find_Repl ();true));
+ ignore(self#main#findReplMenuItem#connect#activate
+ ~callback:show_find_Repl);
+ ignore (findRepl#findEntry#connect#activate ~callback:find_forward);
+ (* developments win *)
+ let model =
+ new MatitaGtkMisc.multiStringListModel
+ ~cols:2 develList#developmentsTreeview
+ in
+ let refresh_devels_win () =
+ model#list_store#clear ();
+ List.iter
+ (fun (name, root) -> model#easy_mappend [name;root])
+ (MatitamakeLib.list_known_developments ())
+ in
+ let get_devel_selected () =
+ match model#easy_mselection () with
+ | [[name;_]] -> MatitamakeLib.development_for_name name
+ | _ -> assert false
+ in
+ connect_button develList#newButton
+ (fun () ->
+ next_devel_must_contain <- None;
+ newDevel#toplevel#misc#show());
+ connect_button develList#deleteButton
+ (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
+ connect_button develList#buildButton
+ (fun () ->
+ match get_devel_selected () with
+ | None -> ()
+ | Some d -> ignore(MatitamakeLib.build_development_in_bg refresh d));
+ connect_button develList#cleanButton
+ (fun () ->
+ match get_devel_selected () with
+ | None -> ()
+ | Some d -> ignore(MatitamakeLib.clean_development_in_bg refresh d));
+ connect_button develList#closeButton
+ (fun () -> develList#toplevel#misc#hide());
+ ignore(develList#toplevel#event#connect#delete
+ (fun _ -> develList#toplevel#misc#hide();true));
+ let selected_devel = ref None in
+ connect_menu_item self#main#developmentsMenuItem
+ (fun () -> refresh_devels_win ();develList#toplevel#misc#show ());
+
+ (* add development win *)
+ let check_if_root_contains root =
+ match next_devel_must_contain with
+ | None -> true
+ | Some path ->
+ let is_prefix_of d1 d2 =
+ let len1 = String.length d1 in
+ let len2 = String.length d2 in
+ if len2 < len1 then
+ false
+ else
+ let pref = String.sub d2 0 len1 in
+ pref = d1
+ in
+ is_prefix_of root path
+ in
+ connect_button newDevel#addButton
+ (fun () ->
+ let name = newDevel#nameEntry#text in
+ let root = newDevel#rootEntry#text in
+ if check_if_root_contains root then
+ begin
+ ignore (MatitamakeLib.initialize_development name root);
+ refresh_devels_win ();
+ newDevel#nameEntry#set_text "";
+ newDevel#rootEntry#set_text "";
+ newDevel#toplevel#misc#hide()
+ end
+ else
+ MatitaLog.error ("The selected root does not contain " ^
+ match next_devel_must_contain with
+ | Some x -> x
+ | _ -> assert false));
+ connect_button newDevel#chooseRootButton
+ (fun () ->
+ let path = self#chooseDir () in
+ match path with
+ | Some path -> newDevel#rootEntry#set_text path
+ | None -> ());
+ connect_button newDevel#cancelButton
+ (fun () -> newDevel#toplevel#misc#hide ());
+ ignore(newDevel#toplevel#event#connect#delete
+ (fun _ -> newDevel#toplevel#misc#hide();true));
+