X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmatita%2FmatitaGeneratedGui.ml;h=c7d13dfbd4c7d216e3c4397896fc89f119169ee2;hb=6912a028bef118d8e9d7c2847200510a9b055c6a;hp=b192fd73255abcf009031ad0f369c502ee3c3502;hpb=ef9ec8cb57d15426a96fe40d056eb07804753bb9;p=helm.git

diff --git a/helm/matita/matitaGeneratedGui.ml b/helm/matita/matitaGeneratedGui.ml
index b192fd732..c7d13dfbd 100644
--- a/helm/matita/matitaGeneratedGui.ml
+++ b/helm/matita/matitaGeneratedGui.ml
@@ -1,403 +1,5 @@
 (* Automatically generated from matita.glade by lablgladecc *)
 
-class mainWin ?(file="matita.glade") ?domain ?autoconnect(*=true*) () =
-  let xmldata = Glade.create ~file  ~root:"MainWin" ?domain () in
-  object (self)
-    inherit Glade.xml ?autoconnect xmldata
-    val toplevel =
-      new GWindow.window (GtkWindow.Window.cast
-        (Glade.get_widget_msg ~name:"MainWin" ~info:"GtkWindow" xmldata))
-    method toplevel = toplevel
-    val mainWin =
-      new GWindow.window (GtkWindow.Window.cast
-        (Glade.get_widget_msg ~name:"MainWin" ~info:"GtkWindow" xmldata))
-    method mainWin = mainWin
-    val mainWinEventBox =
-      new GBin.event_box (GtkBin.EventBox.cast
-        (Glade.get_widget_msg ~name:"MainWinEventBox" ~info:"GtkEventBox" xmldata))
-    method mainWinEventBox = mainWinEventBox
-    val mainWinShape =
-      new GPack.box (GtkPack.Box.cast
-        (Glade.get_widget_msg ~name:"MainWinShape" ~info:"GtkVBox" xmldata))
-    method mainWinShape = mainWinShape
-    val mainMenuBar =
-      new GMenu.menu_shell (GtkMenu.MenuBar.cast
-        (Glade.get_widget_msg ~name:"MainMenuBar" ~info:"GtkMenuBar" xmldata))
-    method mainMenuBar = mainMenuBar
-    val fileMenu =
-      new GMenu.menu_item (GtkMenu.MenuItem.cast
-        (Glade.get_widget_msg ~name:"FileMenu" ~info:"GtkMenuItem" xmldata))
-    method fileMenu = fileMenu
-    val fileMenu_menu =
-      new GMenu.menu (GtkMenu.Menu.cast
-        (Glade.get_widget_msg ~name:"FileMenu_menu" ~info:"GtkMenu" xmldata))
-    method fileMenu_menu = fileMenu_menu
-    val newMenu =
-      new GMenu.image_menu_item (GtkMenu.ImageMenuItem.cast
-        (Glade.get_widget_msg ~name:"NewMenu" ~info:"GtkImageMenuItem" xmldata))
-    method newMenu = newMenu
-    val image224 =
-      new GMisc.image (GtkMisc.Image.cast
-        (Glade.get_widget_msg ~name:"image224" ~info:"GtkImage" xmldata))
-    method image224 = image224
-    val newMenu_menu =
-      new GMenu.menu (GtkMenu.Menu.cast
-        (Glade.get_widget_msg ~name:"NewMenu_menu" ~info:"GtkMenu" xmldata))
-    method newMenu_menu = newMenu_menu
-    val newProofMenuItem =
-      new GMenu.menu_item (GtkMenu.MenuItem.cast
-        (Glade.get_widget_msg ~name:"NewProofMenuItem" ~info:"GtkMenuItem" xmldata))
-    method newProofMenuItem = newProofMenuItem
-    val newDefsMenuItem =
-      new GMenu.menu_item (GtkMenu.MenuItem.cast
-        (Glade.get_widget_msg ~name:"NewDefsMenuItem" ~info:"GtkMenuItem" xmldata))
-    method newDefsMenuItem = newDefsMenuItem
-    val openMenuItem =
-      new GMenu.image_menu_item (GtkMenu.ImageMenuItem.cast
-        (Glade.get_widget_msg ~name:"OpenMenuItem" ~info:"GtkImageMenuItem" xmldata))
-    method openMenuItem = openMenuItem
-    val image225 =
-      new GMisc.image (GtkMisc.Image.cast
-        (Glade.get_widget_msg ~name:"image225" ~info:"GtkImage" xmldata))
-    method image225 = image225
-    val saveMenuItem =
-      new GMenu.image_menu_item (GtkMenu.ImageMenuItem.cast
-        (Glade.get_widget_msg ~name:"SaveMenuItem" ~info:"GtkImageMenuItem" xmldata))
-    method saveMenuItem = saveMenuItem
-    val image226 =
-      new GMisc.image (GtkMisc.Image.cast
-        (Glade.get_widget_msg ~name:"image226" ~info:"GtkImage" xmldata))
-    method image226 = image226
-    val saveAsMenuItem =
-      new GMenu.image_menu_item (GtkMenu.ImageMenuItem.cast
-        (Glade.get_widget_msg ~name:"SaveAsMenuItem" ~info:"GtkImageMenuItem" xmldata))
-    method saveAsMenuItem = saveAsMenuItem
-    val image227 =
-      new GMisc.image (GtkMisc.Image.cast
-        (Glade.get_widget_msg ~name:"image227" ~info:"GtkImage" xmldata))
-    method image227 = image227
-    val separator1 =
-      new GMenu.menu_item (GtkMenu.MenuItem.cast
-        (Glade.get_widget_msg ~name:"separator1" ~info:"GtkSeparatorMenuItem" xmldata))
-    method separator1 = separator1
-    val quitMenuItem =
-      new GMenu.image_menu_item (GtkMenu.ImageMenuItem.cast
-        (Glade.get_widget_msg ~name:"QuitMenuItem" ~info:"GtkImageMenuItem" xmldata))
-    method quitMenuItem = quitMenuItem
-    val image228 =
-      new GMisc.image (GtkMisc.Image.cast
-        (Glade.get_widget_msg ~name:"image228" ~info:"GtkImage" xmldata))
-    method image228 = image228
-    val editMenu =
-      new GMenu.menu_item (GtkMenu.MenuItem.cast
-        (Glade.get_widget_msg ~name:"EditMenu" ~info:"GtkMenuItem" xmldata))
-    method editMenu = editMenu
-    val viewMenu =
-      new GMenu.menu_item (GtkMenu.MenuItem.cast
-        (Glade.get_widget_msg ~name:"ViewMenu" ~info:"GtkMenuItem" xmldata))
-    method viewMenu = viewMenu
-    val viewMenu_menu =
-      new GMenu.menu (GtkMenu.Menu.cast
-        (Glade.get_widget_msg ~name:"ViewMenu_menu" ~info:"GtkMenu" xmldata))
-    method viewMenu_menu = viewMenu_menu
-    val showToolBarMenuItem =
-      new GMenu.check_menu_item (GtkMenu.CheckMenuItem.cast
-        (Glade.get_widget_msg ~name:"ShowToolBarMenuItem" ~info:"GtkCheckMenuItem" xmldata))
-    method showToolBarMenuItem = showToolBarMenuItem
-    val newCicBrowserMenuItem =
-      new GMenu.menu_item (GtkMenu.MenuItem.cast
-        (Glade.get_widget_msg ~name:"NewCicBrowserMenuItem" ~info:"GtkMenuItem" xmldata))
-    method newCicBrowserMenuItem = newCicBrowserMenuItem
-    val showScriptMenuItem =
-      new GMenu.check_menu_item (GtkMenu.CheckMenuItem.cast
-        (Glade.get_widget_msg ~name:"ShowScriptMenuItem" ~info:"GtkCheckMenuItem" xmldata))
-    method showScriptMenuItem = showScriptMenuItem
-    val separator3 =
-      new GMenu.menu_item (GtkMenu.MenuItem.cast
-        (Glade.get_widget_msg ~name:"separator3" ~info:"GtkSeparatorMenuItem" xmldata))
-    method separator3 = separator3
-    val showConsoleMenuItem =
-      new GMenu.menu_item (GtkMenu.MenuItem.cast
-        (Glade.get_widget_msg ~name:"ShowConsoleMenuItem" ~info:"GtkMenuItem" xmldata))
-    method showConsoleMenuItem = showConsoleMenuItem
-    val debugMenu =
-      new GMenu.menu_item (GtkMenu.MenuItem.cast
-        (Glade.get_widget_msg ~name:"DebugMenu" ~info:"GtkMenuItem" xmldata))
-    method debugMenu = debugMenu
-    val debugMenu_menu =
-      new GMenu.menu (GtkMenu.Menu.cast
-        (Glade.get_widget_msg ~name:"DebugMenu_menu" ~info:"GtkMenu" xmldata))
-    method debugMenu_menu = debugMenu_menu
-    val separator2 =
-      new GMenu.menu_item (GtkMenu.MenuItem.cast
-        (Glade.get_widget_msg ~name:"separator2" ~info:"GtkSeparatorMenuItem" xmldata))
-    method separator2 = separator2
-    val helpMenu =
-      new GMenu.menu_item (GtkMenu.MenuItem.cast
-        (Glade.get_widget_msg ~name:"HelpMenu" ~info:"GtkMenuItem" xmldata))
-    method helpMenu = helpMenu
-    val helpMenu_menu =
-      new GMenu.menu (GtkMenu.Menu.cast
-        (Glade.get_widget_msg ~name:"HelpMenu_menu" ~info:"GtkMenu" xmldata))
-    method helpMenu_menu = helpMenu_menu
-    val aboutMenuItem =
-      new GMenu.menu_item (GtkMenu.MenuItem.cast
-        (Glade.get_widget_msg ~name:"AboutMenuItem" ~info:"GtkMenuItem" xmldata))
-    method aboutMenuItem = aboutMenuItem
-    val mainVPanes =
-      new GPack.paned (GtkPack.Paned.cast
-        (Glade.get_widget_msg ~name:"MainVPanes" ~info:"GtkVPaned" xmldata))
-    method mainVPanes = mainVPanes
-    val sequentsNotebook =
-      new GPack.notebook (GtkPack.Notebook.cast
-        (Glade.get_widget_msg ~name:"SequentsNotebook" ~info:"GtkNotebook" xmldata))
-    method sequentsNotebook = sequentsNotebook
-    val consoleEventBox =
-      new GBin.event_box (GtkBin.EventBox.cast
-        (Glade.get_widget_msg ~name:"ConsoleEventBox" ~info:"GtkEventBox" xmldata))
-    method consoleEventBox = consoleEventBox
-    val consoleHBox =
-      new GPack.box (GtkPack.Box.cast
-        (Glade.get_widget_msg ~name:"ConsoleHBox" ~info:"GtkHBox" xmldata))
-    method consoleHBox = consoleHBox
-    val vbox6 =
-      new GPack.box (GtkPack.Box.cast
-        (Glade.get_widget_msg ~name:"vbox6" ~info:"GtkVBox" xmldata))
-    method vbox6 = vbox6
-    val hideConsoleButton =
-      new GButton.button (GtkButton.Button.cast
-        (Glade.get_widget_msg ~name:"HideConsoleButton" ~info:"GtkButton" xmldata))
-    method hideConsoleButton = hideConsoleButton
-    val image169 =
-      new GMisc.image (GtkMisc.Image.cast
-        (Glade.get_widget_msg ~name:"image169" ~info:"GtkImage" xmldata))
-    method image169 = image169
-    val scrolledConsole =
-      new GBin.scrolled_window (GtkBin.ScrolledWindow.cast
-        (Glade.get_widget_msg ~name:"ScrolledConsole" ~info:"GtkScrolledWindow" xmldata))
-    method scrolledConsole = scrolledConsole
-    val mainStatusBar =
-      new GMisc.statusbar (GtkMisc.Statusbar.cast
-        (Glade.get_widget_msg ~name:"MainStatusBar" ~info:"GtkStatusbar" xmldata))
-    method mainStatusBar = mainStatusBar
-    method reparent parent =
-      mainWinEventBox#misc#reparent parent;
-      toplevel#destroy ()
-    method check_widgets () = ()
-  end
-class proofWin ?(file="matita.glade") ?domain ?autoconnect(*=true*) () =
-  let xmldata = Glade.create ~file  ~root:"ProofWin" ?domain () in
-  object (self)
-    inherit Glade.xml ?autoconnect xmldata
-    val toplevel =
-      new GWindow.window (GtkWindow.Window.cast
-        (Glade.get_widget_msg ~name:"ProofWin" ~info:"GtkWindow" xmldata))
-    method toplevel = toplevel
-    val proofWin =
-      new GWindow.window (GtkWindow.Window.cast
-        (Glade.get_widget_msg ~name:"ProofWin" ~info:"GtkWindow" xmldata))
-    method proofWin = proofWin
-    val proofWinEventBox =
-      new GBin.event_box (GtkBin.EventBox.cast
-        (Glade.get_widget_msg ~name:"ProofWinEventBox" ~info:"GtkEventBox" xmldata))
-    method proofWinEventBox = proofWinEventBox
-    val scrolledProof =
-      new GBin.scrolled_window (GtkBin.ScrolledWindow.cast
-        (Glade.get_widget_msg ~name:"ScrolledProof" ~info:"GtkScrolledWindow" xmldata))
-    method scrolledProof = scrolledProof
-    method reparent parent =
-      proofWinEventBox#misc#reparent parent;
-      toplevel#destroy ()
-    method check_widgets () = ()
-  end
-class fileSelectionWin ?(file="matita.glade") ?domain ?autoconnect(*=true*) () =
-  let xmldata = Glade.create ~file  ~root:"FileSelectionWin" ?domain () in
-  object (self)
-    inherit Glade.xml ?autoconnect xmldata
-    val toplevel =
-      new GWindow.file_selection (GtkWindow.FileSelection.cast
-        (Glade.get_widget_msg ~name:"FileSelectionWin" ~info:"GtkFileSelection" xmldata))
-    method toplevel = toplevel
-    val fileSelectionWin =
-      new GWindow.file_selection (GtkWindow.FileSelection.cast
-        (Glade.get_widget_msg ~name:"FileSelectionWin" ~info:"GtkFileSelection" xmldata))
-    method fileSelectionWin = fileSelectionWin
-    val fileSelCancelButton =
-      new GButton.button (GtkButton.Button.cast
-        (Glade.get_widget_msg ~name:"fileSelCancelButton" ~info:"GtkButton" xmldata))
-    method fileSelCancelButton = fileSelCancelButton
-    val fileSelOkButton =
-      new GButton.button (GtkButton.Button.cast
-        (Glade.get_widget_msg ~name:"fileSelOkButton" ~info:"GtkButton" xmldata))
-    method fileSelOkButton = fileSelOkButton
-    method check_widgets () = ()
-  end
-class toolBarWin ?(file="matita.glade") ?domain ?autoconnect(*=true*) () =
-  let xmldata = Glade.create ~file  ~root:"ToolBarWin" ?domain () in
-  object (self)
-    inherit Glade.xml ?autoconnect xmldata
-    val toplevel =
-      new GWindow.window (GtkWindow.Window.cast
-        (Glade.get_widget_msg ~name:"ToolBarWin" ~info:"GtkWindow" xmldata))
-    method toplevel = toplevel
-    val toolBarWin =
-      new GWindow.window (GtkWindow.Window.cast
-        (Glade.get_widget_msg ~name:"ToolBarWin" ~info:"GtkWindow" xmldata))
-    method toolBarWin = toolBarWin
-    val toolBarEventBox =
-      new GBin.event_box (GtkBin.EventBox.cast
-        (Glade.get_widget_msg ~name:"ToolBarEventBox" ~info:"GtkEventBox" xmldata))
-    method toolBarEventBox = toolBarEventBox
-    val toolBarVBox =
-      new GPack.box (GtkPack.Box.cast
-        (Glade.get_widget_msg ~name:"ToolBarVBox" ~info:"GtkVBox" xmldata))
-    method toolBarVBox = toolBarVBox
-    val toolbar2 =
-      new GButton.toolbar (GtkButton.Toolbar.cast
-        (Glade.get_widget_msg ~name:"toolbar2" ~info:"GtkToolbar" xmldata))
-    method toolbar2 = toolbar2
-    val introsButton =
-      new GButton.button (GtkButton.Button.cast
-        (Glade.get_widget_msg ~name:"introsButton" ~info:"GtkButton" xmldata))
-    method introsButton = introsButton
-    val applyButton =
-      new GButton.button (GtkButton.Button.cast
-        (Glade.get_widget_msg ~name:"applyButton" ~info:"GtkButton" xmldata))
-    method applyButton = applyButton
-    val exactButton =
-      new GButton.button (GtkButton.Button.cast
-        (Glade.get_widget_msg ~name:"exactButton" ~info:"GtkButton" xmldata))
-    method exactButton = exactButton
-    val toolbar3 =
-      new GButton.toolbar (GtkButton.Toolbar.cast
-        (Glade.get_widget_msg ~name:"toolbar3" ~info:"GtkToolbar" xmldata))
-    method toolbar3 = toolbar3
-    val elimButton =
-      new GButton.button (GtkButton.Button.cast
-        (Glade.get_widget_msg ~name:"elimButton" ~info:"GtkButton" xmldata))
-    method elimButton = elimButton
-    val elimTypeButton =
-      new GButton.button (GtkButton.Button.cast
-        (Glade.get_widget_msg ~name:"elimTypeButton" ~info:"GtkButton" xmldata))
-    method elimTypeButton = elimTypeButton
-    val toolbar4 =
-      new GButton.toolbar (GtkButton.Toolbar.cast
-        (Glade.get_widget_msg ~name:"toolbar4" ~info:"GtkToolbar" xmldata))
-    method toolbar4 = toolbar4
-    val splitButton =
-      new GButton.button (GtkButton.Button.cast
-        (Glade.get_widget_msg ~name:"splitButton" ~info:"GtkButton" xmldata))
-    method splitButton = splitButton
-    val leftButton =
-      new GButton.button (GtkButton.Button.cast
-        (Glade.get_widget_msg ~name:"leftButton" ~info:"GtkButton" xmldata))
-    method leftButton = leftButton
-    val rightButton =
-      new GButton.button (GtkButton.Button.cast
-        (Glade.get_widget_msg ~name:"rightButton" ~info:"GtkButton" xmldata))
-    method rightButton = rightButton
-    val existsButton =
-      new GButton.button (GtkButton.Button.cast
-        (Glade.get_widget_msg ~name:"existsButton" ~info:"GtkButton" xmldata))
-    method existsButton = existsButton
-    val toolbar5 =
-      new GButton.toolbar (GtkButton.Toolbar.cast
-        (Glade.get_widget_msg ~name:"toolbar5" ~info:"GtkToolbar" xmldata))
-    method toolbar5 = toolbar5
-    val reflexivityButton =
-      new GButton.button (GtkButton.Button.cast
-        (Glade.get_widget_msg ~name:"reflexivityButton" ~info:"GtkButton" xmldata))
-    method reflexivityButton = reflexivityButton
-    val symmetryButton =
-      new GButton.button (GtkButton.Button.cast
-        (Glade.get_widget_msg ~name:"symmetryButton" ~info:"GtkButton" xmldata))
-    method symmetryButton = symmetryButton
-    val transitivityButton =
-      new GButton.button (GtkButton.Button.cast
-        (Glade.get_widget_msg ~name:"transitivityButton" ~info:"GtkButton" xmldata))
-    method transitivityButton = transitivityButton
-    val toolbar8 =
-      new GButton.toolbar (GtkButton.Toolbar.cast
-        (Glade.get_widget_msg ~name:"toolbar8" ~info:"GtkToolbar" xmldata))
-    method toolbar8 = toolbar8
-    val simplifyButton =
-      new GButton.button (GtkButton.Button.cast
-        (Glade.get_widget_msg ~name:"simplifyButton" ~info:"GtkButton" xmldata))
-    method simplifyButton = simplifyButton
-    val reduceButton =
-      new GButton.button (GtkButton.Button.cast
-        (Glade.get_widget_msg ~name:"reduceButton" ~info:"GtkButton" xmldata))
-    method reduceButton = reduceButton
-    val whdButton =
-      new GButton.button (GtkButton.Button.cast
-        (Glade.get_widget_msg ~name:"whdButton" ~info:"GtkButton" xmldata))
-    method whdButton = whdButton
-    val toolbar6 =
-      new GButton.toolbar (GtkButton.Toolbar.cast
-        (Glade.get_widget_msg ~name:"toolbar6" ~info:"GtkToolbar" xmldata))
-    method toolbar6 = toolbar6
-    val assumptionButton =
-      new GButton.button (GtkButton.Button.cast
-        (Glade.get_widget_msg ~name:"assumptionButton" ~info:"GtkButton" xmldata))
-    method assumptionButton = assumptionButton
-    val autoButton =
-      new GButton.button (GtkButton.Button.cast
-        (Glade.get_widget_msg ~name:"autoButton" ~info:"GtkButton" xmldata))
-    method autoButton = autoButton
-    val toolbar7 =
-      new GButton.toolbar (GtkButton.Toolbar.cast
-        (Glade.get_widget_msg ~name:"toolbar7" ~info:"GtkToolbar" xmldata))
-    method toolbar7 = toolbar7
-    val cutButton =
-      new GButton.button (GtkButton.Button.cast
-        (Glade.get_widget_msg ~name:"cutButton" ~info:"GtkButton" xmldata))
-    method cutButton = cutButton
-    val replaceButton =
-      new GButton.button (GtkButton.Button.cast
-        (Glade.get_widget_msg ~name:"replaceButton" ~info:"GtkButton" xmldata))
-    method replaceButton = replaceButton
-    method reparent parent =
-      toolBarEventBox#misc#reparent parent;
-      toplevel#destroy ()
-    method check_widgets () = ()
-  end
-class confirmationDialog ?(file="matita.glade") ?domain ?autoconnect(*=true*) () =
-  let xmldata = Glade.create ~file  ~root:"ConfirmationDialog" ?domain () in
-  object (self)
-    inherit Glade.xml ?autoconnect xmldata
-    val toplevel =
-      new GWindow.dialog_any (GtkWindow.Dialog.cast
-        (Glade.get_widget_msg ~name:"ConfirmationDialog" ~info:"GtkDialog" xmldata))
-    method toplevel = toplevel
-    val confirmationDialog =
-      new GWindow.dialog_any (GtkWindow.Dialog.cast
-        (Glade.get_widget_msg ~name:"ConfirmationDialog" ~info:"GtkDialog" xmldata))
-    method confirmationDialog = confirmationDialog
-    val dialog_vbox1 =
-      new GPack.box (GtkPack.Box.cast
-        (Glade.get_widget_msg ~name:"dialog-vbox1" ~info:"GtkVBox" xmldata))
-    method dialog_vbox1 = dialog_vbox1
-    val dialog_action_area1 =
-      new GPack.button_box (GtkPack.BBox.cast
-        (Glade.get_widget_msg ~name:"dialog-action_area1" ~info:"GtkHButtonBox" xmldata))
-    method dialog_action_area1 = dialog_action_area1
-    val confirmationDialogCancelButton =
-      new GButton.button (GtkButton.Button.cast
-        (Glade.get_widget_msg ~name:"ConfirmationDialogCancelButton" ~info:"GtkButton" xmldata))
-    method confirmationDialogCancelButton = confirmationDialogCancelButton
-    val confirmationDialogOkButton =
-      new GButton.button (GtkButton.Button.cast
-        (Glade.get_widget_msg ~name:"ConfirmationDialogOkButton" ~info:"GtkButton" xmldata))
-    method confirmationDialogOkButton = confirmationDialogOkButton
-    val confirmationDialogLabel =
-      new GMisc.label (GtkMisc.Label.cast
-        (Glade.get_widget_msg ~name:"ConfirmationDialogLabel" ~info:"GtkLabel" xmldata))
-    method confirmationDialogLabel = confirmationDialogLabel
-    method reparent parent =
-      dialog_vbox1#misc#reparent parent;
-      toplevel#destroy ()
-    method check_widgets () = ()
-  end
 class aboutWin ?(file="matita.glade") ?domain ?autoconnect(*=true*) () =
   let xmldata = Glade.create ~file  ~root:"AboutWin" ?domain () in
   object (self)
