- handles about:* uris in cicBrowser

- added comboboxentry in cicBrowser (still ugly ...)

diff --git a/helm/matita/.depend b/helm/matita/.depend
index 618c446299c16355a1ea4c597313a4bc1a5ec78d..95217b4b60350021c133da65c5e6c8265a398e7f 100644 (file)
--- a/helm/matita/.depend
+++ b/helm/matita/.depend
@@ -33,9 +33,9 @@ matita.cmx: matitaTypes.cmx matitaScript.cmx matitaMisc.cmx \
     matitaMathView.cmx matitaLog.cmx matitaGui.cmx matitaGtkMisc.cmx \
     matitaEngine.cmx matitaDisambiguator.cmx matitaDb.cmx buildTimeConf.cmx 
 matitaScript.cmo: matitaTypes.cmo matitaSync.cmi matitaMisc.cmi matitaLog.cmi \
-    matitaEngine.cmi matitaScript.cmi 
+    matitaEngine.cmi matitaDisambiguator.cmi matitaDb.cmi matitaScript.cmi 
 matitaScript.cmx: matitaTypes.cmx matitaSync.cmx matitaMisc.cmx matitaLog.cmx \
-    matitaEngine.cmx matitaScript.cmi 
+    matitaEngine.cmx matitaDisambiguator.cmx matitaDb.cmx matitaScript.cmi 
 matitaSync.cmo: matitaTypes.cmo matitaMisc.cmi matitaLog.cmi matitaDb.cmi \
     matitaSync.cmi 
 matitaSync.cmx: matitaTypes.cmx matitaMisc.cmx matitaLog.cmx matitaDb.cmx \
@@ -46,6 +46,7 @@ matitaDisambiguator.cmi: matitaTypes.cmo
 matitaEngine.cmi: matitaTypes.cmo 
 matitaGtkMisc.cmi: matitaGeneratedGui.cmi 
 matitaGui.cmi: matitaLog.cmi matitaGeneratedGui.cmi matitaDisambiguator.cmi 
+matitaMathView.cmi: matitaTypes.cmo 
 matitaMisc.cmi: matitaTypes.cmo 
 matitaScript.cmi: matitaTypes.cmo 
 matitaSync.cmi: matitaTypes.cmo 

diff --git a/helm/matita/Makefile.in b/helm/matita/Makefile.in
index 155a36e0875e133b66c1acd2a05ddc44e1ca610f..bbf534b325967ccee89dc0b6ce8abd00d25d4d69 100644 (file)
--- a/helm/matita/Makefile.in
+++ b/helm/matita/Makefile.in
@@ -103,7 +103,7 @@ TAGS:
        cd ..; otags -vi -r ocaml/ matita/
 
 #.depend: matitaGeneratedGui.ml matitaGeneratedGui.mli *.ml *.mli
-.depend:
+depend:
        $(OCAMLDEP) *.ml *.mli > .depend
 
 include .depend

diff --git a/helm/matita/matita.glade b/helm/matita/matita.glade
index 4b82c9339a696b95e30244d2a97c28603804d2a8..690e17749e63e91cc6ae835bff211f74ed2afe39 100644 (file)
--- a/helm/matita/matita.glade
+++ b/helm/matita/matita.glade
@@ -110,332 +110,278 @@ Copyright (C) 2005,
            <widget class="GtkFrame" id="frame2">
              <property name="visible">True</property>
              <property name="label_xalign">0</property>
-             <property name="label_yalign">0.5</property>
-             <property name="shadow_type">GTK_SHADOW_OUT</property>
+             <property name="label_yalign">0</property>
+             <property name="shadow_type">GTK_SHADOW_NONE</property>
 
              <child>
-               <widget class="GtkAlignment" id="alignment3">
+               <widget class="GtkHBox" id="BrowserHBox">
                  <property name="visible">True</property>
-                 <property name="xalign">0.5</property>
-                 <property name="yalign">0.5</property>
-                 <property name="xscale">1</property>
-                 <property name="yscale">1</property>
-                 <property name="top_padding">0</property>
-                 <property name="bottom_padding">0</property>
-                 <property name="left_padding">0</property>
-                 <property name="right_padding">0</property>
+                 <property name="homogeneous">False</property>
+                 <property name="spacing">0</property>
 
                  <child>
