X-Git-Url: https://pintos-os.org/cgi-bin/gitweb.cgi?a=blobdiff_plain;f=src%2Fui%2Fgui%2Fsyntax-editor.ui;h=51e589ec730c048cbd2a72799fc8c4800dff0f1c;hb=b0fd056eedc6872d45541c1ee0eb43e909bbc8b1;hp=e65eef66ccd85067d336b121d6d034ca12db7992;hpb=df8e125c0969d3b6e043b7069d52f069c9e7ee78;p=pspp

diff --git a/src/ui/gui/syntax-editor.ui b/src/ui/gui/syntax-editor.ui
index e65eef66cc..51e589ec73 100644
--- a/src/ui/gui/syntax-editor.ui
+++ b/src/ui/gui/syntax-editor.ui
@@ -32,6 +32,7 @@
           <object class="GtkAction" id="file_open">
             <property name="stock-id">gtk-open</property>
             <property name="name">file_open</property>
+            <property name="label" translatable="yes">_Open...</property>
           </object>
         </child>
         <child>
@@ -44,6 +45,13 @@
           <object class="GtkAction" id="file_save_as">
             <property name="stock-id">gtk-save-as</property>
             <property name="name">file_save_as</property>
+            <property name="label" translatable="yes">Save _As...</property>
+          </object>
+        </child>
+        <child>
+          <object class="GtkAction" id="file_print">
+            <property name="name">file_print</property>
+            <property name="stock-id">gtk-print</property>
           </object>
         </child>
         <child>
@@ -86,6 +94,18 @@
             <property name="sensitive">false</property>
           </object>
         </child>
+        <child>
+          <object class="GtkAction" id="edit_undo">
+            <property name="stock-id">gtk-undo</property>
+            <property name="name">edit_undo</property>
+          </object>
+        </child>
+        <child>
+          <object class="GtkAction" id="edit_redo">
+            <property name="stock-id">gtk-redo</property>
+            <property name="name">edit_redo</property>
+          </object>
+        </child>
         <child>
           <object class="GtkAction" id="run1">
             <property name="name">run1</property>
@@ -142,6 +162,8 @@
           <menuitem action="file_save"/>
           <menuitem action="file_save_as"/>
           <separator/>
+          <menuitem action="file_print"/>
+          <separator/>
           <menuitem action="file_quit"/>
         </menu>
         <menu action="menuitem7">
@@ -149,6 +171,9 @@
           <menuitem action="edit_copy"/>
           <menuitem action="edit_paste"/>
           <menuitem action="edit_delete"/>
+          <separator/>
+          <menuitem action="edit_undo"/>
+          <menuitem action="edit_redo"/>
         </menu>
         <menu action="run1">
           <menuitem action="run_all"/>
@@ -175,7 +200,7 @@
     <property name="shadow_type">GTK_SHADOW_IN</property>
     <property name="window_placement">GTK_CORNER_TOP_LEFT</property>
     <child>
-      <object class="GtkTextView" id="syntax_text_view">
+      <object class="GtkSourceView" id="syntax_text_view">
         <property name="visible">True</property>
         <property name="can_focus">True</property>
         <property name="editable">True</property>