@@ -431,107 +33,203 @@ class aboutWin ?(file="matita.glade") ?domain ?autoconnect(*=true*) () =
       toplevel#destroy ()
     method check_widgets () = ()
   end
-class uriChoiceDialog ?(file="matita.glade") ?domain ?autoconnect(*=true*) () =
-  let xmldata = Glade.create ~file  ~root:"UriChoiceDialog" ?domain () in
+class browserWin ?(file="matita.glade") ?domain ?autoconnect(*=true*) () =
+  let xmldata = Glade.create ~file  ~root:"BrowserWin" ?domain () in
   object (self)
     inherit Glade.xml ?autoconnect xmldata
     val toplevel =
-      new GWindow.dialog_any (GtkWindow.Dialog.cast
-        (Glade.get_widget_msg ~name:"UriChoiceDialog" ~info:"GtkDialog" xmldata))
+      new GWindow.window (GtkWindow.Window.cast
+        (Glade.get_widget_msg ~name:"BrowserWin" ~info:"GtkWindow" xmldata))
     method toplevel = toplevel
-    val uriChoiceDialog =
-      new GWindow.dialog_any (GtkWindow.Dialog.cast
-        (Glade.get_widget_msg ~name:"UriChoiceDialog" ~info:"GtkDialog" xmldata))
-    method uriChoiceDialog = uriChoiceDialog
-    val dialog_vbox3 =
+    val browserWin =
+      new GWindow.window (GtkWindow.Window.cast
+        (Glade.get_widget_msg ~name:"BrowserWin" ~info:"GtkWindow" xmldata))
+    method browserWin = browserWin
+    val browserWinEventBox =
+      new GBin.event_box (GtkBin.EventBox.cast
+        (Glade.get_widget_msg ~name:"BrowserWinEventBox" ~info:"GtkEventBox" xmldata))
+    method browserWinEventBox = browserWinEventBox
+    val browserVBox =
       new GPack.box (GtkPack.Box.cast
-        (Glade.get_widget_msg ~name:"dialog-vbox3" ~info:"GtkVBox" xmldata))
-    method dialog_vbox3 = dialog_vbox3
-    val dialog_action_area3 =
-      new GPack.button_box (GtkPack.BBox.cast
-        (Glade.get_widget_msg ~name:"dialog-action_area3" ~info:"GtkHButtonBox" xmldata))
-    method dialog_action_area3 = dialog_action_area3
-    val uriChoiceAbortButton =
+        (Glade.get_widget_msg ~name:"BrowserVBox" ~info:"GtkVBox" xmldata))
+    method browserVBox = browserVBox
+    val handlebox1 =
+      new GBin.handle_box (GtkBin.HandleBox.cast
+        (Glade.get_widget_msg ~name:"handlebox1" ~info:"GtkHandleBox" xmldata))
+    method handlebox1 = handlebox1
+    val hbox7 =
+      new GPack.box (GtkPack.Box.cast
+        (Glade.get_widget_msg ~name:"hbox7" ~info:"GtkHBox" xmldata))
+    method hbox7 = hbox7
+    val browserNewButton =
       new GButton.button (GtkButton.Button.cast
-        (Glade.get_widget_msg ~name:"UriChoiceAbortButton" ~info:"GtkButton" xmldata))
-    method uriChoiceAbortButton = uriChoiceAbortButton
-    val uriChoiceSelectedButton =
+        (Glade.get_widget_msg ~name:"BrowserNewButton" ~info:"GtkButton" xmldata))
+    method browserNewButton = browserNewButton
+    val image191 =
+      new GMisc.image (GtkMisc.Image.cast
+        (Glade.get_widget_msg ~name:"image191" ~info:"GtkImage" xmldata))
+    method image191 = image191
+    val browserBackButton =
       new GButton.button (GtkButton.Button.cast
-        (Glade.get_widget_msg ~name:"UriChoiceSelectedButton" ~info:"GtkButton" xmldata))
-    method uriChoiceSelectedButton = uriChoiceSelectedButton
-    val alignment2 =
+        (Glade.get_widget_msg ~name:"BrowserBackButton" ~info:"GtkButton" xmldata))
+    method browserBackButton = browserBackButton
+    val alignment3 =
       new GBin.alignment (GtkBin.Alignment.cast
-        (Glade.get_widget_msg ~name:"alignment2" ~info:"GtkAlignment" xmldata))
-    method alignment2 = alignment2
-    val hbox3 =
+        (Glade.get_widget_msg ~name:"alignment3" ~info:"GtkAlignment" xmldata))
+    method alignment3 = alignment3
+    val hbox6 =
       new GPack.box (GtkPack.Box.cast
-        (Glade.get_widget_msg ~name:"hbox3" ~info:"GtkHBox" xmldata))
-    method hbox3 = hbox3
-    val image19 =
+        (Glade.get_widget_msg ~name:"hbox6" ~info:"GtkHBox" xmldata))
+    method hbox6 = hbox6
+    val image188 =
       new GMisc.image (GtkMisc.Image.cast
-        (Glade.get_widget_msg ~name:"image19" ~info:"GtkImage" xmldata))
-    method image19 = image19
-    val label3 =
+        (Glade.get_widget_msg ~name:"image188" ~info:"GtkImage" xmldata))
+    method image188 = image188
+    val label10 =
       new GMisc.label (GtkMisc.Label.cast
-        (Glade.get_widget_msg ~name:"label3" ~info:"GtkLabel" xmldata))
-    method label3 = label3
-    val uriChoiceConstantsButton =
+        (Glade.get_widget_msg ~name:"label10" ~info:"GtkLabel" xmldata))
+    method label10 = label10
+    val browserForwardButton =
       new GButton.button (GtkButton.Button.cast
-        (Glade.get_widget_msg ~name:"UriChoiceConstantsButton" ~info:"GtkButton" xmldata))
-    method uriChoiceConstantsButton = uriChoiceConstantsButton
-    val uriChoiceAutoButton =
+        (Glade.get_widget_msg ~name:"BrowserForwardButton" ~info:"GtkButton" xmldata))
+    method browserForwardButton = browserForwardButton
+    val image189 =
+      new GMisc.image (GtkMisc.Image.cast
+        (Glade.get_widget_msg ~name:"image189" ~info:"GtkImage" xmldata))
+    method image189 = image189
+    val browserRefreshButton =
       new GButton.button (GtkButton.Button.cast
-        (Glade.get_widget_msg ~name:"UriChoiceAutoButton" ~info:"GtkButton" xmldata))
-    method uriChoiceAutoButton = uriChoiceAutoButton
-    val alignment1 =
-      new GBin.alignment (GtkBin.Alignment.cast
-        (Glade.get_widget_msg ~name:"alignment1" ~info:"GtkAlignment" xmldata))
-    method alignment1 = alignment1
-    val hbox1 =
-      new GPack.box (GtkPack.Box.cast
-        (Glade.get_widget_msg ~name:"hbox1" ~info:"GtkHBox" xmldata))
-    method hbox1 = hbox1
-    val image18 =
+        (Glade.get_widget_msg ~name:"BrowserRefreshButton" ~info:"GtkButton" xmldata))
+    method browserRefreshButton = browserRefreshButton
+    val image229 =
       new GMisc.image (GtkMisc.Image.cast
-        (Glade.get_widget_msg ~name:"image18" ~info:"GtkImage" xmldata))
-    method image18 = image18
-    val label1 =
-      new GMisc.label (GtkMisc.Label.cast
-        (Glade.get_widget_msg ~name:"label1" ~info:"GtkLabel" xmldata))
-    method label1 = label1
-    val vbox2 =
+        (Glade.get_widget_msg ~name:"image229" ~info:"GtkImage" xmldata))
+    method image229 = image229
+    val browserHomeButton =
+      new GButton.button (GtkButton.Button.cast
+        (Glade.get_widget_msg ~name:"BrowserHomeButton" ~info:"GtkButton" xmldata))
+    method browserHomeButton = browserHomeButton
+    val image190 =
+      new GMisc.image (GtkMisc.Image.cast
+        (Glade.get_widget_msg ~name:"image190" ~info:"GtkImage" xmldata))
+    method image190 = image190
+    val image187 =
+      new GMisc.image (GtkMisc.Image.cast
+        (Glade.get_widget_msg ~name:"image187" ~info:"GtkImage" xmldata))
+    method image187 = image187
+    val browserUri =
+      new GEdit.entry (GtkEdit.Entry.cast
+        (Glade.get_widget_msg ~name:"BrowserUri" ~info:"GtkEntry" xmldata))
+    method browserUri = browserUri
+    val frame1 =
+      new GBin.frame (GtkBin.Frame.cast
+        (Glade.get_widget_msg ~name:"frame1" ~info:"GtkFrame" xmldata))
+    method frame1 = frame1
+    val scrolledBrowser =
+      new GBin.scrolled_window (GtkBin.ScrolledWindow.cast
+        (Glade.get_widget_msg ~name:"ScrolledBrowser" ~info:"GtkScrolledWindow" xmldata))
+    method scrolledBrowser = scrolledBrowser
+    method reparent parent =
+      browserWinEventBox#misc#reparent parent;
+      toplevel#destroy ()
+    method check_widgets () = ()
+  end
+class confirmationDialog ?(file="matita.glade") ?domain ?autoconnect(*=true*) () =
+  let xmldata = Glade.create ~file  ~root:"ConfirmationDialog" ?domain () in
+  object (self)
+    inherit Glade.xml ?autoconnect xmldata
+    val toplevel =
+      new GWindow.dialog_any (GtkWindow.Dialog.cast
+        (Glade.get_widget_msg ~name:"ConfirmationDialog" ~info:"GtkDialog" xmldata))
+    method toplevel = toplevel
+    val confirmationDialog =
+      new GWindow.dialog_any (GtkWindow.Dialog.cast
+        (Glade.get_widget_msg ~name:"ConfirmationDialog" ~info:"GtkDialog" xmldata))
+    method confirmationDialog = confirmationDialog
+    val dialog_vbox1 =
       new GPack.box (GtkPack.Box.cast
-        (Glade.get_widget_msg ~name:"vbox2" ~info:"GtkVBox" xmldata))
-    method vbox2 = vbox2
-    val uriChoiceLabel =
+        (Glade.get_widget_msg ~name:"dialog-vbox1" ~info:"GtkVBox" xmldata))
+    method dialog_vbox1 = dialog_vbox1
+    val dialog_action_area1 =
+      new GPack.button_box (GtkPack.BBox.cast
+        (Glade.get_widget_msg ~name:"dialog-action_area1" ~info:"GtkHButtonBox" xmldata))
+    method dialog_action_area1 = dialog_action_area1
+    val confirmationDialogCancelButton =
+      new GButton.button (GtkButton.Button.cast
+        (Glade.get_widget_msg ~name:"ConfirmationDialogCancelButton" ~info:"GtkButton" xmldata))
+    method confirmationDialogCancelButton = confirmationDialogCancelButton
+    val confirmationDialogOkButton =
+      new GButton.button (GtkButton.Button.cast
+        (Glade.get_widget_msg ~name:"ConfirmationDialogOkButton" ~info:"GtkButton" xmldata))
+    method confirmationDialogOkButton = confirmationDialogOkButton
+    val confirmationDialogLabel =
       new GMisc.label (GtkMisc.Label.cast
-        (Glade.get_widget_msg ~name:"UriChoiceLabel" ~info:"GtkLabel" xmldata))
-    method uriChoiceLabel = uriChoiceLabel
-    val scrolledwindow1 =
-      new GBin.scrolled_window (GtkBin.ScrolledWindow.cast
-        (Glade.get_widget_msg ~name:"scrolledwindow1" ~info:"GtkScrolledWindow" xmldata))
-    method scrolledwindow1 = scrolledwindow1
-    val uriChoiceTreeView =
-      new GTree.view (GtkTree.TreeView.cast
-        (Glade.get_widget_msg ~name:"UriChoiceTreeView" ~info:"GtkTreeView" xmldata))
-    method uriChoiceTreeView = uriChoiceTreeView
-    val hbox2 =
+        (Glade.get_widget_msg ~name:"ConfirmationDialogLabel" ~info:"GtkLabel" xmldata))
+    method confirmationDialogLabel = confirmationDialogLabel
+    method reparent parent =
+      dialog_vbox1#misc#reparent parent;
+      toplevel#destroy ()
+    method check_widgets () = ()
+  end
+class emptyDialog ?(file="matita.glade") ?domain ?autoconnect(*=true*) () =
+  let xmldata = Glade.create ~file  ~root:"EmptyDialog" ?domain () in
+  object (self)
+    inherit Glade.xml ?autoconnect xmldata
+    val toplevel =
+      new GWindow.dialog_any (GtkWindow.Dialog.cast
+        (Glade.get_widget_msg ~name:"EmptyDialog" ~info:"GtkDialog" xmldata))
+    method toplevel = toplevel
+    val emptyDialog =
+      new GWindow.dialog_any (GtkWindow.Dialog.cast
+        (Glade.get_widget_msg ~name:"EmptyDialog" ~info:"GtkDialog" xmldata))
+    method emptyDialog = emptyDialog
+    val emptyDialogVBox =
       new GPack.box (GtkPack.Box.cast
-        (Glade.get_widget_msg ~name:"hbox2" ~info:"GtkHBox" xmldata))
-    method hbox2 = hbox2
-    val label2 =
+        (Glade.get_widget_msg ~name:"EmptyDialogVBox" ~info:"GtkVBox" xmldata))
+    method emptyDialogVBox = emptyDialogVBox
+    val dialog_action_area5 =
+      new GPack.button_box (GtkPack.BBox.cast
+        (Glade.get_widget_msg ~name:"dialog-action_area5" ~info:"GtkHButtonBox" xmldata))
+    method dialog_action_area5 = dialog_action_area5
+    val emptyDialogCancelButton =
+      new GButton.button (GtkButton.Button.cast
+        (Glade.get_widget_msg ~name:"EmptyDialogCancelButton" ~info:"GtkButton" xmldata))
+    method emptyDialogCancelButton = emptyDialogCancelButton
+    val emptyDialogOkButton =
+      new GButton.button (GtkButton.Button.cast
+        (Glade.get_widget_msg ~name:"EmptyDialogOkButton" ~info:"GtkButton" xmldata))
+    method emptyDialogOkButton = emptyDialogOkButton
+    val emptyDialogLabel =
       new GMisc.label (GtkMisc.Label.cast
-        (Glade.get_widget_msg ~name:"label2" ~info:"GtkLabel" xmldata))
-    method label2 = label2
-    val entry1 =
-      new GEdit.entry (GtkEdit.Entry.cast
-        (Glade.get_widget_msg ~name:"entry1" ~info:"GtkEntry" xmldata))
-    method entry1 = entry1
+        (Glade.get_widget_msg ~name:"EmptyDialogLabel" ~info:"GtkLabel" xmldata))
+    method emptyDialogLabel = emptyDialogLabel
     method reparent parent =
