X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaGui.ml;h=8351426f88702e4191141634596cafd1c2323c6a;hb=5b17a67ffd16485adf2e66a6241b72e91ed15621;hp=108b36bfb3f8738ac008a02f65bf1e7207488ef6;hpb=c1902bcdefa7ef7770e470a49fc778f8846cca62;p=helm.git diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml index 108b36bfb..8351426f8 100644 --- a/helm/matita/matitaGui.ml +++ b/helm/matita/matitaGui.ml @@ -29,7 +29,7 @@ open MatitaGeneratedGui open MatitaGtkMisc open MatitaMisc -let gui_instance = ref None ;; +let gui_instance = ref None class type browserWin = (* this class exists only because GEdit.combo_box_entry is not supported by @@ -67,7 +67,8 @@ let clean_current_baseuri status = let ask_and_save_moo_if_needed parent fname status = let save () = - MatitacLib.dump_moo_to_file fname status.MatitaTypes.moo_content_rev in + let moo_fname = MatitaMisc.obj_file_of_script fname in + MatitaMoo.save_moo moo_fname status.MatitaTypes.moo_content_rev in if (MatitaScript.instance ())#eos && status.MatitaTypes.proof_status = MatitaTypes.No_proof then @@ -80,7 +81,7 @@ let ask_and_save_moo_if_needed parent fname status = ~title:"A .moo can be generated" ~message:(Printf.sprintf "%s can be generated for %s.\nShould I generate it?" - mooname fname) + (Filename.basename mooname) (Filename.basename fname)) ~parent () in let b = @@ -110,7 +111,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 @@ -171,15 +172,13 @@ class gui () = (*~comments:"comments"*) ~copyright:"Copyright (C) 2005, the HELM team" ~license:(String.concat "\n" (parse_txt_file "LICENSE")) - (*?logo:GdkPixbuf.pixbuf*) - (*?logo_icon_name:string*) + ~logo:(GdkPixbuf.from_file (MatitaMisc.image_path "/matita_medium.png")) ~name:"Matita" ~version:BuildTimeConf.version ~website:"http://helm.cs.unibo.it" () in - ignore (main#aboutMenuItem#connect#activate - (fun _ -> about_dialog#present ())); + connect_menu_item main#aboutMenuItem about_dialog#present; (* findRepl win *) let show_find_Repl () = findRepl#toplevel#misc#show (); @@ -292,12 +291,12 @@ class gui () = source_view#source_buffer#redo (); source_view#misc#grab_focus () in - ignore(self#main#undoMenuItem#connect#activate ~callback:safe_undo); + connect_menu_item main#undoMenuItem safe_undo; ignore(source_view#source_buffer#connect#can_undo - ~callback:self#main#undoMenuItem#misc#set_sensitive); - ignore(self#main#redoMenuItem#connect#activate ~callback:safe_redo); + ~callback:main#undoMenuItem#misc#set_sensitive); + connect_menu_item main#redoMenuItem safe_redo; ignore(source_view#source_buffer#connect#can_redo - ~callback:self#main#redoMenuItem#misc#set_sensitive); + ~callback:main#redoMenuItem#misc#set_sensitive); ignore(source_view#connect#after#populate_popup ~callback:(fun pre_menu -> let menu = new GMenu.menu pre_menu in @@ -316,7 +315,7 @@ class gui () = new_undoMenuItem#misc#set_sensitive (undoMenuItem#misc#get_flag `SENSITIVE); menu#remove (undoMenuItem :> GMenu.menu_item); - ignore(new_undoMenuItem#connect#activate ~callback:safe_undo); + connect_menu_item new_undoMenuItem safe_undo; let new_redoMenuItem = GMenu.image_menu_item ~image:(GMisc.image ~stock:`REDO ()) @@ -326,38 +325,62 @@ class gui () = 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#cutMenuItem#connect#activate - ~callback:(fun () -> source_view#buffer#cut_clipboard clipboard)); - ignore(self#main#copyMenuItem#connect#activate - ~callback:(fun () -> source_view#buffer#copy_clipboard clipboard)); - ignore(self#main#pasteMenuItem#connect#activate - ~callback:(fun () -> - source_view#buffer#paste_clipboard clipboard; - (MatitaScript.instance ())#clean_dirty_lock)); - ignore(self#main#deleteMenuItem#connect#activate - ~callback:(fun () -> ignore (source_view#buffer#delete_selection ()))); - ignore(self#main#findReplMenuItem#connect#activate - ~callback:show_find_Repl); - ignore (findRepl#findEntry#connect#activate ~callback:find_forward); + connect_menu_item new_redoMenuItem safe_redo)); + let clipboard = GData.clipboard Gdk.Atom.clipboard in + let text_selected () = + (source_buffer#get_iter_at_mark `INSERT)#compare + (source_buffer#get_iter_at_mark `SEL_BOUND) <> 0 + in + let markup_selected () = MatitaMathView.get_selections () <> None in + connect_menu_item main#editMenu (fun () -> + let text_selected = text_selected () in + let markup_selected = markup_selected () in + let something_selected = text_selected || markup_selected in + main#cutMenuItem#misc#set_sensitive text_selected; + main#copyMenuItem#misc#set_sensitive something_selected; + main#deleteMenuItem#misc#set_sensitive text_selected; + main#pasteMenuItem#misc#set_sensitive (clipboard#text <> None)); + connect_menu_item main#cutMenuItem (fun () -> + source_view#buffer#cut_clipboard clipboard); + connect_menu_item main#copyMenuItem (fun () -> + if text_selected () then + source_view#buffer#copy_clipboard clipboard + else if markup_selected () then + match MatitaMathView.get_selections () with + | None + | Some [] -> () + | Some (s :: _) -> clipboard#set_text s); + connect_menu_item main#pasteMenuItem (fun () -> + source_view#buffer#paste_clipboard clipboard; + (MatitaScript.instance ())#clean_dirty_lock); + connect_menu_item main#deleteMenuItem (fun () -> + ignore (source_view#buffer#delete_selection ())); + connect_menu_item main#selectAllMenuItem (fun () -> + source_buffer#move_mark `INSERT source_buffer#start_iter; + source_buffer#move_mark `SEL_BOUND source_buffer#end_iter); + connect_menu_item main#findReplMenuItem show_find_Repl; + ignore (findRepl#findEntry#connect#activate 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 @@ -372,47 +395,47 @@ class gui () = let get_devel_selected () = match model#easy_mselection () with | [[name;_]] -> MatitamakeLib.development_for_name name - | _ -> assert false + | _ -> None + 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 (fun _ -> develList#toplevel#misc#hide();true)); let selected_devel = ref None in - connect_menu_item self#main#developmentsMenuItem + connect_menu_item main#developmentsMenuItem (fun () -> refresh_devels_win ();develList#toplevel#misc#show ()); (* add development win *) @@ -472,9 +495,9 @@ class gui () = let fname = fileSel#fileSelectionWin#filename in if Sys.file_exists fname then begin - if is_regular fname && not(_only_directory) then + if HExtlib.is_regular fname && not (_only_directory) then return (Some fname) - else if _only_directory && is_dir fname then + else if _only_directory && HExtlib.is_dir fname then return (Some fname) end else @@ -495,7 +518,7 @@ class gui () = (* toolbar *) let module A = GrafiteAst in let hole = CicNotationPt.UserInput in - let loc = Disambiguate.dummy_floc in + let loc = DisambiguateTypes.dummy_floc in let tac ast _ = if (MatitaScript.instance ())#onGoingProof () then (MatitaScript.instance ())#advance @@ -508,12 +531,14 @@ class gui () = buf#insert ~iter:(buf#get_iter_at_mark (`NAME "locked")) ("\n" ^ GrafiteAstPp.pp_tactic ast) in - let tbar = self#main in + let tbar = main in connect_button tbar#introsButton (tac (A.Intros (loc, None, []))); connect_button tbar#applyButton (tac_w_term (A.Apply (loc, hole))); connect_button tbar#exactButton (tac_w_term (A.Exact (loc, hole))); - connect_button tbar#elimButton (tac_w_term (A.Elim (loc, hole, None, None, []))); - connect_button tbar#elimTypeButton (tac_w_term (A.ElimType (loc, hole, None, None, []))); + connect_button tbar#elimButton (tac_w_term + (A.Elim (loc, hole, None, None, []))); + connect_button tbar#elimTypeButton (tac_w_term + (A.ElimType (loc, hole, None, None, []))); connect_button tbar#splitButton (tac (A.Split loc)); connect_button tbar#leftButton (tac (A.Left loc)); connect_button tbar#rightButton (tac (A.Right loc)); @@ -524,25 +549,28 @@ 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,None))); MatitaGtkMisc.toggle_widget_visibility - ~widget:(self#main#tacticsButtonsHandlebox :> GObj.widget) - ~check:self#main#tacticsBarMenuItem; + ~widget:(main#tacticsButtonsHandlebox :> GObj.widget) + ~check:main#tacticsBarMenuItem; let module Hr = Helm_registry in if not (Hr.get_opt_default Hr.bool ~default:false "matita.tactics_bar") then - self#main#tacticsBarMenuItem#set_active false; + main#tacticsBarMenuItem#set_active false; MatitaGtkMisc.toggle_callback ~callback:(function - | true -> self#main#toplevel#fullscreen () - | false -> self#main#toplevel#unfullscreen ()) - ~check:self#main#fullscreenMenuItem; - self#main#fullscreenMenuItem#set_active false; + | true -> main#toplevel#fullscreen () + | false -> main#toplevel#unfullscreen ()) + ~check:main#fullscreenMenuItem; + main#fullscreenMenuItem#set_active false; (* log *) MatitaLog.set_log_callback self#console#log_callback; GtkSignal.user_handler := - (fun exn -> MatitaLog.error (MatitaExcPp.to_string exn)); + (fun exn -> + if Helm_registry.get_bool "matita.catch_top_level_exn" then + MatitaLog.error (MatitaExcPp.to_string exn) + else raise exn); (* script *) let _ = match GSourceView.source_language_from_file BuildTimeConf.lang_file with @@ -556,7 +584,7 @@ class gui () = let s () = MatitaScript.instance () in let disableSave () = script_fname <- None; - self#main#saveMenuItem#misc#set_sensitive false + main#saveMenuItem#misc#set_sensitive false in let saveAsScript () = let script = s () in @@ -580,19 +608,19 @@ class gui () = let script = s () in let status = script#status in try - if source_view#buffer#modified then - begin - match ask_unsaved main#toplevel with - | `YES -> saveScript () - | `NO -> () - | `CANCEL -> raise MatitaTypes.Cancel - end; - (match script_fname with - | None -> () - | Some fname -> - ask_and_save_moo_if_needed main#toplevel fname status); match self#chooseFile () with | Some f -> + if source_view#buffer#modified then + begin + match ask_unsaved main#toplevel with + | `YES -> saveScript () + | `NO -> () + | `CANCEL -> raise MatitaTypes.Cancel + end; + (match script_fname with + | None -> () + | Some fname -> + ask_and_save_moo_if_needed main#toplevel fname status); script#reset (); script#assignFileName f; source_view#source_buffer#begin_not_undoable_action (); @@ -613,21 +641,19 @@ 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 + connect_key main#mainWinEventBox#event ~modifiers:[`CONTROL] ~stop:true sym f; connect_key self#sourceView#event ~modifiers:[`CONTROL] ~stop:true sym f @@ -664,19 +690,19 @@ class gui () = GMain.Main.quit () with MatitaTypes.Cancel -> ()) end); - connect_button self#main#scriptAdvanceButton advance; - connect_button self#main#scriptRetractButton retract; - connect_button self#main#scriptTopButton top; - connect_button self#main#scriptBottomButton bottom; + connect_button main#scriptAdvanceButton advance; + connect_button main#scriptRetractButton retract; + connect_button main#scriptTopButton top; + connect_button main#scriptBottomButton bottom; connect_key GdkKeysyms._Down advance; connect_key GdkKeysyms._Up retract; connect_key GdkKeysyms._Home top; connect_key GdkKeysyms._End bottom; - connect_button self#main#scriptJumpButton jump; - connect_menu_item self#main#openMenuItem loadScript; - connect_menu_item self#main#saveMenuItem saveScript; - connect_menu_item self#main#saveAsMenuItem saveAsScript; - connect_menu_item self#main#newMenuItem newScript; + connect_button main#scriptJumpButton jump; + connect_menu_item main#openMenuItem loadScript; + connect_menu_item main#saveMenuItem saveScript; + connect_menu_item main#saveAsMenuItem saveAsScript; + connect_menu_item main#newMenuItem newScript; connect_key GdkKeysyms._period (fun () -> source_buffer#insert ~iter:(source_buffer#get_iter_at_mark `INSERT) @@ -690,11 +716,11 @@ class gui () = (* script monospace font stuff *) self#updateFontSize (); (* debug menu *) - self#main#debugMenu#misc#hide (); + main#debugMenu#misc#hide (); (* status bar *) - self#main#hintLowImage#set_file (image_path "matita-bulb-low.png"); - self#main#hintMediumImage#set_file (image_path "matita-bulb-medium.png"); - self#main#hintHighImage#set_file (image_path "matita-bulb-high.png"); + main#hintLowImage#set_file (image_path "matita-bulb-low.png"); + main#hintMediumImage#set_file (image_path "matita-bulb-medium.png"); + main#hintHighImage#set_file (image_path "matita-bulb-high.png"); (* focus *) self#sourceView#misc#grab_focus (); (* main win dimension *) @@ -703,11 +729,50 @@ class gui () = let main_w = width * 90 / 100 in let main_h = height * 80 / 100 in let script_w = main_w * 6 / 10 in - self#main#toplevel#resize ~width:main_w ~height:main_h; - self#main#hpaneScriptSequent#set_position script_w; + main#toplevel#resize ~width:main_w ~height:main_h; + 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 @@ -734,9 +799,9 @@ class gui () = script_fname <- Some file; self#main#saveMenuItem#misc#set_sensitive true - method console = console - method sourceView: GSourceView.source_view = (source_view: GSourceView.source_view) + method sourceView: GSourceView.source_view = + (source_view: GSourceView.source_view) method fileSel = fileSel method findRepl = findRepl method main = main @@ -780,7 +845,7 @@ class gui () = keyBindingBoxes method setQuitCallback callback = - ignore (main#quitMenuItem#connect#activate callback); + connect_menu_item main#quitMenuItem callback; ignore (main#toplevel#event#connect#delete (fun _ -> callback ();true)); self#addKeyBinding GdkKeysyms._q callback @@ -844,6 +909,7 @@ class gui () = let gui () = let g = new gui () in gui_instance := Some g; + MatitaMathView.set_gui g; g let instance = singleton gui @@ -993,11 +1059,18 @@ let interactive_interp_choice () choices = let selection = dialog#interpChoiceTreeView#selection in ignore (selection#connect#changed (fun _ -> match selection#get_selected_rows with - | [path] -> - MatitaLog.debug (sprintf "selection: %d" (model#get_interp_no path)); - interp_no := Some (model#get_interp_no path) + | [path] -> interp_no := Some (model#get_interp_no path) | _ -> assert false)); dialog#interpChoiceDialog#show (); 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 ()) +