-                   <widget class="GtkHBox" id="hbox11">
+                   <widget class="GtkButton" id="BrowserNewButton">
                      <property name="visible">True</property>
-                     <property name="homogeneous">False</property>
-                     <property name="spacing">0</property>
+                     <property name="tooltip" translatable="yes">new browser win</property>
+                     <property name="can_default">True</property>
+                     <property name="can_focus">True</property>
+                     <property name="relief">GTK_RELIEF_NONE</property>
+                     <property name="focus_on_click">False</property>
 
                      <child>
-                       <widget class="GtkButton" id="BrowserNewButton">
+                       <widget class="GtkImage" id="image191">
                          <property name="visible">True</property>
-                         <property name="tooltip" translatable="yes">new browser win</property>
-                         <property name="can_default">True</property>
-                         <property name="can_focus">True</property>
-                         <property name="relief">GTK_RELIEF_NONE</property>
-                         <property name="focus_on_click">False</property>
-
-                         <child>
-                           <widget class="GtkImage" id="image191">
-                             <property name="visible">True</property>
-                             <property name="stock">gtk-new</property>
-                             <property name="icon_size">4</property>
-                             <property name="xalign">0.5</property>
-                             <property name="yalign">0.5</property>
-                             <property name="xpad">0</property>
-                             <property name="ypad">0</property>
-                           </widget>
-                         </child>
+                         <property name="stock">gtk-new</property>
+                         <property name="icon_size">4</property>
+                         <property name="xalign">0.5</property>
+                         <property name="yalign">0.5</property>
+                         <property name="xpad">0</property>
+                         <property name="ypad">0</property>
                        </widget>
-                       <packing>
-                         <property name="padding">0</property>
-                         <property name="expand">False</property>
-                         <property name="fill">False</property>
-                       </packing>
                      </child>
+                   </widget>
+                   <packing>
+                     <property name="padding">0</property>
+                     <property name="expand">False</property>
+                     <property name="fill">False</property>
+                   </packing>
+                 </child>
+
+                 <child>
+                   <widget class="GtkButton" id="BrowserBackButton">
+                     <property name="visible">True</property>
+                     <property name="tooltip" translatable="yes">history back</property>
+                     <property name="can_default">True</property>
+                     <property name="can_focus">True</property>
+                     <property name="relief">GTK_RELIEF_NONE</property>
+                     <property name="focus_on_click">True</property>
 
                      <child>
-                       <widget class="GtkButton" id="BrowserBackButton">
+                       <widget class="GtkAlignment" id="alignment3">
                          <property name="visible">True</property>
-                         <property name="tooltip" translatable="yes">history back</property>
-                         <property name="can_default">True</property>
-                         <property name="can_focus">True</property>
-                         <property name="relief">GTK_RELIEF_NONE</property>
-                         <property name="focus_on_click">True</property>
+                         <property name="xalign">0.5</property>
+                         <property name="yalign">0.5</property>
+                         <property name="xscale">0</property>
+                         <property name="yscale">0</property>
+                         <property name="top_padding">0</property>
+                         <property name="bottom_padding">0</property>
+                         <property name="left_padding">0</property>
+                         <property name="right_padding">0</property>
 
                          <child>
-                           <widget class="GtkAlignment" id="alignment3">
+                           <widget class="GtkHBox" id="hbox6">
                              <property name="visible">True</property>
-                             <property name="xalign">0.5</property>
-                             <property name="yalign">0.5</property>
-                             <property name="xscale">0</property>
-                             <property name="yscale">0</property>
-                             <property name="top_padding">0</property>
-                             <property name="bottom_padding">0</property>
-                             <property name="left_padding">0</property>
-                             <property name="right_padding">0</property>
+                             <property name="homogeneous">False</property>
+                             <property name="spacing">2</property>
 
                              <child>
-                               <widget class="GtkHBox" id="hbox6">
+                               <widget class="GtkImage" id="image188">
                                  <property name="visible">True</property>
