X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaGui.ml;h=4ca67368fce43a6d4fe880ad2c75f956f5d518b5;hb=40a09a72c4e86256ace6e8b26942d1bd2238534b;hp=6308eab86e3035f0fe170ce0b24bbf82f21cb843;hpb=41be5e85a1103a5b14495bb487995a6a88e79c48;p=helm.git diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml index 6308eab86..4ca67368f 100644 --- a/helm/matita/matitaGui.ml +++ b/helm/matita/matitaGui.ml @@ -23,6 +23,8 @@ * http://helm.cs.unibo.it/ *) +(* $Id$ *) + open Printf open MatitaGeneratedGui @@ -61,24 +63,32 @@ class console ~(buffer: GText.buffer) () = | `Warning -> self#warning (s ^ "\n") end -let clean_current_baseuri status = +let clean_current_baseuri grafite_status = try - let baseuri = GrafiteTypes.get_string_option status "baseuri" in + let baseuri = GrafiteTypes.get_string_option grafite_status "baseuri" in let basedir = Helm_registry.get "matita.basedir" in LibraryClean.clean_baseuris ~basedir [baseuri] with GrafiteTypes.Option_error _ -> () -let ask_and_save_moo_if_needed parent fname status = +let ask_and_save_moo_if_needed parent fname lexicon_status grafite_status = let basedir = Helm_registry.get "matita.basedir" in - let baseuri = GrafiteParserMisc.baseuri_of_script ~include_paths:[] fname in + let baseuri = DependenciesParser.baseuri_of_script ~include_paths:[] fname in let moo_fname = LibraryMisc.obj_file_of_baseuri ~basedir ~baseuri in let save () = - let metadata_fname= LibraryMisc.metadata_file_of_baseuri ~basedir ~baseuri in - GrafiteMarshal.save_moo moo_fname status.GrafiteTypes.moo_content_rev; - LibraryNoDb.save_metadata metadata_fname status.GrafiteTypes.metadata + let metadata_fname = + LibraryMisc.metadata_file_of_baseuri ~basedir ~baseuri in + let lexicon_fname = + LibraryMisc.lexicon_file_of_baseuri ~basedir ~baseuri + in + GrafiteMarshal.save_moo moo_fname + grafite_status.GrafiteTypes.moo_content_rev; + LibraryNoDb.save_metadata metadata_fname + lexicon_status.LexiconEngine.metadata; + LexiconMarshal.save_lexicon lexicon_fname + lexicon_status.LexiconEngine.lexicon_content_rev in if (MatitaScript.current ())#eos && - status.GrafiteTypes.proof_status = GrafiteTypes.No_proof + grafite_status.GrafiteTypes.proof_status = GrafiteTypes.No_proof then begin let rc = @@ -98,10 +108,10 @@ let ask_and_save_moo_if_needed parent fname status = if b then save () else - clean_current_baseuri status + clean_current_baseuri grafite_status end else - clean_current_baseuri status + clean_current_baseuri grafite_status let ask_unsaved parent = MatitaGtkMisc.ask_confirmation @@ -110,6 +120,16 @@ let ask_unsaved parent = "Do you want to save the script before continuing?") () +(** Selection handling + * Two clipboards are used: "clipboard" and "primary". + * "primary" is used by X, when you hit the middle button mouse is content is + * pasted between applications. In Matita this selection always contain the + * textual version of the selected term. + * "clipboard" is used inside Matita only and support ATM two different targets: + * "TERM" and "PATTERN", in the future other targets like "MATHMLCONTENT" may + * be added + *) + class gui () = (* creation order _is_ relevant for windows placement *) let main = new mainWin () in @@ -143,6 +163,8 @@ class gui () = val mutable font_size = default_font_size val mutable next_devel_must_contain = None val mutable next_ligatures = [] + val clipboard = GData.clipboard Gdk.Atom.clipboard + val primary = GData.clipboard Gdk.Atom.primary initializer (* glade's check widgets *) @@ -310,8 +332,32 @@ class gui () = let undoMenuItem, redoMenuItem = match menuItems with [undo;redo;sep1;cut;copy;paste;delete;sep2; - selectall;sep3;inputmethod;insertunicodecharacter] -> undo,redo + selectall;sep3;inputmethod;insertunicodecharacter] -> + List.iter menu#remove [ copy; cut; delete; paste ]; + undo,redo | _ -> assert false in + let add_menu_item = + let i = ref 2 in (* last occupied position *) + fun ?label ?stock () -> + incr i; + GMenu.image_menu_item ?label ?stock ~packing:(menu#insert ~pos:!i) + () + in + let copy = add_menu_item ~stock:`COPY () in + let cut = add_menu_item ~stock:`CUT () in + let delete = add_menu_item ~stock:`DELETE () in + let paste = add_menu_item ~stock:`PASTE () in + let paste_pattern = add_menu_item ~label:"Paste as pattern" () in + copy#misc#set_sensitive self#canCopy; + cut#misc#set_sensitive self#canCut; + delete#misc#set_sensitive self#canDelete; + paste#misc#set_sensitive self#canPaste; + paste_pattern#misc#set_sensitive self#canPastePattern; + connect_menu_item copy self#copy; + connect_menu_item cut self#cut; + connect_menu_item delete self#delete; + connect_menu_item paste self#paste; + connect_menu_item paste_pattern self#pastePattern; let new_undoMenuItem = GMenu.image_menu_item ~image:(GMisc.image ~stock:`UNDO ()) @@ -332,35 +378,18 @@ class gui () = (redoMenuItem#misc#get_flag `SENSITIVE); menu#remove (redoMenuItem :> GMenu.menu_item); 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.current ())#clean_dirty_lock); - connect_menu_item main#deleteMenuItem (fun () -> - ignore (source_view#buffer#delete_selection ())); + main#copyMenuItem#misc#set_sensitive self#canCopy; + main#cutMenuItem#misc#set_sensitive self#canCut; + main#deleteMenuItem#misc#set_sensitive self#canDelete; + main#pasteMenuItem#misc#set_sensitive self#canPaste; + main#pastePatternMenuItem#misc#set_sensitive self#canPastePattern); + connect_menu_item main#copyMenuItem self#copy; + connect_menu_item main#cutMenuItem self#cut; + connect_menu_item main#deleteMenuItem self#delete; + connect_menu_item main#pasteMenuItem self#paste; + connect_menu_item main#pastePatternMenuItem self#pastePattern; 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); @@ -525,18 +554,22 @@ class gui () = (* toolbar *) let module A = GrafiteAst in let hole = CicNotationPt.UserInput in - let loc = DisambiguateTypes.dummy_floc in + let loc = HExtlib.dummy_floc in let tac ast _ = if (MatitaScript.current ())#onGoingProof () then (MatitaScript.current ())#advance - ~statement:("\n" ^ GrafiteAstPp.pp_tactical (A.Tactic (loc, ast))) + ~statement:("\n" + ^ GrafiteAstPp.pp_tactical ~term_pp:CicNotationPp.pp_term + ~lazy_term_pp:CicNotationPp.pp_term (A.Tactic (loc, ast))) () in let tac_w_term ast _ = if (MatitaScript.current ())#onGoingProof () then let buf = source_buffer in buf#insert ~iter:(buf#get_iter_at_mark (`NAME "locked")) - ("\n" ^ GrafiteAstPp.pp_tactic ast) + ("\n" + ^ GrafiteAstPp.pp_tactic ~term_pp:CicNotationPp.pp_term + ~lazy_term_pp:CicNotationPp.pp_term ast) in let tbar = main in connect_button tbar#introsButton (tac (A.Intros (loc, None, []))); @@ -641,7 +674,8 @@ class gui () = console#message ("'"^f^"' saved.\n"); in let abandon_script () = - let status = (s ())#status in + let lexicon_status = (s ())#lexicon_status in + let grafite_status = (s ())#grafite_status in if source_view#buffer#modified then (match ask_unsaved main#toplevel with | `YES -> saveScript () @@ -649,7 +683,9 @@ class gui () = | `CANCEL -> raise MatitaTypes.Cancel); (match script_fname with | None -> () - | Some fname -> ask_and_save_moo_if_needed main#toplevel fname status); + | Some fname -> + ask_and_save_moo_if_needed main#toplevel fname + lexicon_status grafite_status); in let loadScript () = let script = s () in @@ -697,7 +733,8 @@ class gui () = in (* quit *) self#setQuitCallback (fun () -> - let status = (MatitaScript.current ())#status in + let lexicon_status = (MatitaScript.current ())#lexicon_status in + let grafite_status = (MatitaScript.current ())#grafite_status in if source_view#buffer#modified then begin let rc = ask_unsaved main#toplevel in @@ -709,8 +746,8 @@ class gui () = (match script_fname with | None -> () | Some fname -> - ask_and_save_moo_if_needed - main#toplevel fname status); + ask_and_save_moo_if_needed main#toplevel + fname lexicon_status grafite_status); GMain.Main.quit () end | `NO -> GMain.Main.quit () @@ -720,10 +757,11 @@ class gui () = else begin (match script_fname with - | None -> clean_current_baseuri status; GMain.Main.quit () + | None -> clean_current_baseuri grafite_status; GMain.Main.quit () | Some fname -> try - ask_and_save_moo_if_needed main#toplevel fname status; + ask_and_save_moo_if_needed main#toplevel fname lexicon_status + grafite_status; GMain.Main.quit () with MatitaTypes.Cancel -> ()) end); @@ -801,6 +839,42 @@ class gui () = MatitaMathView.reset_font_size (); MatitaMathView.update_font_sizes ()); MatitaMathView.reset_font_size (); + + (** selections / clipboards handling *) + + method markupSelected = MatitaMathView.has_selection () + method private textSelected = + (source_buffer#get_iter_at_mark `INSERT)#compare + (source_buffer#get_iter_at_mark `SEL_BOUND) <> 0 + method private somethingSelected = self#markupSelected || self#textSelected + method private markupStored = MatitaMathView.has_clipboard () + method private textStored = clipboard#text <> None + method private somethingStored = self#markupStored || self#textStored + + method canCopy = self#somethingSelected + method canCut = self#textSelected + method canDelete = self#textSelected + method canPaste = self#somethingStored + method canPastePattern = self#markupStored + + method copy () = + if self#textSelected + then begin + MatitaMathView.empty_clipboard (); + source_view#buffer#copy_clipboard clipboard; + end else + MatitaMathView.copy_selection () + method cut () = + source_view#buffer#cut_clipboard clipboard; + MatitaMathView.empty_clipboard () + method delete () = ignore (source_view#buffer#delete_selection ()) + method paste () = + if MatitaMathView.has_clipboard () + then source_view#buffer#insert (MatitaMathView.paste_clipboard `Term) + else source_view#buffer#paste_clipboard clipboard; + (MatitaScript.current ())#clean_dirty_lock + method pastePattern () = + source_view#buffer#insert (MatitaMathView.paste_clipboard `Pattern) method private nextLigature () = let iter = source_buffer#get_iter_at_mark `INSERT in @@ -1201,8 +1275,8 @@ let interactive_interp_choice () choices = let _ = (* disambiguator callbacks *) - MatitaDisambiguator.set_choose_uris_callback (interactive_uri_choice ()); - MatitaDisambiguator.set_choose_interp_callback (interactive_interp_choice ()); + GrafiteDisambiguator.set_choose_uris_callback (interactive_uri_choice ()); + GrafiteDisambiguator.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;