]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/matita/matitaGeneratedGui.ml
filled toolbar and implemented buttons behaviours
[helm.git] / helm / matita / matitaGeneratedGui.ml
index f912ef0f9c5bc92e3ff7bb2980194a6b165b069f..95ae9648ea7b90316454cc9f2fa3fbf9fed48947 100644 (file)
@@ -12,6 +12,10 @@ class mainWin ?(file="matita.glade") ?domain ?autoconnect(*=true*) () =
       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))
@@ -32,10 +36,10 @@ class mainWin ?(file="matita.glade") ?domain ?autoconnect(*=true*) () =
       new GMenu.image_menu_item (GtkMenu.ImageMenuItem.cast
         (Glade.get_widget_msg ~name:"NewMenu" ~info:"GtkImageMenuItem" xmldata))
     method newMenu = newMenu
-    val image40 =
+    val image128 =
       new GMisc.image (GtkMisc.Image.cast
-        (Glade.get_widget_msg ~name:"image40" ~info:"GtkImage" xmldata))
-    method image40 = image40
+        (Glade.get_widget_msg ~name:"image128" ~info:"GtkImage" xmldata))
+    method image128 = image128
     val newMenu_menu =
       new GMenu.menu (GtkMenu.Menu.cast
         (Glade.get_widget_msg ~name:"NewMenu_menu" ~info:"GtkMenu" xmldata))
@@ -52,38 +56,38 @@ class mainWin ?(file="matita.glade") ?domain ?autoconnect(*=true*) () =
       new GMenu.image_menu_item (GtkMenu.ImageMenuItem.cast
         (Glade.get_widget_msg ~name:"OpenMenuItem" ~info:"GtkImageMenuItem" xmldata))
     method openMenuItem = openMenuItem
-    val image41 =
+    val image129 =
       new GMisc.image (GtkMisc.Image.cast
-        (Glade.get_widget_msg ~name:"image41" ~info:"GtkImage" xmldata))
-    method image41 = image41
+        (Glade.get_widget_msg ~name:"image129" ~info:"GtkImage" xmldata))
+    method image129 = image129
     val saveMenuItem =
       new GMenu.image_menu_item (GtkMenu.ImageMenuItem.cast
         (Glade.get_widget_msg ~name:"SaveMenuItem" ~info:"GtkImageMenuItem" xmldata))
     method saveMenuItem = saveMenuItem
-    val image42 =
+    val image130 =
       new GMisc.image (GtkMisc.Image.cast
-        (Glade.get_widget_msg ~name:"image42" ~info:"GtkImage" xmldata))
-    method image42 = image42
+        (Glade.get_widget_msg ~name:"image130" ~info:"GtkImage" xmldata))
+    method image130 = image130
     val saveAsMenuItem =
       new GMenu.image_menu_item (GtkMenu.ImageMenuItem.cast
         (Glade.get_widget_msg ~name:"SaveAsMenuItem" ~info:"GtkImageMenuItem" xmldata))
     method saveAsMenuItem = saveAsMenuItem
-    val image43 =
+    val image131 =
       new GMisc.image (GtkMisc.Image.cast
-        (Glade.get_widget_msg ~name:"image43" ~info:"GtkImage" xmldata))
-    method image43 = image43
+        (Glade.get_widget_msg ~name:"image131" ~info:"GtkImage" xmldata))
+    method image131 = image131
     val separator1 =
       new GMenu.menu_item (GtkMenu.MenuItem.cast
-        (Glade.get_widget_msg ~name:"separator1" ~info:"GtkMenuItem" xmldata))
+        (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 image44 =
+    val image132 =
       new GMisc.image (GtkMisc.Image.cast
-        (Glade.get_widget_msg ~name:"image44" ~info:"GtkImage" xmldata))
-    method image44 = image44
+        (Glade.get_widget_msg ~name:"image132" ~info:"GtkImage" xmldata))
+    method image132 = image132
     val editMenu =
       new GMenu.menu_item (GtkMenu.MenuItem.cast
         (Glade.get_widget_msg ~name:"EditMenu" ~info:"GtkMenuItem" xmldata))
