X-Git-Url: https://pintos-os.org/cgi-bin/gitweb.cgi?a=blobdiff_plain;f=src%2Fui%2Fgui%2Fsyntax-editor.ui;h=6c7adc9110049698cc2b0ca946329c56eda6daff;hb=42993d3ae61750a8f1e291297d8ac91465afcff2;hp=91fdec4946b7049b398b4a35bfe4e8a49c0591c0;hpb=770a9763c4059adc0fde5f7b169814181ac14158;p=pspp

diff --git a/src/ui/gui/syntax-editor.ui b/src/ui/gui/syntax-editor.ui
index 91fdec4946..6c7adc9110 100644
--- a/src/ui/gui/syntax-editor.ui
+++ b/src/ui/gui/syntax-editor.ui
@@ -48,6 +48,12 @@
             <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>
           <object class="GtkAction" id="file_quit">
             <property name="stock-id">gtk-quit</property>
@@ -88,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>
@@ -144,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">
@@ -151,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"/>
@@ -177,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>
@@ -197,6 +220,5 @@
   </object>
   <object class="GtkStatusbar" id="statusbar2">
     <property name="visible">True</property>
-    <property name="has_resize_grip">True</property>
   </object>
 </interface>