-      dialog_vbox3#misc#reparent parent;
+      emptyDialogVBox#misc#reparent parent;
       toplevel#destroy ()
     method check_widgets () = ()
   end
+class fileSelectionWin ?(file="matita.glade") ?domain ?autoconnect(*=true*) () =
+  let xmldata = Glade.create ~file  ~root:"FileSelectionWin" ?domain () in
+  object (self)
+    inherit Glade.xml ?autoconnect xmldata
+    val toplevel =
+      new GWindow.file_selection (GtkWindow.FileSelection.cast
+        (Glade.get_widget_msg ~name:"FileSelectionWin" ~info:"GtkFileSelection" xmldata))
+    method toplevel = toplevel
+    val fileSelectionWin =
+      new GWindow.file_selection (GtkWindow.FileSelection.cast
+        (Glade.get_widget_msg ~name:"FileSelectionWin" ~info:"GtkFileSelection" xmldata))
+    method fileSelectionWin = fileSelectionWin
+    val fileSelCancelButton =
+      new GButton.button (GtkButton.Button.cast
+        (Glade.get_widget_msg ~name:"fileSelCancelButton" ~info:"GtkButton" xmldata))
+    method fileSelCancelButton = fileSelCancelButton
+    val fileSelOkButton =
+      new GButton.button (GtkButton.Button.cast
+        (Glade.get_widget_msg ~name:"fileSelOkButton" ~info:"GtkButton" xmldata))
+    method fileSelOkButton = fileSelOkButton
+    method check_widgets () = ()
+  end
 class interpChoiceDialog ?(file="matita.glade") ?domain ?autoconnect(*=true*) () =
   let xmldata = Glade.create ~file  ~root:"InterpChoiceDialog" ?domain () in
   object (self)