@@ -104,6 +108,14 @@ class mainWin ?(file="matita.glade") ?domain ?autoconnect(*=true*) () =
       new GMenu.check_menu_item (GtkMenu.CheckMenuItem.cast
         (Glade.get_widget_msg ~name:"ShowProofMenuItem" ~info:"GtkCheckMenuItem" xmldata))
     method showProofMenuItem = showProofMenuItem
+    val showCheckMenuItem =
+      new GMenu.check_menu_item (GtkMenu.CheckMenuItem.cast
+        (Glade.get_widget_msg ~name:"ShowCheckMenuItem" ~info:"GtkCheckMenuItem" xmldata))
+    method showCheckMenuItem = showCheckMenuItem
+    val showScriptMenuItem =
+      new GMenu.check_menu_item (GtkMenu.CheckMenuItem.cast
+        (Glade.get_widget_msg ~name:"ShowScriptMenuItem" ~info:"GtkCheckMenuItem" xmldata))
+    method showScriptMenuItem = showScriptMenuItem
     val debugMenu =
       new GMenu.menu_item (GtkMenu.MenuItem.cast
         (Glade.get_widget_msg ~name:"DebugMenu" ~info:"GtkMenuItem" xmldata))
@@ -112,18 +124,10 @@ class mainWin ?(file="matita.glade") ?domain ?autoconnect(*=true*) () =
       new GMenu.menu (GtkMenu.Menu.cast
         (Glade.get_widget_msg ~name:"DebugMenu_menu" ~info:"GtkMenu" xmldata))
     method debugMenu_menu = debugMenu_menu
-    val debugMenuItem0 =
-      new GMenu.menu_item (GtkMenu.MenuItem.cast
-        (Glade.get_widget_msg ~name:"DebugMenuItem0" ~info:"GtkMenuItem" xmldata))
-    method debugMenuItem0 = debugMenuItem0
-    val debugMenuItem1 =
-      new GMenu.menu_item (GtkMenu.MenuItem.cast
-        (Glade.get_widget_msg ~name:"DebugMenuItem1" ~info:"GtkMenuItem" xmldata))
-    method debugMenuItem1 = debugMenuItem1
-    val debugMenuItem2 =
+    val separator2 =
       new GMenu.menu_item (GtkMenu.MenuItem.cast
-        (Glade.get_widget_msg ~name:"DebugMenuItem2" ~info:"GtkMenuItem" xmldata))
-    method debugMenuItem2 = debugMenuItem2
+        (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))
@@ -140,20 +144,32 @@ class mainWin ?(file="matita.glade") ?domain ?autoconnect(*=true*) () =
       new GPack.paned (GtkPack.Paned.cast
         (Glade.get_widget_msg ~name:"MainVPanes" ~info:"GtkVPaned" xmldata))
     method mainVPanes = mainVPanes