-                                 <property name="homogeneous">False</property>
-                                 <property name="spacing">2</property>
-
-                                 <child>
-                                   <widget class="GtkImage" id="image188">
-                                     <property name="visible">True</property>
-                                     <property name="stock">gtk-go-back</property>
-                                     <property name="icon_size">4</property>
-                                     <property name="xalign">0.5</property>
-                                     <property name="yalign">0.5</property>
-                                     <property name="xpad">0</property>
-                                     <property name="ypad">0</property>
-                                   </widget>
-                                   <packing>
-                                     <property name="padding">0</property>
-                                     <property name="expand">False</property>
-                                     <property name="fill">False</property>
-                                   </packing>
-                                 </child>
+                                 <property name="stock">gtk-go-back</property>
+                                 <property name="icon_size">4</property>
+                                 <property name="xalign">0.5</property>
+                                 <property name="yalign">0.5</property>
+                                 <property name="xpad">0</property>
+                                 <property name="ypad">0</property>
+                               </widget>
+                               <packing>
+                                 <property name="padding">0</property>
+                                 <property name="expand">False</property>
+                                 <property name="fill">False</property>
+                               </packing>
+                             </child>
 
-                                 <child>
-                                   <widget class="GtkLabel" id="label10">
-                                     <property name="visible">True</property>
-                                     <property name="label" translatable="yes"></property>
-                                     <property name="use_underline">True</property>
-                                     <property name="use_markup">False</property>
-                                     <property name="justify">GTK_JUSTIFY_LEFT</property>
-                                     <property name="wrap">False</property>
-                                     <property name="selectable">False</property>
-                                     <property name="xalign">0.5</property>
-                                     <property name="yalign">0.5</property>
-                                     <property name="xpad">0</property>
-                                     <property name="ypad">0</property>
-                                   </widget>
-                                   <packing>
-                                     <property name="padding">0</property>
-                                     <property name="expand">False</property>
-                                     <property name="fill">False</property>
-                                   </packing>
-                                 </child>
+                             <child>
+                               <widget class="GtkLabel" id="label10">
+                                 <property name="visible">True</property>
+                                 <property name="label" translatable="yes"></property>
+                                 <property name="use_underline">True</property>
+                                 <property name="use_markup">False</property>
+                                 <property name="justify">GTK_JUSTIFY_LEFT</property>
+                                 <property name="wrap">False</property>
+                                 <property name="selectable">False</property>
+                                 <property name="xalign">0.5</property>
+                                 <property name="yalign">0.5</property>
+                                 <property name="xpad">0</property>
+                                 <property name="ypad">0</property>
                                </widget>
+                               <packing>
+                                 <property name="padding">0</property>
+                                 <property name="expand">False</property>
+                                 <property name="fill">False</property>
+                               </packing>
                              </child>
                            </widget>
                          </child>
                        </widget>
-                       <packing>
-                         <property name="padding">0</property>
-                         <property name="expand">False</property>
-                         <property name="fill">False</property>
-                       </packing>
                      </child>
+                   </widget>
+                   <packing>
+                     <property name="padding">0</property>
+                     <property name="expand">False</property>
+                     <property name="fill">False</property>
+                   </packing>
+                 </child>
 
-                     <child>
-                       <widget class="GtkButton" id="BrowserForwardButton">
-                         <property name="visible">True</property>
-                         <property name="tooltip" translatable="yes">history forward</property>
-                         <property name="can_default">True</property>
-                         <property name="can_focus">True</property>
-                         <property name="relief">GTK_RELIEF_NONE</property>
-                         <property name="focus_on_click">True</property>
-
-                         <child>
-                           <widget class="GtkImage" id="image189">
-                             <property name="visible">True</property>
-                             <property name="stock">gtk-go-forward</property>
-                             <property name="icon_size">4</property>
-                             <property name="xalign">0.5</property>
-                             <property name="yalign">0.5</property>
-                             <property name="xpad">0</property>
-                             <property name="ypad">0</property>
-                           </widget>
-                         </child>
-                       </widget>
-                       <packing>
-                         <property name="padding">0</property>
-                         <property name="expand">False</property>
-                         <property name="fill">False</property>
-                       </packing>
-                     </child>
+                 <child>
+                   <widget class="GtkButton" id="BrowserForwardButton">
+                     <property name="visible">True</property>
+                     <property name="tooltip" translatable="yes">history forward</property>
+                     <property name="can_default">True</property>
+                     <property name="can_focus">True</property>
+                     <property name="relief">GTK_RELIEF_NONE</property>
+                     <property name="focus_on_click">True</property>
 
                      <child>