@@ -566,84 +264,207 @@ class interpChoiceDialog ?(file="matita.glade") ?domain ?autoconnect(*=true*) ()
     method interpChoiceOkButton = interpChoiceOkButton
     val vbox3 =
       new GPack.box (GtkPack.Box.cast
-        (Glade.get_widget_msg ~name:"vbox3" ~info:"GtkVBox" xmldata))
-    method vbox3 = vbox3
-    val interpChoiceDialogLabel =
-      new GMisc.label (GtkMisc.Label.cast
-        (Glade.get_widget_msg ~name:"InterpChoiceDialogLabel" ~info:"GtkLabel" xmldata))
-    method interpChoiceDialogLabel = interpChoiceDialogLabel
-    val scrolledwindow4 =
-      new GBin.scrolled_window (GtkBin.ScrolledWindow.cast
-        (Glade.get_widget_msg ~name:"scrolledwindow4" ~info:"GtkScrolledWindow" xmldata))
-    method scrolledwindow4 = scrolledwindow4
-    val interpChoiceTreeView =
-      new GTree.view (GtkTree.TreeView.cast
-        (Glade.get_widget_msg ~name:"InterpChoiceTreeView" ~info:"GtkTreeView" xmldata))
-    method interpChoiceTreeView = interpChoiceTreeView
-    method reparent parent =
-      dialog_vbox4#misc#reparent parent;
-      toplevel#destroy ()
-    method check_widgets () = ()
-  end
-class emptyDialog ?(file="matita.glade") ?domain ?autoconnect(*=true*) () =
-  let xmldata = Glade.create ~file  ~root:"EmptyDialog" ?domain () in
-  object (self)
-    inherit Glade.xml ?autoconnect xmldata
-    val toplevel =
-      new GWindow.dialog_any (GtkWindow.Dialog.cast
-        (Glade.get_widget_msg ~name:"EmptyDialog" ~info:"GtkDialog" xmldata))
-    method toplevel = toplevel
-    val emptyDialog =
-      new GWindow.dialog_any (GtkWindow.Dialog.cast
-        (Glade.get_widget_msg ~name:"EmptyDialog" ~info:"GtkDialog" xmldata))
-    method emptyDialog = emptyDialog
-    val emptyDialogVBox =
+        (Glade.get_widget_msg ~name:"vbox3" ~info:"GtkVBox" xmldata))
+    method vbox3 = vbox3
+    val interpChoiceDialogLabel =
+      new GMisc.label (GtkMisc.Label.cast
+        (Glade.get_widget_msg ~name:"InterpChoiceDialogLabel" ~info:"GtkLabel" xmldata))
+    method interpChoiceDialogLabel = interpChoiceDialogLabel
+    val scrolledwindow4 =
+      new GBin.scrolled_window (GtkBin.ScrolledWindow.cast
+        (Glade.get_widget_msg ~name:"scrolledwindow4" ~info:"GtkScrolledWindow" xmldata))
+    method scrolledwindow4 = scrolledwindow4
+    val interpChoiceTreeView =
+      new GTree.view (GtkTree.TreeView.cast
+        (Glade.get_widget_msg ~name:"InterpChoiceTreeView" ~info:"GtkTreeView" xmldata))
+    method interpChoiceTreeView = interpChoiceTreeView
+    method reparent parent =
+      dialog_vbox4#misc#reparent parent;
+      toplevel#destroy ()
+    method check_widgets () = ()
+  end
+class mainWin ?(file="matita.glade") ?domain ?autoconnect(*=true*) () =
+  let xmldata = Glade.create ~file  ~root:"MainWin" ?domain () in
+  object (self)
+    inherit Glade.xml ?autoconnect xmldata
+    val toplevel =
+      new GWindow.window (GtkWindow.Window.cast
+        (Glade.get_widget_msg ~name:"MainWin" ~info:"GtkWindow" xmldata))
+    method toplevel = toplevel
+    val mainWin =
+      new GWindow.window (GtkWindow.Window.cast
+        (Glade.get_widget_msg ~name:"MainWin" ~info:"GtkWindow" xmldata))
+    method mainWin = mainWin
+    val mainWinEventBox =
+      new GBin.event_box (GtkBin.EventBox.cast
+        (Glade.get_widget_msg ~name:"MainWinEventBox" ~info:"GtkEventBox" xmldata))
+    method mainWinEventBox = mainWinEventBox
+    val mainWinShape =
+      new GPack.box (GtkPack.Box.cast
+        (Glade.get_widget_msg ~name:"MainWinShape" ~info:"GtkVBox" xmldata))
+    method mainWinShape = mainWinShape
+    val mainMenuBar =
+      new GMenu.menu_shell (GtkMenu.MenuBar.cast
+        (Glade.get_widget_msg ~name:"MainMenuBar" ~info:"GtkMenuBar" xmldata))
+    method mainMenuBar = mainMenuBar
+    val fileMenu =
+      new GMenu.menu_item (GtkMenu.MenuItem.cast
+        (Glade.get_widget_msg ~name:"FileMenu" ~info:"GtkMenuItem" xmldata))
+    method fileMenu = fileMenu
+    val fileMenu_menu =
+      new GMenu.menu (GtkMenu.Menu.cast
+        (Glade.get_widget_msg ~name:"FileMenu_menu" ~info:"GtkMenu" xmldata))
+    method fileMenu_menu = fileMenu_menu
+    val newMenu =
+      new GMenu.image_menu_item (GtkMenu.ImageMenuItem.cast
+        (Glade.get_widget_msg ~name:"NewMenu" ~info:"GtkImageMenuItem" xmldata))
+    method newMenu = newMenu
+    val image224 =
+      new GMisc.image (GtkMisc.Image.cast
+        (Glade.get_widget_msg ~name:"image224" ~info:"GtkImage" xmldata))
+    method image224 = image224
+    val newMenu_menu =
+      new GMenu.menu (GtkMenu.Menu.cast
+        (Glade.get_widget_msg ~name:"NewMenu_menu" ~info:"GtkMenu" xmldata))
+    method newMenu_menu = newMenu_menu
+    val newProofMenuItem =
+      new GMenu.menu_item (GtkMenu.MenuItem.cast
+        (Glade.get_widget_msg ~name:"NewProofMenuItem" ~info:"GtkMenuItem" xmldata))
+    method newProofMenuItem = newProofMenuItem
+    val newDefsMenuItem =
+      new GMenu.menu_item (GtkMenu.MenuItem.cast
+        (Glade.get_widget_msg ~name:"NewDefsMenuItem" ~info:"GtkMenuItem" xmldata))
+    method newDefsMenuItem = newDefsMenuItem
+    val openMenuItem =
+      new GMenu.image_menu_item (GtkMenu.ImageMenuItem.cast
+        (Glade.get_widget_msg ~name:"OpenMenuItem" ~info:"GtkImageMenuItem" xmldata))
+    method openMenuItem = openMenuItem
+    val image225 =
+      new GMisc.image (GtkMisc.Image.cast
+        (Glade.get_widget_msg ~name:"image225" ~info:"GtkImage" xmldata))
+    method image225 = image225
+    val saveMenuItem =
+      new GMenu.image_menu_item (GtkMenu.ImageMenuItem.cast
+        (Glade.get_widget_msg ~name:"SaveMenuItem" ~info:"GtkImageMenuItem" xmldata))
+    method saveMenuItem = saveMenuItem
+    val image226 =
+      new GMisc.image (GtkMisc.Image.cast
+        (Glade.get_widget_msg ~name:"image226" ~info:"GtkImage" xmldata))
+    method image226 = image226
+    val saveAsMenuItem =
+      new GMenu.image_menu_item (GtkMenu.ImageMenuItem.cast
+        (Glade.get_widget_msg ~name:"SaveAsMenuItem" ~info:"GtkImageMenuItem" xmldata))
+    method saveAsMenuItem = saveAsMenuItem
+    val image227 =
+      new GMisc.image (GtkMisc.Image.cast
+        (Glade.get_widget_msg ~name:"image227" ~info:"GtkImage" xmldata))
+    method image227 = image227
+    val separator1 =
+      new GMenu.menu_item (GtkMenu.MenuItem.cast
+        (Glade.get_widget_msg ~name:"separator1" ~info:"GtkSeparatorMenuItem" xmldata))
+    method separator1 = separator1
+    val quitMenuItem =
+      new GMenu.image_menu_item (GtkMenu.ImageMenuItem.cast
+        (Glade.get_widget_msg ~name:"QuitMenuItem" ~info:"GtkImageMenuItem" xmldata))
+    method quitMenuItem = quitMenuItem
+    val image228 =
+      new GMisc.image (GtkMisc.Image.cast
+        (Glade.get_widget_msg ~name:"image228" ~info:"GtkImage" xmldata))
+    method image228 = image228
+    val editMenu =
+      new GMenu.menu_item (GtkMenu.MenuItem.cast
+        (Glade.get_widget_msg ~name:"EditMenu" ~info:"GtkMenuItem" xmldata))
+    method editMenu = editMenu
+    val viewMenu =
+      new GMenu.menu_item (GtkMenu.MenuItem.cast
+        (Glade.get_widget_msg ~name:"ViewMenu" ~info:"GtkMenuItem" xmldata))
+    method viewMenu = viewMenu
+    val viewMenu_menu =
+      new GMenu.menu (GtkMenu.Menu.cast
+        (Glade.get_widget_msg ~name:"ViewMenu_menu" ~info:"GtkMenu" xmldata))
+    method viewMenu_menu = viewMenu_menu
+    val showToolBarMenuItem =
+      new GMenu.check_menu_item (GtkMenu.CheckMenuItem.cast
+        (Glade.get_widget_msg ~name:"ShowToolBarMenuItem" ~info:"GtkCheckMenuItem" xmldata))
+    method showToolBarMenuItem = showToolBarMenuItem
+    val newCicBrowserMenuItem =
+      new GMenu.menu_item (GtkMenu.MenuItem.cast
+        (Glade.get_widget_msg ~name:"NewCicBrowserMenuItem" ~info:"GtkMenuItem" xmldata))
+    method newCicBrowserMenuItem = newCicBrowserMenuItem
+    val showScriptMenuItem =
+      new GMenu.check_menu_item (GtkMenu.CheckMenuItem.cast
+        (Glade.get_widget_msg ~name:"ShowScriptMenuItem" ~info:"GtkCheckMenuItem" xmldata))
+    method showScriptMenuItem = showScriptMenuItem
+    val separator3 =
+      new GMenu.menu_item (GtkMenu.MenuItem.cast
+        (Glade.get_widget_msg ~name:"separator3" ~info:"GtkSeparatorMenuItem" xmldata))
+    method separator3 = separator3
+    val showConsoleMenuItem =
+      new GMenu.menu_item (GtkMenu.MenuItem.cast
+        (Glade.get_widget_msg ~name:"ShowConsoleMenuItem" ~info:"GtkMenuItem" xmldata))
+    method showConsoleMenuItem = showConsoleMenuItem
+    val debugMenu =
+      new GMenu.menu_item (GtkMenu.MenuItem.cast
+        (Glade.get_widget_msg ~name:"DebugMenu" ~info:"GtkMenuItem" xmldata))
+    method debugMenu = debugMenu
+    val debugMenu_menu =
+      new GMenu.menu (GtkMenu.Menu.cast
+        (Glade.get_widget_msg ~name:"DebugMenu_menu" ~info:"GtkMenu" xmldata))
+    method debugMenu_menu = debugMenu_menu
+    val separator2 =
+      new GMenu.menu_item (GtkMenu.MenuItem.cast
+        (Glade.get_widget_msg ~name:"separator2" ~info:"GtkSeparatorMenuItem" xmldata))
+    method separator2 = separator2
+    val helpMenu =
+      new GMenu.menu_item (GtkMenu.MenuItem.cast
+        (Glade.get_widget_msg ~name:"HelpMenu" ~info:"GtkMenuItem" xmldata))
+    method helpMenu = helpMenu
+    val helpMenu_menu =
+      new GMenu.menu (GtkMenu.Menu.cast
+        (Glade.get_widget_msg ~name:"HelpMenu_menu" ~info:"GtkMenu" xmldata))
+    method helpMenu_menu = helpMenu_menu
+    val aboutMenuItem =
+      new GMenu.menu_item (GtkMenu.MenuItem.cast
+        (Glade.get_widget_msg ~name:"AboutMenuItem" ~info:"GtkMenuItem" xmldata))
+    method aboutMenuItem = aboutMenuItem
+    val mainVPanes =
+      new GPack.paned (GtkPack.Paned.cast
+        (Glade.get_widget_msg ~name:"MainVPanes" ~info:"GtkVPaned" xmldata))
+    method mainVPanes = mainVPanes
+    val sequentsNotebook =
+      new GPack.notebook (GtkPack.Notebook.cast
+        (Glade.get_widget_msg ~name:"SequentsNotebook" ~info:"GtkNotebook" xmldata))
+    method sequentsNotebook = sequentsNotebook
+    val consoleEventBox =
+      new GBin.event_box (GtkBin.EventBox.cast
+        (Glade.get_widget_msg ~name:"ConsoleEventBox" ~info:"GtkEventBox" xmldata))
+    method consoleEventBox = consoleEventBox
+    val consoleHBox =
+      new GPack.box (GtkPack.Box.cast
+        (Glade.get_widget_msg ~name:"ConsoleHBox" ~info:"GtkHBox" xmldata))
+    method consoleHBox = consoleHBox
+    val vbox6 =
       new GPack.box (GtkPack.Box.cast
-        (Glade.get_widget_msg ~name:"EmptyDialogVBox" ~info:"GtkVBox" xmldata))
-    method emptyDialogVBox = emptyDialogVBox
-    val dialog_action_area5 =
-      new GPack.button_box (GtkPack.BBox.cast
-        (Glade.get_widget_msg ~name:"dialog-action_area5" ~info:"GtkHButtonBox" xmldata))
-    method dialog_action_area5 = dialog_action_area5
-    val emptyDialogCancelButton =
-      new GButton.button (GtkButton.Button.cast
-        (Glade.get_widget_msg ~name:"EmptyDialogCancelButton" ~info:"GtkButton" xmldata))
-    method emptyDialogCancelButton = emptyDialogCancelButton
-    val emptyDialogOkButton =
+        (Glade.get_widget_msg ~name:"vbox6" ~info:"GtkVBox" xmldata))
+    method vbox6 = vbox6
+    val hideConsoleButton =
       new GButton.button (GtkButton.Button.cast
-        (Glade.get_widget_msg ~name:"EmptyDialogOkButton" ~info:"GtkButton" xmldata))
-    method emptyDialogOkButton = emptyDialogOkButton
-    val emptyDialogLabel =
-      new GMisc.label (GtkMisc.Label.cast
-        (Glade.get_widget_msg ~name:"EmptyDialogLabel" ~info:"GtkLabel" xmldata))
-    method emptyDialogLabel = emptyDialogLabel
-    method reparent parent =
-      emptyDialogVBox#misc#reparent parent;
-      toplevel#destroy ()
-    method check_widgets () = ()
-  end
-class checkWin ?(file="matita.glade") ?domain ?autoconnect(*=true*) () =
-  let xmldata = Glade.create ~file  ~root:"CheckWin" ?domain () in
-  object (self)
-    inherit Glade.xml ?autoconnect xmldata
-    val toplevel =
-      new GWindow.window (GtkWindow.Window.cast
-        (Glade.get_widget_msg ~name:"CheckWin" ~info:"GtkWindow" xmldata))
-    method toplevel = toplevel
-    val checkWin =
-      new GWindow.window (GtkWindow.Window.cast
-        (Glade.get_widget_msg ~name:"CheckWin" ~info:"GtkWindow" xmldata))
-    method checkWin = checkWin
-    val checkWinEventBox =
-      new GBin.event_box (GtkBin.EventBox.cast
-        (Glade.get_widget_msg ~name:"CheckWinEventBox" ~info:"GtkEventBox" xmldata))
-    method checkWinEventBox = checkWinEventBox
-    val scrolledCheck =
+        (Glade.get_widget_msg ~name:"HideConsoleButton" ~info:"GtkButton" xmldata))
+    method hideConsoleButton = hideConsoleButton
+    val image169 =
+      new GMisc.image (GtkMisc.Image.cast
+        (Glade.get_widget_msg ~name:"image169" ~info:"GtkImage" xmldata))
+    method image169 = image169
+    val scrolledConsole =
       new GBin.scrolled_window (GtkBin.ScrolledWindow.cast
-        (Glade.get_widget_msg ~name:"ScrolledCheck" ~info:"GtkScrolledWindow" xmldata))
-    method scrolledCheck = scrolledCheck
+        (Glade.get_widget_msg ~name:"ScrolledConsole" ~info:"GtkScrolledWindow" xmldata))
+    method scrolledConsole = scrolledConsole
+    val mainStatusBar =
+      new GMisc.statusbar (GtkMisc.Statusbar.cast
+        (Glade.get_widget_msg ~name:"MainStatusBar" ~info:"GtkStatusbar" xmldata))
+    method mainStatusBar = mainStatusBar
     method reparent parent =
