X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaGui.ml;h=16712c4541b77047970d8530b69c165427021340;hb=78229b5b53f947df657547e682c5365bbba9455b;hp=74913dbe6d46c596cc73ecb640e93ac218c27e28;hpb=3ce38077e0b1e2a38ad513d3c108d7ef3c09bb7c;p=helm.git

diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml
index 74913dbe6..16712c454 100644
--- a/helm/matita/matitaGui.ml
+++ b/helm/matita/matitaGui.ml
@@ -70,9 +70,10 @@ 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
-    let metadata_fname = GrafiteMisc.metadata_file_of_script ~basedir fname 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
@@ -80,13 +81,12 @@ let ask_and_save_moo_if_needed parent fname status =
      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 = 
@@ -96,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
@@ -110,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
@@ -143,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 *)
@@ -310,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 ())
@@ -332,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);
@@ -529,14 +548,18 @@ class gui () =
       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, [])));
@@ -801,6 +824,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