-                       <widget class="GtkButton" id="BrowserRefreshButton">
+                       <widget class="GtkImage" id="image189">
                          <property name="visible">True</property>
-                         <property name="tooltip" translatable="yes">refresh</property>
-                         <property name="can_default">True</property>
-                         <property name="can_focus">True</property>
-                         <property name="relief">GTK_RELIEF_NONE</property>
-                         <property name="focus_on_click">True</property>
-
-                         <child>
-                           <widget class="GtkImage" id="image229">
-                             <property name="visible">True</property>
-                             <property name="stock">gtk-refresh</property>
-                             <property name="icon_size">4</property>
-                             <property name="xalign">0.5</property>
-                             <property name="yalign">0.5</property>
-                             <property name="xpad">0</property>
-                             <property name="ypad">0</property>
-                           </widget>
-                         </child>
+                         <property name="stock">gtk-go-forward</property>
+                         <property name="icon_size">4</property>
+                         <property name="xalign">0.5</property>
+                         <property name="yalign">0.5</property>
+                         <property name="xpad">0</property>
+                         <property name="ypad">0</property>
                        </widget>
-                       <packing>
-                         <property name="padding">0</property>
-                         <property name="expand">False</property>
-                         <property name="fill">False</property>
-                       </packing>
                      </child>
+                   </widget>
+                   <packing>
+                     <property name="padding">0</property>
+                     <property name="expand">False</property>
+                     <property name="fill">False</property>
+                   </packing>
+                 </child>
 
-                     <child>
-                       <widget class="GtkButton" id="BrowserHomeButton">
-                         <property name="visible">True</property>
-                         <property name="tooltip" translatable="yes">home</property>
-                         <property name="can_default">True</property>
-                         <property name="can_focus">True</property>
-                         <property name="relief">GTK_RELIEF_NONE</property>
-                         <property name="focus_on_click">True</property>
-
-                         <child>
-                           <widget class="GtkImage" id="image190">
-                             <property name="visible">True</property>
-                             <property name="stock">gtk-home</property>
-                             <property name="icon_size">4</property>
-                             <property name="xalign">0.5</property>
-                             <property name="yalign">0.5</property>
-                             <property name="xpad">0</property>
-                             <property name="ypad">0</property>
-                           </widget>
-                         </child>
-                       </widget>
-                       <packing>
-                         <property name="padding">0</property>
-                         <property name="expand">False</property>
-                         <property name="fill">False</property>
-                       </packing>
-                     </child>
+                 <child>
+                   <widget class="GtkButton" id="BrowserRefreshButton">
+                     <property name="visible">True</property>
+                     <property name="tooltip" translatable="yes">refresh</property>
+                     <property name="can_default">True</property>
+                     <property name="can_focus">True</property>
+                     <property name="relief">GTK_RELIEF_NONE</property>
+                     <property name="focus_on_click">True</property>
 
                      <child>
-                       <widget class="GtkImage" id="image301">
+                       <widget class="GtkImage" id="image229">
                          <property name="visible">True</property>
-                         <property name="stock">gtk-jump-to</property>
+                         <property name="stock">gtk-refresh</property>
                          <property name="icon_size">4</property>
                          <property name="xalign">0.5</property>
                          <property name="yalign">0.5</property>
                          <property name="xpad">0</property>
                          <property name="ypad">0</property>
                        </widget>