-      checkWinEventBox#misc#reparent parent;
+      mainWinEventBox#misc#reparent parent;
       toplevel#destroy ()
     method check_widgets () = ()
   end
@@ -663,26 +484,34 @@ class scriptWin ?(file="matita.glade") ?domain ?autoconnect(*=true*) () =
       new GBin.event_box (GtkBin.EventBox.cast
         (Glade.get_widget_msg ~name:"ScriptWinEventBox" ~info:"GtkEventBox" xmldata))
     method scriptWinEventBox = scriptWinEventBox
-    val scriptNotebook =
-      new GPack.notebook (GtkPack.Notebook.cast
-        (Glade.get_widget_msg ~name:"scriptNotebook" ~info:"GtkNotebook" xmldata))
-    method scriptNotebook = scriptNotebook
-    val vbox4 =
+    val vbox7 =
       new GPack.box (GtkPack.Box.cast
-        (Glade.get_widget_msg ~name:"vbox4" ~info:"GtkVBox" xmldata))
-    method vbox4 = vbox4
-    val toolbar1 =
-      new GButton.toolbar (GtkButton.Toolbar.cast
-        (Glade.get_widget_msg ~name:"toolbar1" ~info:"GtkToolbar" xmldata))
-    method toolbar1 = toolbar1
+        (Glade.get_widget_msg ~name:"vbox7" ~info:"GtkVBox" xmldata))
+    method vbox7 = vbox7
+    val handlebox2 =
+      new GBin.handle_box (GtkBin.HandleBox.cast
+        (Glade.get_widget_msg ~name:"handlebox2" ~info:"GtkHandleBox" xmldata))
+    method handlebox2 = handlebox2
+    val hbox8 =
+      new GPack.box (GtkPack.Box.cast
+        (Glade.get_widget_msg ~name:"hbox8" ~info:"GtkHBox" xmldata))
+    method hbox8 = hbox8
+    val scriptWinTopButton =
+      new GButton.button (GtkButton.Button.cast
+        (Glade.get_widget_msg ~name:"ScriptWinTopButton" ~info:"GtkButton" xmldata))
+    method scriptWinTopButton = scriptWinTopButton
+    val image235 =
+      new GMisc.image (GtkMisc.Image.cast
+        (Glade.get_widget_msg ~name:"image235" ~info:"GtkImage" xmldata))
+    method image235 = image235
     val scriptWinBackButton =
       new GButton.button (GtkButton.Button.cast
         (Glade.get_widget_msg ~name:"ScriptWinBackButton" ~info:"GtkButton" xmldata))
     method scriptWinBackButton = scriptWinBackButton