-    val proofStatus =
+    val scrolledSequents =
       new GBin.scrolled_window (GtkBin.ScrolledWindow.cast
-        (Glade.get_widget_msg ~name:"ProofStatus" ~info:"GtkScrolledWindow" xmldata))
-    method proofStatus = proofStatus
-    val scrolledUserInput =
+        (Glade.get_widget_msg ~name:"ScrolledSequents" ~info:"GtkScrolledWindow" xmldata))
+    method scrolledSequents = scrolledSequents
+    val viewport1 =
+      new GBin.viewport (GtkBin.Viewport.cast
+        (Glade.get_widget_msg ~name:"viewport1" ~info:"GtkViewport" xmldata))
+    method viewport1 = viewport1
+    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 scrolledConsole =
       new GBin.scrolled_window (GtkBin.ScrolledWindow.cast
-        (Glade.get_widget_msg ~name:"ScrolledUserInput" ~info:"GtkScrolledWindow" xmldata))
-    method scrolledUserInput = scrolledUserInput
+        (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 =
-      mainWinShape#misc#reparent parent;
+      mainWinEventBox#misc#reparent parent;
       toplevel#destroy ()
     method check_widgets () = ()
   end
@@ -177,10 +193,6 @@ class proofWin ?(file="matita.glade") ?domain ?autoconnect(*=true*) () =
       new GBin.scrolled_window (GtkBin.ScrolledWindow.cast
         (Glade.get_widget_msg ~name:"ScrolledProof" ~info:"GtkScrolledWindow" xmldata))
     method scrolledProof = scrolledProof
-    val viewport1 =
-      new GBin.viewport (GtkBin.Viewport.cast
-        (Glade.get_widget_msg ~name:"viewport1" ~info:"GtkViewport" xmldata))
-    method viewport1 = viewport1
     method reparent parent =
       proofWinEventBox#misc#reparent parent;
       toplevel#destroy ()
@@ -198,14 +210,14 @@ class fileSelectionWin ?(file="matita.glade") ?domain ?autoconnect(*=true*) () =
       new GWindow.file_selection (GtkWindow.FileSelection.cast
         (Glade.get_widget_msg ~name:"FileSelectionWin" ~info:"GtkFileSelection" xmldata))
     method fileSelectionWin = fileSelectionWin
-    val cancel_button1 =
+    val fileSelCancelButton =
       new GButton.button (GtkButton.Button.cast
-        (Glade.get_widget_msg ~name:"cancel_button1" ~info:"GtkButton" xmldata))
-    method cancel_button1 = cancel_button1
-    val ok_button1 =
+        (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:"ok_button1" ~info:"GtkButton" xmldata))
-    method ok_button1 = ok_button1
+        (Glade.get_widget_msg ~name:"fileSelOkButton" ~info:"GtkButton" xmldata))
+    method fileSelOkButton = fileSelOkButton
     method check_widgets () = ()
   end
 class toolBarWin ?(file="matita.glade") ?domain ?autoconnect(*=true*) () =
@@ -224,55 +236,139 @@ class toolBarWin ?(file="matita.glade") ?domain ?autoconnect(*=true*) () =
       new GBin.event_box (GtkBin.EventBox.cast
         (Glade.get_widget_msg ~name:"ToolBarEventBox" ~info:"GtkEventBox" xmldata))
     method toolBarEventBox = toolBarEventBox