-                       <packing>
-                         <property name="padding">3</property>
-                         <property name="expand">False</property>
-                         <property name="fill">False</property>
-                       </packing>
-                     </child>
-
-                     <child>
-                       <widget class="GtkEntry" id="BrowserUri">
-                         <property name="visible">True</property>
-                         <property name="tooltip" translatable="yes">cic uri</property>
-                         <property name="can_default">True</property>
-                         <property name="can_focus">True</property>
-                         <property name="has_focus">True</property>
-                         <property name="editable">True</property>
-                         <property name="visibility">True</property>
-                         <property name="max_length">0</property>
-                         <property name="text" translatable="yes"></property>
-                         <property name="has_frame">True</property>
-                         <property name="invisible_char">*</property>
-                         <property name="activates_default">False</property>
-                       </widget>
-                       <packing>
-                         <property name="padding">3</property>
-                         <property name="expand">True</property>
-                         <property name="fill">True</property>
-                       </packing>
                      </child>
+                   </widget>
+                   <packing>
+                     <property name="padding">0</property>
+                     <property name="expand">False</property>
+                     <property name="fill">False</property>
+                   </packing>
+                 </child>
 
-                     <child>
-                       <widget class="GtkVBox" id="vbox14">
-                         <property name="width_request">20</property>
-                         <property name="visible">True</property>
-                         <property name="homogeneous">False</property>
-                         <property name="spacing">0</property>
-
-                         <child>
-                           <placeholder/>
-                         </child>
-
-                         <child>
-                           <placeholder/>
-                         </child>
-                       </widget>
-                       <packing>
-                         <property name="padding">0</property>
-                         <property name="expand">False</property>
-                         <property name="fill">True</property>
-                       </packing>
-                     </child>
+                 <child>
+                   <widget class="GtkButton" id="BrowserHomeButton">
+                     <property name="visible">True</property>
+                     <property name="tooltip" translatable="yes">home</property>
+                     <property name="can_default">True</property>
+                     <property name="can_focus">True</property>
+                     <property name="relief">GTK_RELIEF_NONE</property>
+                     <property name="focus_on_click">True</property>
 
                      <child>
-                       <widget class="GtkImage" id="whelpImage2">
+                       <widget class="GtkImage" id="image190">
                          <property name="visible">True</property>
+                         <property name="stock">gtk-home</property>
+                         <property name="icon_size">4</property>
                          <property name="xalign">0.5</property>
                          <property name="yalign">0.5</property>
                          <property name="xpad">0</property>
                          <property name="ypad">0</property>
                        </widget>
-                       <packing>
-                         <property name="padding">0</property>
-                         <property name="expand">False</property>
-                         <property name="fill">False</property>
-                       </packing>
                      </child>
+                   </widget>
+                   <packing>
+                     <property name="padding">0</property>
+                     <property name="expand">False</property>
+                     <property name="fill">False</property>
+                   </packing>
+                 </child>
+
+                 <child>
+                   <widget class="GtkImage" id="image301">
+                     <property name="visible">True</property>
+                     <property name="stock">gtk-jump-to</property>
+                     <property name="icon_size">4</property>
+                     <property name="xalign">0.5</property>
+                     <property name="yalign">0.5</property>
+                     <property name="xpad">0</property>
+                     <property name="ypad">0</property>
+                   </widget>
+                   <packing>
+                     <property name="padding">3</property>
+                     <property name="expand">False</property>
+                     <property name="fill">False</property>
+                   </packing>
+                 </child>
+
+                 <child>
+                   <placeholder/>
+                 </child>
+
+                 <child>
+                   <widget class="GtkImage" id="whelpImage2">
+                     <property name="visible">True</property>
+                     <property name="xalign">0.5</property>
+                     <property name="yalign">0.5</property>
+                     <property name="xpad">0</property>
+                     <property name="ypad">0</property>
+                   </widget>
+                   <packing>
+                     <property name="padding">0</property>
+                     <property name="expand">False</property>
+                     <property name="fill">False</property>
+                   </packing>
+                 </child>
+
+                 <child>
+                   <widget class="GtkToggleButton" id="whelpBarToggleButton">
+                     <property name="visible">True</property>
+                     <property name="can_focus">True</property>
+                     <property name="relief">GTK_RELIEF_NONE</property>
+                     <property name="focus_on_click">True</property>
+                     <property name="active">False</property>
+                     <property name="inconsistent">False</property>
 
                      <child>