-    val image133 =
+    val image237 =
       new GMisc.image (GtkMisc.Image.cast
-        (Glade.get_widget_msg ~name:"image133" ~info:"GtkImage" xmldata))
-    method image133 = image133
+        (Glade.get_widget_msg ~name:"image237" ~info:"GtkImage" xmldata))
+    method image237 = image237
     val scriptWinJumpButton =
       new GButton.button (GtkButton.Button.cast
         (Glade.get_widget_msg ~name:"ScriptWinJumpButton" ~info:"GtkButton" xmldata))
@@ -695,10 +524,22 @@ class scriptWin ?(file="matita.glade") ?domain ?autoconnect(*=true*) () =
       new GButton.button (GtkButton.Button.cast
         (Glade.get_widget_msg ~name:"ScriptWinForwardButton" ~info:"GtkButton" xmldata))
     method scriptWinForwardButton = scriptWinForwardButton
-    val image135 =
+    val image239 =
+      new GMisc.image (GtkMisc.Image.cast
+        (Glade.get_widget_msg ~name:"image239" ~info:"GtkImage" xmldata))
+    method image239 = image239
+    val scriptWinBottomButton =
+      new GButton.button (GtkButton.Button.cast
+        (Glade.get_widget_msg ~name:"ScriptWinBottomButton" ~info:"GtkButton" xmldata))
+    method scriptWinBottomButton = scriptWinBottomButton
+    val image238 =
       new GMisc.image (GtkMisc.Image.cast
-        (Glade.get_widget_msg ~name:"image135" ~info:"GtkImage" xmldata))
-    method image135 = image135
+        (Glade.get_widget_msg ~name:"image238" ~info:"GtkImage" xmldata))
+    method image238 = image238
+    val scriptNotebook =
+      new GPack.notebook (GtkPack.Notebook.cast
+        (Glade.get_widget_msg ~name:"ScriptNotebook" ~info:"GtkNotebook" xmldata))
+    method scriptNotebook = scriptNotebook
     val scrolledScript =
       new GBin.scrolled_window (GtkBin.ScrolledWindow.cast
         (Glade.get_widget_msg ~name:"ScrolledScript" ~info:"GtkScrolledWindow" xmldata))
@@ -711,206 +552,333 @@ class scriptWin ?(file="matita.glade") ?domain ?autoconnect(*=true*) () =
       new GMisc.label (GtkMisc.Label.cast
         (Glade.get_widget_msg ~name:"label7" ~info:"GtkLabel" xmldata))
     method label7 = label7
-    val scrolledwindow3 =
+    val scrolledOutline =
       new GBin.scrolled_window (GtkBin.ScrolledWindow.cast
-        (Glade.get_widget_msg ~name:"scrolledwindow3" ~info:"GtkScrolledWindow" xmldata))
-    method scrolledwindow3 = scrolledwindow3
-    val treeview1 =
+        (Glade.get_widget_msg ~name:"ScrolledOutline" ~info:"GtkScrolledWindow" xmldata))
+    method scrolledOutline = scrolledOutline
+    val outlineTreeView =
       new GTree.view (GtkTree.TreeView.cast
-        (Glade.get_widget_msg ~name:"treeview1" ~info:"GtkTreeView" xmldata))
-    method treeview1 = treeview1
+        (Glade.get_widget_msg ~name:"OutlineTreeView" ~info:"GtkTreeView" xmldata))
+    method outlineTreeView = outlineTreeView
     val label8 =
       new GMisc.label (GtkMisc.Label.cast
         (Glade.get_widget_msg ~name:"label8" ~info:"GtkLabel" xmldata))
     method label8 = label8
     method reparent parent =
