X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaGui.ml;h=fe0b4a1f9870ebd3e314363692b8d55040303bac;hb=ddff8ae1e15c9fcaf83320978a5cad509d734a74;hp=8d82497654a94546595fab91019846957ca43a5b;hpb=570fd2488f0ba8c16105dc30dd25dd00b558f0fe;p=helm.git diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml index 8d8249765..fe0b4a1f9 100644 --- a/helm/matita/matitaGui.ml +++ b/helm/matita/matitaGui.ml @@ -110,7 +110,7 @@ class gui () = let fileSel = new fileSelectionWin () in let findRepl = new findReplWin () in let develList = new develListWin () in - let newDevel = new newDevelopmentWin () in + let newDevel = new newDevelWin () in let keyBindingBoxes = (* event boxes which should receive global key events *) [ main#mainWinEventBox ] in @@ -154,7 +154,7 @@ class gui () = [ ]; (* about win *) let parse_txt_file file = - let ch = open_in file in + let ch = open_in (BuildTimeConf.runtime_base_dir ^ "/" ^ file) in let l_rev = ref [] in try while true do @@ -168,7 +168,7 @@ class gui () = let about_dialog = GWindow.about_dialog ~authors:(parse_txt_file "AUTHORS") - ~comments:"comments" + (*~comments:"comments"*) ~copyright:"Copyright (C) 2005, the HELM team" ~license:(String.concat "\n" (parse_txt_file "LICENSE")) (*?logo:GdkPixbuf.pixbuf*) @@ -331,6 +331,18 @@ class gui () = 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 @@ -341,23 +353,34 @@ class gui () = (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 @@ -374,39 +397,39 @@ class gui () = | [[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 @@ -524,7 +547,7 @@ class gui () = (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; @@ -596,7 +619,7 @@ class gui () = 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 @@ -613,19 +636,17 @@ class gui () = in let cursor () = source_buffer#place_cursor - (source_buffer#get_iter_at_mark (`NAME "locked")); - source_view#misc#grab_focus () - 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; @@ -707,24 +728,60 @@ class gui () = self#main#hpaneScriptSequent#set_position script_w; (* source_view *) ignore(source_view#connect#after#paste_clipboard - ~callback:(fun () -> (MatitaScript.instance ())#clean_dirty_lock)) + ~callback:(fun () -> (MatitaScript.instance ())#clean_dirty_lock)); + (* clean_locked is set to true only "during" a PRIMARY paste + operation (i.e. by clicking with the second mouse button) *) + let clean_locked = ref false in + ignore(source_view#event#connect#button_press + ~callback: + (fun button -> + if GdkEvent.Button.button button = 2 then + clean_locked := true; + false + )); + ignore(source_view#event#connect#button_release + ~callback:(fun button -> clean_locked := false; false)); + ignore(source_view#buffer#connect#after#apply_tag + ~callback:( + fun tag ~start:_ ~stop:_ -> + if !clean_locked && + tag#get_oid = (MatitaScript.instance ())#locked_tag#get_oid + then + begin + clean_locked := false; + (MatitaScript.instance ())#clean_dirty_lock; + clean_locked := true + end)); + (* math view handling *) + connect_menu_item main#newCicBrowserMenuItem (fun () -> + ignore (MatitaMathView.cicBrowser ())); + connect_menu_item main#increaseFontSizeMenuItem (fun () -> + self#increaseFontSize (); + MatitaMathView.increase_font_size (); + MatitaMathView.update_font_sizes ()); + connect_menu_item main#decreaseFontSizeMenuItem (fun () -> + self#decreaseFontSize (); + MatitaMathView.decrease_font_size (); + MatitaMathView.update_font_sizes ()); + connect_menu_item main#normalFontSizeMenuItem (fun () -> + self#resetFontSize (); + MatitaMathView.reset_font_size (); + MatitaMathView.update_font_sizes ()); + MatitaMathView.reset_font_size (); method loadScript file = 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 @@ -847,6 +904,7 @@ class gui () = let gui () = let g = new gui () in gui_instance := Some g; + MatitaMathView.set_gui g; g let instance = singleton gui @@ -1004,3 +1062,12 @@ let interactive_interp_choice () choices = GtkThread.main (); (match !interp_no with Some row -> [row] | _ -> raise MatitaTypes.Cancel) +let _ = + (* disambiguator callbacks *) + MatitaDisambiguator.set_choose_uris_callback (interactive_uri_choice ()); + MatitaDisambiguator.set_choose_interp_callback (interactive_interp_choice ()); + (* gtk initialization *) + GtkMain.Rc.add_default_file BuildTimeConf.gtkrc_file; (* loads gtk rc *) + GMathView.add_configuration_path BuildTimeConf.gtkmathview_conf; + ignore (GMain.Main.init ()) +