X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaGui.ml;h=5aa3d59e9c69edb491a4bd3c0189d33d16cf6489;hb=6a149d262dfcb03a7d57f8ecabf23b0b59e99f85;hp=6b4afa3cf3e549f9f484ed54c71d14504750965e;hpb=ebe70c001a623e0440f21cd16dc88f585edcf0ea;p=helm.git

diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml
index 6b4afa3cf..5aa3d59e9 100644
--- a/helm/matita/matitaGui.ml
+++ b/helm/matita/matitaGui.ml
@@ -70,21 +70,23 @@ let clean_current_baseuri status =
 
 let ask_and_save_moo_if_needed parent fname status = 
   let basedir = Helm_registry.get "matita.basedir" in
+  let baseuri = GrafiteParserMisc.baseuri_of_script ~include_paths:[] fname in
+  let moo_fname = LibraryMisc.obj_file_of_baseuri ~basedir ~baseuri in
   let save () =
-    let moo_fname = GrafiteMisc.obj_file_of_script ~basedir fname in
-     GrafiteMarshal.save_moo moo_fname
-      status.GrafiteTypes.moo_content_rev in
+    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
+  in
   if (MatitaScript.current ())#eos &&
      status.GrafiteTypes.proof_status = GrafiteTypes.No_proof
   then
     begin
-      let mooname = GrafiteMisc.obj_file_of_script ~basedir fname in
       let rc = 
         MatitaGtkMisc.ask_confirmation
         ~title:"A .moo can be generated"
         ~message:(Printf.sprintf 
           "%s can be generated for %s.\n<i>Should I generate it?</i>"
-          (Filename.basename mooname) (Filename.basename fname))
+          (Filename.basename moo_fname) (Filename.basename fname))
         ~parent ()
       in
       let b = 
@@ -94,7 +96,7 @@ let ask_and_save_moo_if_needed parent fname status =
         | `CANCEL -> raise MatitaTypes.Cancel 
       in
       if b then
-        save ()
+          save ()
       else
         clean_current_baseuri status
     end
@@ -108,6 +110,16 @@ let ask_unsaved parent =
          "<i>Do you want to save the script before continuing?</i>")
     ()
 
+(** 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
@@ -141,6 +153,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 *)
@@ -308,8 +322,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 ())
@@ -330,35 +368,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);
@@ -799,6 +820,43 @@ class gui () =
         MatitaMathView.reset_font_size ();
         MatitaMathView.update_font_sizes ());
       MatitaMathView.reset_font_size ();
+
+      (** selections / clipboards handling *)
+
+    method private markup_selected = MatitaMathView.has_selection ()
+    method private text_selected =
+      (source_buffer#get_iter_at_mark `INSERT)#compare
+        (source_buffer#get_iter_at_mark `SEL_BOUND) <> 0
+    method private something_selected =
+      self#markup_selected || self#text_selected
+    method private markup_stored = MatitaMathView.has_clipboard ()
+    method private text_stored = clipboard#text <> None
+    method private something_stored = self#markup_stored || self#text_stored
+
+    method canCopy = self#something_selected
+    method canCut = self#text_selected
+    method canDelete = self#text_selected
+    method canPaste = self#something_stored
+    method canPastePattern = self#markup_stored
+
+    method copy () =
+      if self#text_selected
+      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