-      scriptWinEventBox#misc#reparent parent;
+      scriptWinEventBox#misc#reparent parent;
+      toplevel#destroy ()
+    method check_widgets () = ()
+  end
+class textDialog ?(file="matita.glade") ?domain ?autoconnect(*=true*) () =
+  let xmldata = Glade.create ~file  ~root:"TextDialog" ?domain () in
+  object (self)
+    inherit Glade.xml ?autoconnect xmldata
+    val toplevel =
+      new GWindow.dialog_any (GtkWindow.Dialog.cast
+        (Glade.get_widget_msg ~name:"TextDialog" ~info:"GtkDialog" xmldata))
+    method toplevel = toplevel
+    val textDialog =
+      new GWindow.dialog_any (GtkWindow.Dialog.cast
+        (Glade.get_widget_msg ~name:"TextDialog" ~info:"GtkDialog" xmldata))
+    method textDialog = textDialog
+    val vbox5 =
+      new GPack.box (GtkPack.Box.cast
+        (Glade.get_widget_msg ~name:"vbox5" ~info:"GtkVBox" xmldata))
+    method vbox5 = vbox5
+    val hbuttonbox1 =
+      new GPack.button_box (GtkPack.BBox.cast
+        (Glade.get_widget_msg ~name:"hbuttonbox1" ~info:"GtkHButtonBox" xmldata))
+    method hbuttonbox1 = hbuttonbox1
+    val textDialogCancelButton =
+      new GButton.button (GtkButton.Button.cast
+        (Glade.get_widget_msg ~name:"TextDialogCancelButton" ~info:"GtkButton" xmldata))
+    method textDialogCancelButton = textDialogCancelButton
+    val textDialogOkButton =
+      new GButton.button (GtkButton.Button.cast
+        (Glade.get_widget_msg ~name:"TextDialogOkButton" ~info:"GtkButton" xmldata))
+    method textDialogOkButton = textDialogOkButton
+    val textDialogLabel =
+      new GMisc.label (GtkMisc.Label.cast
+        (Glade.get_widget_msg ~name:"TextDialogLabel" ~info:"GtkLabel" xmldata))
+    method textDialogLabel = textDialogLabel
+    val scrolledwindow2 =
+      new GBin.scrolled_window (GtkBin.ScrolledWindow.cast
+        (Glade.get_widget_msg ~name:"scrolledwindow2" ~info:"GtkScrolledWindow" xmldata))
+    method scrolledwindow2 = scrolledwindow2
+    val textDialogTextView =
+      new GText.view (GtkText.View.cast
+        (Glade.get_widget_msg ~name:"TextDialogTextView" ~info:"GtkTextView" xmldata))
+    method textDialogTextView = textDialogTextView
+    method reparent parent =
+      vbox5#misc#reparent parent;
+      toplevel#destroy ()
+    method check_widgets () = ()
+  end
+class toolBarWin ?(file="matita.glade") ?domain ?autoconnect(*=true*) () =
+  let xmldata = Glade.create ~file  ~root:"ToolBarWin" ?domain () in
+  object (self)
+    inherit Glade.xml ?autoconnect xmldata
+    val toplevel =
+      new GWindow.window (GtkWindow.Window.cast
+        (Glade.get_widget_msg ~name:"ToolBarWin" ~info:"GtkWindow" xmldata))
+    method toplevel = toplevel
+    val toolBarWin =
+      new GWindow.window (GtkWindow.Window.cast
+        (Glade.get_widget_msg ~name:"ToolBarWin" ~info:"GtkWindow" xmldata))
+    method toolBarWin = toolBarWin
+    val toolBarEventBox =
+      new GBin.event_box (GtkBin.EventBox.cast
+        (Glade.get_widget_msg ~name:"ToolBarEventBox" ~info:"GtkEventBox" xmldata))
+    method toolBarEventBox = toolBarEventBox
+    val toolBarVBox =
+      new GPack.box (GtkPack.Box.cast
+        (Glade.get_widget_msg ~name:"ToolBarVBox" ~info:"GtkVBox" xmldata))
+    method toolBarVBox = toolBarVBox
+    val toolbar2 =
+      new GButton.toolbar (GtkButton.Toolbar.cast
+        (Glade.get_widget_msg ~name:"toolbar2" ~info:"GtkToolbar" xmldata))
+    method toolbar2 = toolbar2
+    val introsButton =
+      new GButton.button (GtkButton.Button.cast
+        (Glade.get_widget_msg ~name:"introsButton" ~info:"GtkButton" xmldata))
+    method introsButton = introsButton
+    val applyButton =
+      new GButton.button (GtkButton.Button.cast
+        (Glade.get_widget_msg ~name:"applyButton" ~info:"GtkButton" xmldata))
+    method applyButton = applyButton
+    val exactButton =
+      new GButton.button (GtkButton.Button.cast
+        (Glade.get_widget_msg ~name:"exactButton" ~info:"GtkButton" xmldata))
+    method exactButton = exactButton
+    val toolbar3 =
+      new GButton.toolbar (GtkButton.Toolbar.cast
+        (Glade.get_widget_msg ~name:"toolbar3" ~info:"GtkToolbar" xmldata))
+    method toolbar3 = toolbar3
+    val elimButton =
+      new GButton.button (GtkButton.Button.cast
+        (Glade.get_widget_msg ~name:"elimButton" ~info:"GtkButton" xmldata))
+    method elimButton = elimButton
+    val elimTypeButton =
+      new GButton.button (GtkButton.Button.cast
+        (Glade.get_widget_msg ~name:"elimTypeButton" ~info:"GtkButton" xmldata))
+    method elimTypeButton = elimTypeButton
+    val toolbar4 =
+      new GButton.toolbar (GtkButton.Toolbar.cast
+        (Glade.get_widget_msg ~name:"toolbar4" ~info:"GtkToolbar" xmldata))
+    method toolbar4 = toolbar4
+    val splitButton =
+      new GButton.button (GtkButton.Button.cast
+        (Glade.get_widget_msg ~name:"splitButton" ~info:"GtkButton" xmldata))
+    method splitButton = splitButton
+    val leftButton =
+      new GButton.button (GtkButton.Button.cast
+        (Glade.get_widget_msg ~name:"leftButton" ~info:"GtkButton" xmldata))
+    method leftButton = leftButton
+    val rightButton =
+      new GButton.button (GtkButton.Button.cast
+        (Glade.get_widget_msg ~name:"rightButton" ~info:"GtkButton" xmldata))
+    method rightButton = rightButton
+    val existsButton =
+      new GButton.button (GtkButton.Button.cast
+        (Glade.get_widget_msg ~name:"existsButton" ~info:"GtkButton" xmldata))
+    method existsButton = existsButton
+    val toolbar5 =
+      new GButton.toolbar (GtkButton.Toolbar.cast
+        (Glade.get_widget_msg ~name:"toolbar5" ~info:"GtkToolbar" xmldata))
+    method toolbar5 = toolbar5
+    val reflexivityButton =
+      new GButton.button (GtkButton.Button.cast
+        (Glade.get_widget_msg ~name:"reflexivityButton" ~info:"GtkButton" xmldata))
+    method reflexivityButton = reflexivityButton
+    val symmetryButton =
+      new GButton.button (GtkButton.Button.cast
+        (Glade.get_widget_msg ~name:"symmetryButton" ~info:"GtkButton" xmldata))
+    method symmetryButton = symmetryButton
+    val transitivityButton =
+      new GButton.button (GtkButton.Button.cast
+        (Glade.get_widget_msg ~name:"transitivityButton" ~info:"GtkButton" xmldata))
+    method transitivityButton = transitivityButton
+    val toolbar8 =
+      new GButton.toolbar (GtkButton.Toolbar.cast
+        (Glade.get_widget_msg ~name:"toolbar8" ~info:"GtkToolbar" xmldata))
+    method toolbar8 = toolbar8
+    val simplifyButton =
+      new GButton.button (GtkButton.Button.cast
+        (Glade.get_widget_msg ~name:"simplifyButton" ~info:"GtkButton" xmldata))
+    method simplifyButton = simplifyButton
+    val reduceButton =
+      new GButton.button (GtkButton.Button.cast
+        (Glade.get_widget_msg ~name:"reduceButton" ~info:"GtkButton" xmldata))
+    method reduceButton = reduceButton
+    val whdButton =
+      new GButton.button (GtkButton.Button.cast
+        (Glade.get_widget_msg ~name:"whdButton" ~info:"GtkButton" xmldata))
+    method whdButton = whdButton
+    val toolbar6 =
+      new GButton.toolbar (GtkButton.Toolbar.cast
+        (Glade.get_widget_msg ~name:"toolbar6" ~info:"GtkToolbar" xmldata))
+    method toolbar6 = toolbar6
+    val assumptionButton =
+      new GButton.button (GtkButton.Button.cast
+        (Glade.get_widget_msg ~name:"assumptionButton" ~info:"GtkButton" xmldata))
+    method assumptionButton = assumptionButton
+    val autoButton =
+      new GButton.button (GtkButton.Button.cast
+        (Glade.get_widget_msg ~name:"autoButton" ~info:"GtkButton" xmldata))
+    method autoButton = autoButton
+    val toolbar7 =
+      new GButton.toolbar (GtkButton.Toolbar.cast
+        (Glade.get_widget_msg ~name:"toolbar7" ~info:"GtkToolbar" xmldata))
+    method toolbar7 = toolbar7
+    val cutButton =
+      new GButton.button (GtkButton.Button.cast
+        (Glade.get_widget_msg ~name:"cutButton" ~info:"GtkButton" xmldata))
+    method cutButton = cutButton
+    val replaceButton =
+      new GButton.button (GtkButton.Button.cast
+        (Glade.get_widget_msg ~name:"replaceButton" ~info:"GtkButton" xmldata))
+    method replaceButton = replaceButton
+    method reparent parent =
+      toolBarEventBox#misc#reparent parent;
       toplevel#destroy ()
     method check_widgets () = ()
   end
-class textDialog ?(file="matita.glade") ?domain ?autoconnect(*=true*) () =
-  let xmldata = Glade.create ~file  ~root:"TextDialog" ?domain () in
+class uriChoiceDialog ?(file="matita.glade") ?domain ?autoconnect(*=true*) () =
+  let xmldata = Glade.create ~file  ~root:"UriChoiceDialog" ?domain () in
   object (self)
     inherit Glade.xml ?autoconnect xmldata
     val toplevel =
       new GWindow.dialog_any (GtkWindow.Dialog.cast
-        (Glade.get_widget_msg ~name:"TextDialog" ~info:"GtkDialog" xmldata))
+        (Glade.get_widget_msg ~name:"UriChoiceDialog" ~info:"GtkDialog" xmldata))
     method toplevel = toplevel
