X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2FmatitaScript.ml;h=33296d2320ec2be4487110090af548ba9586d86b;hb=f34f2623a3133e235331d0c0c1830ec213dd09f1;hp=de78194f0254f0592642d8b90ad40c3ccd183fde;hpb=7e6fea0332e132a8cb89c689ba68c5e884c4354c;p=helm.git

diff --git a/matita/matita/matitaScript.ml b/matita/matita/matitaScript.ml
index de78194f0..33296d232 100644
--- a/matita/matita/matitaScript.ml
+++ b/matita/matita/matitaScript.ml
@@ -251,7 +251,7 @@ let fresh_script_id =
  *)
 class script ~(parent:GBin.scrolled_window) ~tab_label () =
 let source_view =
-  GSourceView2.source_view
+  GSourceView3.source_view
     ~auto_indent:true
     ~insert_spaces_instead_of_tabs:true ~tab_width:2
     ~right_margin_position:80 ~show_right_margin:true
@@ -260,6 +260,12 @@ let source_view =
     () in
 let buffer = source_view#buffer in
 let source_buffer = source_view#source_buffer in
+let _ =
+ source_buffer#connect#notify_can_undo
+  ~callback:(MatitaMisc.get_gui ())#main#undoMenuItem#misc#set_sensitive in
+let _ =
+ source_buffer#connect#notify_can_redo
+  ~callback:(MatitaMisc.get_gui ())#main#redoMenuItem#misc#set_sensitive in
 let similarsymbols_tag_name = "similarsymbolos" in
 let similarsymbols_tag = `NAME similarsymbols_tag_name in
 let initial_statuses current baseuri =
@@ -376,16 +382,14 @@ object (self)
          | _ -> assert false in
        let add_menu_item =
          let i = ref 2 in (* last occupied position *)
-         fun ?label ?stock () ->
+         fun ~label ->
            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
+           GMenu.menu_item ~label ~packing:(menu#insert ~pos:!i) () in
+       let copy = add_menu_item ~label:"Copy" in
+       let cut = add_menu_item ~label:"Cut" in
+       let delete = add_menu_item ~label:"Delete" in
+       let paste = add_menu_item ~label:"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;
@@ -397,24 +401,22 @@ object (self)
        MatitaGtkMisc.connect_menu_item paste self#paste;
        MatitaGtkMisc.connect_menu_item paste_pattern self#pastePattern;
        let new_undoMenuItem =
-        GMenu.image_menu_item
-         ~image:(GMisc.image ~stock:`UNDO ())
+        GMenu.menu_item
          ~use_mnemonic:true
          ~label:"_Undo"
          ~packing:(menu#insert ~pos:0) () in
        new_undoMenuItem#misc#set_sensitive
-        (undoMenuItem#misc#get_flag `SENSITIVE);
+        undoMenuItem#misc#sensitive;
        menu#remove (undoMenuItem :> GMenu.menu_item);
        MatitaGtkMisc.connect_menu_item new_undoMenuItem
         (fun () -> self#safe_undo);
        let new_redoMenuItem =
-        GMenu.image_menu_item
-         ~image:(GMisc.image ~stock:`REDO ())
+        GMenu.menu_item
          ~use_mnemonic:true
          ~label:"_Redo"
          ~packing:(menu#insert ~pos:1) () in
        new_redoMenuItem#misc#set_sensitive
-        (redoMenuItem#misc#get_flag `SENSITIVE);
+        redoMenuItem#misc#sensitive;
         menu#remove (redoMenuItem :> GMenu.menu_item);
         MatitaGtkMisc.connect_menu_item new_redoMenuItem
          (fun () -> self#safe_redo)));