-                       <widget class="GtkToggleButton" id="whelpBarToggleButton">
+                       <widget class="GtkHBox" id="hbox15">
                          <property name="visible">True</property>
-                         <property name="can_focus">True</property>
-                         <property name="relief">GTK_RELIEF_NONE</property>
-                         <property name="focus_on_click">True</property>
-                         <property name="active">False</property>
-                         <property name="inconsistent">False</property>
+                         <property name="homogeneous">False</property>
+                         <property name="spacing">0</property>
 
                          <child>
-                           <widget class="GtkHBox" id="hbox15">
+                           <widget class="GtkArrow" id="arrow1">
                              <property name="visible">True</property>
-                             <property name="homogeneous">False</property>
-                             <property name="spacing">0</property>
-
-                             <child>
-                               <widget class="GtkArrow" id="arrow1">
-                                 <property name="visible">True</property>
-                                 <property name="arrow_type">GTK_ARROW_DOWN</property>
-                                 <property name="shadow_type">GTK_SHADOW_NONE</property>
-                                 <property name="xalign">0.5</property>
-                                 <property name="yalign">0.5</property>
-                                 <property name="xpad">0</property>
-                                 <property name="ypad">0</property>
-                               </widget>
-                               <packing>
-                                 <property name="padding">0</property>
-                                 <property name="expand">True</property>
-                                 <property name="fill">True</property>
-                               </packing>
-                             </child>
+                             <property name="arrow_type">GTK_ARROW_DOWN</property>
+                             <property name="shadow_type">GTK_SHADOW_NONE</property>
+                             <property name="xalign">0.5</property>
+                             <property name="yalign">0.5</property>
+                             <property name="xpad">0</property>
+                             <property name="ypad">0</property>
                            </widget>
+                           <packing>
+                             <property name="padding">0</property>
+                             <property name="expand">True</property>
+                             <property name="fill">True</property>
+                           </packing>
                          </child>
                        </widget>
-                       <packing>
-                         <property name="padding">0</property>
-                         <property name="expand">False</property>
-                         <property name="fill">False</property>
-                       </packing>
                      </child>
                    </widget>
+                   <packing>
+                     <property name="padding">0</property>
+                     <property name="expand">False</property>
+                     <property name="fill">False</property>
+                   </packing>
                  </child>
                </widget>
              </child>

diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml
index d18b82d140833f1cedfdc78db10d728f6af639cb..a17b9bfb16942a8c62ba3cda6f6a186f8824fbad 100644 (file)
--- a/helm/matita/matitaGui.ml
+++ b/helm/matita/matitaGui.ml
@@ -31,6 +31,14 @@ open MatitaMisc
 
 let gui_instance = ref None ;;
 