-    val textDialog =
+    val uriChoiceDialog =
       new GWindow.dialog_any (GtkWindow.Dialog.cast
-        (Glade.get_widget_msg ~name:"TextDialog" ~info:"GtkDialog" xmldata))
-    method textDialog = textDialog
-    val vbox5 =
+        (Glade.get_widget_msg ~name:"UriChoiceDialog" ~info:"GtkDialog" xmldata))
+    method uriChoiceDialog = uriChoiceDialog
+    val dialog_vbox3 =
       new GPack.box (GtkPack.Box.cast
-        (Glade.get_widget_msg ~name:"vbox5" ~info:"GtkVBox" xmldata))
-    method vbox5 = vbox5
-    val hbuttonbox1 =
+        (Glade.get_widget_msg ~name:"dialog-vbox3" ~info:"GtkVBox" xmldata))
+    method dialog_vbox3 = dialog_vbox3
+    val dialog_action_area3 =
       new GPack.button_box (GtkPack.BBox.cast
-        (Glade.get_widget_msg ~name:"hbuttonbox1" ~info:"GtkHButtonBox" xmldata))
-    method hbuttonbox1 = hbuttonbox1
-    val textDialogCancelButton =
-      new GButton.button (GtkButton.Button.cast
-        (Glade.get_widget_msg ~name:"TextDialogCancelButton" ~info:"GtkButton" xmldata))
-    method textDialogCancelButton = textDialogCancelButton
-    val textDialogOkButton =
-      new GButton.button (GtkButton.Button.cast
-        (Glade.get_widget_msg ~name:"TextDialogOkButton" ~info:"GtkButton" xmldata))
-    method textDialogOkButton = textDialogOkButton
-    val textDialogLabel =
-      new GMisc.label (GtkMisc.Label.cast
-        (Glade.get_widget_msg ~name:"TextDialogLabel" ~info:"GtkLabel" xmldata))
-    method textDialogLabel = textDialogLabel
-    val scrolledwindow2 =
-      new GBin.scrolled_window (GtkBin.ScrolledWindow.cast
-        (Glade.get_widget_msg ~name:"scrolledwindow2" ~info:"GtkScrolledWindow" xmldata))
-    method scrolledwindow2 = scrolledwindow2
-    val textDialogTextView =
-      new GText.view (GtkText.View.cast
-        (Glade.get_widget_msg ~name:"TextDialogTextView" ~info:"GtkTextView" xmldata))
-    method textDialogTextView = textDialogTextView
-    method reparent parent =
-      vbox5#misc#reparent parent;
-      toplevel#destroy ()
-    method check_widgets () = ()
-  end
-class browserWin ?(file="matita.glade") ?domain ?autoconnect(*=true*) () =
-  let xmldata = Glade.create ~file  ~root:"BrowserWin" ?domain () in
-  object (self)
-    inherit Glade.xml ?autoconnect xmldata
-    val toplevel =
-      new GWindow.window (GtkWindow.Window.cast
-        (Glade.get_widget_msg ~name:"BrowserWin" ~info:"GtkWindow" xmldata))
-    method toplevel = toplevel
-    val browserWin =
-      new GWindow.window (GtkWindow.Window.cast
-        (Glade.get_widget_msg ~name:"BrowserWin" ~info:"GtkWindow" xmldata))
-    method browserWin = browserWin
-    val browserWinEventBox =
-      new GBin.event_box (GtkBin.EventBox.cast
-        (Glade.get_widget_msg ~name:"BrowserWinEventBox" ~info:"GtkEventBox" xmldata))
-    method browserWinEventBox = browserWinEventBox
-    val browserVBox =
-      new GPack.box (GtkPack.Box.cast
-        (Glade.get_widget_msg ~name:"BrowserVBox" ~info:"GtkVBox" xmldata))
-    method browserVBox = browserVBox
-    val hbox7 =
-      new GPack.box (GtkPack.Box.cast
-        (Glade.get_widget_msg ~name:"hbox7" ~info:"GtkHBox" xmldata))
-    method hbox7 = hbox7
-    val browserNewButton =
+        (Glade.get_widget_msg ~name:"dialog-action_area3" ~info:"GtkHButtonBox" xmldata))
+    method dialog_action_area3 = dialog_action_area3
+    val uriChoiceAbortButton =
       new GButton.button (GtkButton.Button.cast
-        (Glade.get_widget_msg ~name:"BrowserNewButton" ~info:"GtkButton" xmldata))
-    method browserNewButton = browserNewButton
-    val image191 =
-      new GMisc.image (GtkMisc.Image.cast
-        (Glade.get_widget_msg ~name:"image191" ~info:"GtkImage" xmldata))
-    method image191 = image191
-    val browserBackButton =
+        (Glade.get_widget_msg ~name:"UriChoiceAbortButton" ~info:"GtkButton" xmldata))
+    method uriChoiceAbortButton = uriChoiceAbortButton
+    val uriChoiceSelectedButton =
       new GButton.button (GtkButton.Button.cast
-        (Glade.get_widget_msg ~name:"BrowserBackButton" ~info:"GtkButton" xmldata))
-    method browserBackButton = browserBackButton
-    val alignment3 =
+        (Glade.get_widget_msg ~name:"UriChoiceSelectedButton" ~info:"GtkButton" xmldata))
+    method uriChoiceSelectedButton = uriChoiceSelectedButton
+    val alignment2 =
       new GBin.alignment (GtkBin.Alignment.cast
-        (Glade.get_widget_msg ~name:"alignment3" ~info:"GtkAlignment" xmldata))
-    method alignment3 = alignment3
-    val hbox6 =
+        (Glade.get_widget_msg ~name:"alignment2" ~info:"GtkAlignment" xmldata))
+    method alignment2 = alignment2
+    val hbox3 =
       new GPack.box (GtkPack.Box.cast
-        (Glade.get_widget_msg ~name:"hbox6" ~info:"GtkHBox" xmldata))
-    method hbox6 = hbox6
-    val image188 =
+        (Glade.get_widget_msg ~name:"hbox3" ~info:"GtkHBox" xmldata))
+    method hbox3 = hbox3
+    val image19 =
       new GMisc.image (GtkMisc.Image.cast
-        (Glade.get_widget_msg ~name:"image188" ~info:"GtkImage" xmldata))
-    method image188 = image188
-    val label10 =
+        (Glade.get_widget_msg ~name:"image19" ~info:"GtkImage" xmldata))
+    method image19 = image19
+    val label3 =
       new GMisc.label (GtkMisc.Label.cast
-        (Glade.get_widget_msg ~name:"label10" ~info:"GtkLabel" xmldata))
-    method label10 = label10
-    val browserForwardButton =
-      new GButton.button (GtkButton.Button.cast
-        (Glade.get_widget_msg ~name:"BrowserForwardButton" ~info:"GtkButton" xmldata))
-    method browserForwardButton = browserForwardButton
-    val image189 =
-      new GMisc.image (GtkMisc.Image.cast
-        (Glade.get_widget_msg ~name:"image189" ~info:"GtkImage" xmldata))
-    method image189 = image189
-    val browserRefreshButton =
+        (Glade.get_widget_msg ~name:"label3" ~info:"GtkLabel" xmldata))
+    method label3 = label3
+    val uriChoiceConstantsButton =
       new GButton.button (GtkButton.Button.cast
-        (Glade.get_widget_msg ~name:"BrowserRefreshButton" ~info:"GtkButton" xmldata))
-    method browserRefreshButton = browserRefreshButton
-    val image229 =
-      new GMisc.image (GtkMisc.Image.cast
-        (Glade.get_widget_msg ~name:"image229" ~info:"GtkImage" xmldata))
-    method image229 = image229
-    val browserHomeButton =
+        (Glade.get_widget_msg ~name:"UriChoiceConstantsButton" ~info:"GtkButton" xmldata))
+    method uriChoiceConstantsButton = uriChoiceConstantsButton
+    val uriChoiceAutoButton =
       new GButton.button (GtkButton.Button.cast
-        (Glade.get_widget_msg ~name:"BrowserHomeButton" ~info:"GtkButton" xmldata))
-    method browserHomeButton = browserHomeButton
-    val image190 =
-      new GMisc.image (GtkMisc.Image.cast
-        (Glade.get_widget_msg ~name:"image190" ~info:"GtkImage" xmldata))
-    method image190 = image190
-    val image187 =
+        (Glade.get_widget_msg ~name:"UriChoiceAutoButton" ~info:"GtkButton" xmldata))
+    method uriChoiceAutoButton = uriChoiceAutoButton
+    val alignment1 =
+      new GBin.alignment (GtkBin.Alignment.cast
+        (Glade.get_widget_msg ~name:"alignment1" ~info:"GtkAlignment" xmldata))
+    method alignment1 = alignment1
+    val hbox1 =
+      new GPack.box (GtkPack.Box.cast
+        (Glade.get_widget_msg ~name:"hbox1" ~info:"GtkHBox" xmldata))
+    method hbox1 = hbox1
+    val image18 =
       new GMisc.image (GtkMisc.Image.cast
-        (Glade.get_widget_msg ~name:"image187" ~info:"GtkImage" xmldata))
-    method image187 = image187
-    val browserUri =
-      new GEdit.entry (GtkEdit.Entry.cast
-        (Glade.get_widget_msg ~name:"BrowserUri" ~info:"GtkEntry" xmldata))
-    method browserUri = browserUri
-    val frame1 =
-      new GBin.frame (GtkBin.Frame.cast
-        (Glade.get_widget_msg ~name:"frame1" ~info:"GtkFrame" xmldata))
-    method frame1 = frame1
-    val scrolledBrowser =
+        (Glade.get_widget_msg ~name:"image18" ~info:"GtkImage" xmldata))
+    method image18 = image18
+    val label1 =
+      new GMisc.label (GtkMisc.Label.cast
+        (Glade.get_widget_msg ~name:"label1" ~info:"GtkLabel" xmldata))
+    method label1 = label1
+    val vbox2 =
+      new GPack.box (GtkPack.Box.cast
+        (Glade.get_widget_msg ~name:"vbox2" ~info:"GtkVBox" xmldata))
+    method vbox2 = vbox2
+    val uriChoiceLabel =
+      new GMisc.label (GtkMisc.Label.cast
+        (Glade.get_widget_msg ~name:"UriChoiceLabel" ~info:"GtkLabel" xmldata))
+    method uriChoiceLabel = uriChoiceLabel
+    val scrolledwindow1 =
       new GBin.scrolled_window (GtkBin.ScrolledWindow.cast
-        (Glade.get_widget_msg ~name:"ScrolledBrowser" ~info:"GtkScrolledWindow" xmldata))
-    method scrolledBrowser = scrolledBrowser
+        (Glade.get_widget_msg ~name:"scrolledwindow1" ~info:"GtkScrolledWindow" xmldata))
+    method scrolledwindow1 = scrolledwindow1
+    val uriChoiceTreeView =
+      new GTree.view (GtkTree.TreeView.cast
+        (Glade.get_widget_msg ~name:"UriChoiceTreeView" ~info:"GtkTreeView" xmldata))
+    method uriChoiceTreeView = uriChoiceTreeView
+    val hbox2 =
+      new GPack.box (GtkPack.Box.cast
+        (Glade.get_widget_msg ~name:"hbox2" ~info:"GtkHBox" xmldata))
+    method hbox2 = hbox2
+    val label2 =
+      new GMisc.label (GtkMisc.Label.cast
+        (Glade.get_widget_msg ~name:"label2" ~info:"GtkLabel" xmldata))
+    method label2 = label2
+    val entry1 =
+      new GEdit.entry (GtkEdit.Entry.cast
+        (Glade.get_widget_msg ~name:"entry1" ~info:"GtkEntry" xmldata))
+    method entry1 = entry1
     method reparent parent =
-      browserWinEventBox#misc#reparent parent;
+      dialog_vbox3#misc#reparent parent;
       toplevel#destroy ()
     method check_widgets () = ()
   end
 
 let check_all ?(show=false) () =
   ignore (GMain.Main.init ());
-  let browserWin = new browserWin () in
-  if show then browserWin#toplevel#show ();
-  browserWin#check_widgets ();
+  let uriChoiceDialog = new uriChoiceDialog () in
+  if show then uriChoiceDialog#toplevel#show ();
+  uriChoiceDialog#check_widgets ();
+  let toolBarWin = new toolBarWin () in
+  if show then toolBarWin#toplevel#show ();
+  toolBarWin#check_widgets ();
   let textDialog = new textDialog () in
   if show then textDialog#toplevel#show ();
   textDialog#check_widgets ();
   let scriptWin = new scriptWin () in
   if show then scriptWin#toplevel#show ();
   scriptWin#check_widgets ();
-  let checkWin = new checkWin () in
-  if show then checkWin#toplevel#show ();
-  checkWin#check_widgets ();
-  let emptyDialog = new emptyDialog () in
-  if show then emptyDialog#toplevel#show ();
-  emptyDialog#check_widgets ();
+  let mainWin = new mainWin () in
+  if show then mainWin#toplevel#show ();
+  mainWin#check_widgets ();
   let interpChoiceDialog = new interpChoiceDialog () in
   if show then interpChoiceDialog#toplevel#show ();
   interpChoiceDialog#check_widgets ();
-  let uriChoiceDialog = new uriChoiceDialog () in
-  if show then uriChoiceDialog#toplevel#show ();
-  uriChoiceDialog#check_widgets ();
-  let aboutWin = new aboutWin () in
-  if show then aboutWin#toplevel#show ();
-  aboutWin#check_widgets ();
-  let confirmationDialog = new confirmationDialog () in
-  if show then confirmationDialog#toplevel#show ();
-  confirmationDialog#check_widgets ();
-  let toolBarWin = new toolBarWin () in
-  if show then toolBarWin#toplevel#show ();
-  toolBarWin#check_widgets ();
   let fileSelectionWin = new fileSelectionWin () in
   if show then fileSelectionWin#toplevel#show ();
   fileSelectionWin#check_widgets ();
-  let proofWin = new proofWin () in
-  if show then proofWin#toplevel#show ();
-  proofWin#check_widgets ();
-  let mainWin = new mainWin () in
-  if show then mainWin#toplevel#show ();
-  mainWin#check_widgets ();
+  let emptyDialog = new emptyDialog () in
+  if show then emptyDialog#toplevel#show ();
+  emptyDialog#check_widgets ();
+  let confirmationDialog = new confirmationDialog () in
+  if show then confirmationDialog#toplevel#show ();
+  confirmationDialog#check_widgets ();
+  let browserWin = new browserWin () in
+  if show then browserWin#toplevel#show ();
+  browserWin#check_widgets ();
+  let aboutWin = new aboutWin () in
+  if show then aboutWin#toplevel#show ();
+  aboutWin#check_widgets ();
   if show then GMain.Main.main ()
 ;;