integrated lablgtksourceview

[helm.git] / helm / matita / matita.glade

diff --git a/helm/matita/matita.glade b/helm/matita/matita.glade
index bea43910b80469455c525ff33e6796a493562793..d1a39dd9d38c10a65d400159df174a7480109005 100644 (file)
--- a/helm/matita/matita.glade
+++ b/helm/matita/matita.glade
@@ -1906,7 +1906,7 @@ Copyright (C) 2005,
                              <property name="enable_popup">False</property>
 
                              <child>
-                               <widget class="GtkScrolledWindow" id="scrolledwindow7">
+                               <widget class="GtkScrolledWindow" id="ScriptScrolledWin">
                                  <property name="visible">True</property>
                                  <property name="can_focus">True</property>
                                  <property name="hscrollbar_policy">GTK_POLICY_AUTOMATIC</property>
@@ -1915,24 +1915,7 @@ Copyright (C) 2005,
                                  <property name="window_placement">GTK_CORNER_TOP_LEFT</property>
 
                                  <child>
-                                   <widget class="GtkTextView" id="scriptTextView">
-                                     <property name="border_width">2</property>
-                                     <property name="visible">True</property>
-                                     <property name="can_focus">True</property>
-                                     <property name="editable">True</property>
-                                     <property name="overwrite">False</property>
-                                     <property name="accepts_tab">True</property>
-                                     <property name="justification">GTK_JUSTIFY_LEFT</property>
-                                     <property name="wrap_mode">GTK_WRAP_NONE</property>
-                                     <property name="cursor_visible">True</property>
-                                     <property name="pixels_above_lines">0</property>
-                                     <property name="pixels_below_lines">0</property>
-                                     <property name="pixels_inside_wrap">0</property>
-                                     <property name="left_margin">2</property>
-                                     <property name="right_margin">0</property>
-                                     <property name="indent">0</property>
-                                     <property name="text" translatable="yes"></property>
-                                   </widget>
+                                   <placeholder/>
                                  </child>
                                </widget>
                                <packing>