X-Git-Url: https://pintos-os.org/cgi-bin/gitweb.cgi?a=blobdiff_plain;f=src%2Fui%2Fgui%2Fsyntax-editor.ui;fp=src%2Fui%2Fgui%2Fsyntax-editor.ui;h=4f134c2e1cb51b966674a5c0dc764941b7a5b93e;hb=ca5f6bb9df6d4019d777b52da0419d917d4dfc52;hp=c9436629e58779d6922bf4e795afbd35d675ca30;hpb=f5c20c9555754967be55d063f450db23557478cc;p=pspp

diff --git a/src/ui/gui/syntax-editor.ui b/src/ui/gui/syntax-editor.ui
index c9436629e5..4f134c2e1c 100644
--- a/src/ui/gui/syntax-editor.ui
+++ b/src/ui/gui/syntax-editor.ui
@@ -58,6 +58,12 @@
             <property name="name">file_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>
@@ -98,6 +104,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>
@@ -157,6 +175,8 @@
           <menuitem action="file_save"/>
           <menuitem action="file_save_as"/>
           <separator/>
+          <menuitem action="file_print"/>
+          <separator/>
           <menuitem action="file_quit"/>
         </menu>
         <menu action="menuitem7">
@@ -164,6 +184,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"/>
@@ -190,7 +213,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>