+class type browserWin =
+  (* this class exists only because GEdit.combo_box_entry is not supported by
+   * lablgladecc :-(((( *)
+object
+  inherit MatitaGeneratedGui.browserWin
+  method browserUri: GEdit.combo_box_entry
+end
+
 class console ~(buffer: GText.buffer) () =
   object (self)
     val error_tag   = buffer#create_tag [ `FOREGROUND "red" ]
@@ -275,9 +283,16 @@ class gui () =
     method main = main
 
     method newBrowserWin () =
-      let win = new browserWin () in
-      win#check_widgets ();
-      win
+      object (self)
+        inherit browserWin ()
+        val combo = GEdit.combo_box_entry ()
+        initializer
+          self#check_widgets ();
+          let combo_widget = combo#coerce in
+          browserHBox#add combo_widget;
+          browserHBox#reorder_child combo_widget ~pos:6
+        method browserUri = combo
+      end
 
     method newUriDialog () =
       let dialog = new uriChoiceDialog () in

diff --git a/helm/matita/matitaGui.mli b/helm/matita/matitaGui.mli
index f517bbb9cb3c59415cc6e87933e353af687e3ec5..674f3702cec56241bfd6d10af607e2f0ef394dc6 100644 (file)
--- a/helm/matita/matitaGui.mli
+++ b/helm/matita/matitaGui.mli
@@ -34,6 +34,12 @@ object
   method log_callback: MatitaLog.log_callback
 end
 
+class type browserWin =
+object
+  inherit MatitaGeneratedGui.browserWin
+  method browserUri: GEdit.combo_box_entry
+end
+
   (** @param fname name of the Glade file describing the GUI *)
 class type gui =
 object
@@ -53,7 +59,7 @@ object
      * methods below create a new window on each invocation. You should
      * remember to destroy windows after use *)
 
-  method newBrowserWin:         unit -> MatitaGeneratedGui.browserWin
+  method newBrowserWin:         unit -> browserWin
   method newUriDialog:          unit -> MatitaGeneratedGui.uriChoiceDialog
   method newInterpDialog:       unit -> MatitaGeneratedGui.interpChoiceDialog
   method newConfirmationDialog: unit -> MatitaGeneratedGui.confirmationDialog

diff --git a/helm/matita/matitaMathView.ml b/helm/matita/matitaMathView.ml
index f22b3a170b6546d922721b78d56a0ad50bbb51d1..225738d581b88baee3bce8118e3d75fcc2f74d4f 100644 (file)
--- a/helm/matita/matitaMathView.ml
+++ b/helm/matita/matitaMathView.ml
@@ -381,8 +381,8 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
 
       win#browserForwardButton#misc#set_sensitive false;
       win#browserBackButton#misc#set_sensitive false;
-      ignore (win#browserUri#connect#activate (handle_error' (fun () ->
-        self#loadInput win#browserUri#text)));
+      ignore (win#browserUri#entry#connect#activate (handle_error' (fun () ->
+        self#loadInput win#browserUri#entry#text)));
       ignore (win#browserHomeButton#connect#clicked (handle_error' (fun () ->
         self#load (`About `Current_proof))));
       ignore (win#browserRefreshButton#connect#clicked
@@ -414,8 +414,8 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
 
     method private _getSelectedUri () =
       match model#easy_selection () with
-      | [sel] when is_uri sel -> sel        (* absolute URI selected *)
-      | [sel] -> win#browserUri#text ^ sel  (* relative URI selected *)
+      | [sel] when is_uri sel -> sel  (* absolute URI selected *)
+      | [sel] -> win#browserUri#entry#text ^ sel  (* relative URI selected *)
       | _ -> assert false
 
     (** history RATIONALE 
@@ -523,7 +523,7 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
       self#_loadList l
 
     method private setEntry entry =
-      win#browserUri#set_text (string_of_entry entry);
+      win#browserUri#entry#set_text (string_of_entry entry);
       current_entry <- entry
 
     method private _loadObj obj =
@@ -579,7 +579,11 @@ class cicBrowser_impl ~(history:MatitaTypes.mathViewer_entry MatitaMisc.history)
           match txt with
           | txt when is_uri txt -> `Uri (fix_uri txt)
           | txt when is_dir txt -> `Dir (add_trailing_slash txt)
-          | _ -> raise (Browser_failure (sprintf "unsupported uri: %s" txt))
+          | txt ->
+              (try
+                entry_of_string txt
+              with Invalid_argument _ ->
+                raise (Browser_failure (sprintf "unsupported uri: %s" txt)))
         in
         self#_load entry;
         self#_historyAdd entry

diff --git a/helm/matita/matitaTypes.ml b/helm/matita/matitaTypes.ml
index 800ae1c7e2c569bc1cb604c7ae5a32d5df16b9fd..d7dc383b7757fc5d4da9c6a5b9d34abe99bb95f1 100644 (file)
--- a/helm/matita/matitaTypes.ml
+++ b/helm/matita/matitaTypes.ml
@@ -163,6 +163,13 @@ let string_of_entry = function
   | `Dir uri | `Uri uri -> uri
   | `Whelp (query, _) -> query
 
+let entry_of_string = function
+  | "about:blank" -> `About `Blank
+  | "about:proof" -> `About `Current_proof
+  | "about:us"    -> `About `Us
+  | _ ->  (* only about entries supported ATM *)
+      raise (Invalid_argument "entry_of_string")
+
 class type mathViewer =
   object
     (** @param reuse if set reused last opened cic browser otherwise