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

diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml
index 3ea6b4f87..5aa3d59e9 100644
--- a/helm/matita/matitaGui.ml
+++ b/helm/matita/matitaGui.ml
@@ -53,7 +53,7 @@ class console ~(buffer: GText.buffer) () =
     method debug s   = buffer#insert ~iter:buffer#end_iter ~tags:[debug_tag] s
     method clear () =
       buffer#delete ~start:buffer#start_iter ~stop:buffer#end_iter
-    method log_callback (tag: MatitaLog.log_tag) s =
+    method log_callback (tag: HLog.log_tag) s =
       match tag with
       | `Debug -> self#debug (s ^ "\n")
       | `Error -> self#error (s ^ "\n")
@@ -63,27 +63,30 @@ class console ~(buffer: GText.buffer) () =
         
 let clean_current_baseuri status = 
     try  
-      let baseuri = MatitaTypes.get_string_option status "baseuri" in
-      MatitacleanLib.clean_baseuris [baseuri]
-    with MatitaTypes.Option_error _ -> ()
+      let baseuri = GrafiteTypes.get_string_option 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 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 = MatitacleanLib.obj_file_of_script fname in
-    MatitaMoo.save_moo moo_fname status.MatitaTypes.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.MatitaTypes.proof_status = MatitaTypes.No_proof
+     status.GrafiteTypes.proof_status = GrafiteTypes.No_proof
   then
     begin
-      let mooname = 
-        MatitacleanLib.obj_file_of_script 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 = 
@@ -93,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
@@ -107,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
@@ -140,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 *)
@@ -307,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 ())
@@ -329,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);
@@ -471,7 +493,7 @@ class gui () =
               newDevel#toplevel#misc#hide()
             end
           else
-            MatitaLog.error ("The selected root does not contain " ^ 
+            HLog.error ("The selected root does not contain " ^ 
               match next_devel_must_contain with 
               | Some x -> x 
               | _ -> assert false));
@@ -569,7 +591,7 @@ class gui () =
         ~check:main#fullscreenMenuItem;
       main#fullscreenMenuItem#set_active false;
         (* log *)
-      MatitaLog.set_log_callback self#console#log_callback;
+      HLog.set_log_callback self#console#log_callback;
       GtkSignal.user_handler :=
         (fun exn ->
           if not (Helm_registry.get_bool "matita.debug") then
@@ -601,14 +623,14 @@ class gui () =
                  source_buffer#place_cursor
                   (source_buffer#get_iter (`OFFSET x'));
             end;
-            MatitaLog.error msg
+            HLog.error msg
           else raise exn);
         (* script *)
       ignore (source_buffer#connect#mark_set (fun _ _ -> next_ligatures <- []));
       let _ =
         match GSourceView.source_language_from_file BuildTimeConf.lang_file with
         | None ->
-            MatitaLog.warn (sprintf "can't load language file %s"
+            HLog.warn (sprintf "can't load language file %s"
               BuildTimeConf.lang_file)
         | Some matita_lang ->
             source_buffer#set_language matita_lang;
@@ -798,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