-    val vbox1 =
+    val toolBarVBox =
       new GPack.box (GtkPack.Box.cast
-        (Glade.get_widget_msg ~name:"vbox1" ~info:"GtkVBox" xmldata))
-    method vbox1 = vbox1
-    val button1 =
+        (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:"button1" ~info:"GtkButton" xmldata))
-    method button1 = button1
-    val button2 =
+        (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:"button2" ~info:"GtkButton" xmldata))
-    method button2 = button2
-    val button3 =
+        (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:"button3" ~info:"GtkButton" xmldata))
-    method button3 = button3
-    val button4 =
+        (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:"button4" ~info:"GtkButton" xmldata))
-    method button4 = button4
+        (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 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 searchButton =
+      new GButton.button (GtkButton.Button.cast
+        (Glade.get_widget_msg ~name:"searchButton" ~info:"GtkButton" xmldata))
+    method searchButton = searchButton
+    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 genericDialog ?(file="matita.glade") ?domain ?autoconnect(*=true*) () =
-  let xmldata = Glade.create ~file  ~root:"GenericDialog" ?domain () in
+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 : [`NONE | `DELETE_EVENT | `ID of int] GWindow.dialog =
-      new GWindow.dialog (GtkWindow.Dialog.cast
-        (Glade.get_widget_msg ~name:"GenericDialog" ~info:"GtkDialog" xmldata))
+    val toplevel =
+      new GWindow.dialog_any (GtkWindow.Dialog.cast
+        (Glade.get_widget_msg ~name:"ConfirmationDialog" ~info:"GtkDialog" xmldata))
     method toplevel = toplevel
-    val genericDialog : [`NONE | `DELETE_EVENT | `ID of int] GWindow.dialog =
-      new GWindow.dialog (GtkWindow.Dialog.cast
-        (Glade.get_widget_msg ~name:"GenericDialog" ~info:"GtkDialog" xmldata))
-    method genericDialog = genericDialog
+    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 cancelbutton1 =
+    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:"cancelbutton1" ~info:"GtkButton" xmldata))
-    method cancelbutton1 = cancelbutton1
-    val okbutton1 =
+        (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:"okbutton1" ~info:"GtkButton" xmldata))
-    method okbutton1 = okbutton1
+        (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 ()
@@ -282,22 +378,30 @@ class aboutWin ?(file="matita.glade") ?domain ?autoconnect(*=true*) () =
   let xmldata = Glade.create ~file  ~root:"AboutWin" ?domain () in
   object (self)
     inherit Glade.xml ?autoconnect xmldata
-    val toplevel : [`NONE | `DELETE_EVENT | `ID of int] GWindow.dialog =
-      new GWindow.dialog (GtkWindow.Dialog.cast
+    val toplevel =
+      new GWindow.dialog_any (GtkWindow.Dialog.cast
         (Glade.get_widget_msg ~name:"AboutWin" ~info:"GtkDialog" xmldata))
     method toplevel = toplevel
-    val aboutWin : [`NONE | `DELETE_EVENT | `ID of int] GWindow.dialog =
-      new GWindow.dialog (GtkWindow.Dialog.cast
+    val aboutWin =
+      new GWindow.dialog_any (GtkWindow.Dialog.cast
         (Glade.get_widget_msg ~name:"AboutWin" ~info:"GtkDialog" xmldata))
     method aboutWin = aboutWin
     val dialog_vbox2 =
       new GPack.box (GtkPack.Box.cast
         (Glade.get_widget_msg ~name:"dialog-vbox2" ~info:"GtkVBox" xmldata))
     method dialog_vbox2 = dialog_vbox2
+    val dialog_action_area2 =
+      new GPack.button_box (GtkPack.BBox.cast
+        (Glade.get_widget_msg ~name:"dialog-action_area2" ~info:"GtkHButtonBox" xmldata))
+    method dialog_action_area2 = dialog_action_area2
     val aboutDismissButton =
       new GButton.button (GtkButton.Button.cast
         (Glade.get_widget_msg ~name:"AboutDismissButton" ~info:"GtkButton" xmldata))
     method aboutDismissButton = aboutDismissButton
+    val aboutLabel =
+      new GMisc.label (GtkMisc.Label.cast
+        (Glade.get_widget_msg ~name:"AboutLabel" ~info:"GtkLabel" xmldata))
+    method aboutLabel = aboutLabel
     method reparent parent =
       dialog_vbox2#misc#reparent parent;
       toplevel#destroy ()
@@ -307,18 +411,22 @@ 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 : [`NONE | `DELETE_EVENT | `ID of int] GWindow.dialog =
-      new GWindow.dialog (GtkWindow.Dialog.cast
+    val toplevel =
+      new GWindow.dialog_any (GtkWindow.Dialog.cast
         (Glade.get_widget_msg ~name:"UriChoiceDialog" ~info:"GtkDialog" xmldata))
     method toplevel = toplevel
-    val uriChoiceDialog : [`NONE | `DELETE_EVENT | `ID of int] GWindow.dialog =
-      new GWindow.dialog (GtkWindow.Dialog.cast
+    val uriChoiceDialog =
+      new GWindow.dialog_any (GtkWindow.Dialog.cast
         (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:"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 =
       new GButton.button (GtkButton.Button.cast
         (Glade.get_widget_msg ~name:"UriChoiceAbortButton" ~info:"GtkButton" xmldata))
@@ -404,18 +512,22 @@ class interpChoiceDialog ?(file="matita.glade") ?domain ?autoconnect(*=true*) ()
   let xmldata = Glade.create ~file  ~root:"InterpChoiceDialog" ?domain () in
   object (self)
     inherit Glade.xml ?autoconnect xmldata
-    val toplevel : [`NONE | `DELETE_EVENT | `ID of int] GWindow.dialog =
-      new GWindow.dialog (GtkWindow.Dialog.cast
+    val toplevel =
+      new GWindow.dialog_any (GtkWindow.Dialog.cast
         (Glade.get_widget_msg ~name:"InterpChoiceDialog" ~info:"GtkDialog" xmldata))
     method toplevel = toplevel
-    val interpChoiceDialog : [`NONE | `DELETE_EVENT | `ID of int] GWindow.dialog =
-      new GWindow.dialog (GtkWindow.Dialog.cast
+    val interpChoiceDialog =
+      new GWindow.dialog_any (GtkWindow.Dialog.cast
         (Glade.get_widget_msg ~name:"InterpChoiceDialog" ~info:"GtkDialog" xmldata))
     method interpChoiceDialog = interpChoiceDialog
     val dialog_vbox4 =
       new GPack.box (GtkPack.Box.cast
         (Glade.get_widget_msg ~name:"dialog-vbox4" ~info:"GtkVBox" xmldata))
     method dialog_vbox4 = dialog_vbox4
+    val dialog_action_area4 =
+      new GPack.button_box (GtkPack.BBox.cast
+        (Glade.get_widget_msg ~name:"dialog-action_area4" ~info:"GtkHButtonBox" xmldata))
+    method dialog_action_area4 = dialog_action_area4
     val interpChoiceHelpButton =
       new GButton.button (GtkButton.Button.cast
         (Glade.get_widget_msg ~name:"InterpChoiceHelpButton" ~info:"GtkButton" xmldata))
@@ -441,41 +553,189 @@ class interpChoiceDialog ?(file="matita.glade") ?domain ?autoconnect(*=true*) ()
       toplevel#destroy ()
     method check_widgets () = ()
   end
-class debug ?(file="matita.glade") ?domain ?autoconnect(*=true*) () =
-  let xmldata = Glade.create ~file  ~root:"Debug" ?domain () in
+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 : [`NONE | `DELETE_EVENT | `ID of int] GWindow.dialog =
-      new GWindow.dialog (GtkWindow.Dialog.cast
-        (Glade.get_widget_msg ~name:"Debug" ~info:"GtkDialog" xmldata))
+    val toplevel =
+      new GWindow.dialog_any (GtkWindow.Dialog.cast
+        (Glade.get_widget_msg ~name:"EmptyDialog" ~info:"GtkDialog" xmldata))
     method toplevel = toplevel
-    val debug : [`NONE | `DELETE_EVENT | `ID of int] GWindow.dialog =
-      new GWindow.dialog (GtkWindow.Dialog.cast
-        (Glade.get_widget_msg ~name:"Debug" ~info:"GtkDialog" xmldata))
-    method debug = debug
-    val dialog_vbox5 =
+    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:"dialog-vbox5" ~info:"GtkVBox" xmldata))
-    method dialog_vbox5 = dialog_vbox5
-    val cancelbutton2 =
+        (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:"cancelbutton2" ~info:"GtkButton" xmldata))
-    method cancelbutton2 = cancelbutton2
-    val okbutton2 =
+        (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:"okbutton2" ~info:"GtkButton" xmldata))
-    method okbutton2 = okbutton2
+        (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 =
+      new GBin.scrolled_window (GtkBin.ScrolledWindow.cast
+        (Glade.get_widget_msg ~name:"ScrolledCheck" ~info:"GtkScrolledWindow" xmldata))
+    method scrolledCheck = scrolledCheck
+    method reparent parent =
+      checkWinEventBox#misc#reparent parent;
+      toplevel#destroy ()
+    method check_widgets () = ()
+  end
+class scriptWin ?(file="matita.glade") ?domain ?autoconnect(*=true*) () =
+  let xmldata = Glade.create ~file  ~root:"ScriptWin" ?domain () in
+  object (self)
+    inherit Glade.xml ?autoconnect xmldata
+    val toplevel =
+      new GWindow.window (GtkWindow.Window.cast
+        (Glade.get_widget_msg ~name:"ScriptWin" ~info:"GtkWindow" xmldata))
+    method toplevel = toplevel
+    val scriptWin =
+      new GWindow.window (GtkWindow.Window.cast
+        (Glade.get_widget_msg ~name:"ScriptWin" ~info:"GtkWindow" xmldata))
+    method scriptWin = scriptWin
+    val scriptWinEventBox =
+      new GBin.event_box (GtkBin.EventBox.cast
+        (Glade.get_widget_msg ~name:"ScriptWinEventBox" ~info:"GtkEventBox" xmldata))
+    method scriptWinEventBox = scriptWinEventBox
+    val vbox4 =
+      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
+    val button5 =
+      new GButton.button (GtkButton.Button.cast
+        (Glade.get_widget_msg ~name:"button5" ~info:"GtkButton" xmldata))
+    method button5 = button5
+    val image133 =
+      new GMisc.image (GtkMisc.Image.cast
+        (Glade.get_widget_msg ~name:"image133" ~info:"GtkImage" xmldata))
+    method image133 = image133
+    val button6 =
+      new GButton.button (GtkButton.Button.cast
+        (Glade.get_widget_msg ~name:"button6" ~info:"GtkButton" xmldata))
+    method button6 = button6
+    val image134 =
+      new GMisc.image (GtkMisc.Image.cast
+        (Glade.get_widget_msg ~name:"image134" ~info:"GtkImage" xmldata))
+    method image134 = image134
+    val button7 =
+      new GButton.button (GtkButton.Button.cast
+        (Glade.get_widget_msg ~name:"button7" ~info:"GtkButton" xmldata))
+    method button7 = button7
+    val image135 =
+      new GMisc.image (GtkMisc.Image.cast
+        (Glade.get_widget_msg ~name:"image135" ~info:"GtkImage" xmldata))
+    method image135 = image135
+    val scrolledScript =
+      new GBin.scrolled_window (GtkBin.ScrolledWindow.cast
+        (Glade.get_widget_msg ~name:"ScrolledScript" ~info:"GtkScrolledWindow" xmldata))
+    method scrolledScript = scrolledScript
+    val scriptTextView =
+      new GText.view (GtkText.View.cast
+        (Glade.get_widget_msg ~name:"ScriptTextView" ~info:"GtkTextView" xmldata))
+    method scriptTextView = scriptTextView
+    method 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 =
-      dialog_vbox5#misc#reparent parent;
+      vbox5#misc#reparent parent;
       toplevel#destroy ()
     method check_widgets () = ()
   end
 
 let check_all ?(show=false) () =
   ignore (GMain.Main.init ());
-  let debug = new debug () in
-  if show then debug#toplevel#show ();
-  debug#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 interpChoiceDialog = new interpChoiceDialog () in
   if show then interpChoiceDialog#toplevel#show ();
   interpChoiceDialog#check_widgets ();
@@ -485,9 +745,9 @@ let check_all ?(show=false) () =
   let aboutWin = new aboutWin () in
   if show then aboutWin#toplevel#show ();
   aboutWin#check_widgets ();
-  let genericDialog = new genericDialog () in
-  if show then genericDialog#toplevel#show ();
-  genericDialog#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 ();