X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fmathita%2FmathitaGui.ml;h=957c5edcc12e4eaaa7de4b73852d224310693803;hb=07287062d5b84a0f2b66380d0d380bbf68217a27;hp=b11877a1117b8c625f71a591921020d16a7ebd60;hpb=012882cec674d741f69fce307a6822a584fd6a45;p=helm.git

diff --git a/helm/mathita/mathitaGui.ml b/helm/mathita/mathitaGui.ml
index b11877a11..957c5edcc 100644
--- a/helm/mathita/mathitaGui.ml
+++ b/helm/mathita/mathitaGui.ml
@@ -1,260 +1,110 @@
-(* Automatically generated from mathita.glade by lablgladecc *)
+(* Copyright (C) 2004, HELM Team.
+ * 
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ * 
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ * 
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA  02111-1307, USA.
+ * 
+ * For details, see the HELM World-Wide-Web page,
+ * http://helm.cs.unibo.it/
+ *)
 
-class mainWin ?(file="mathita.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 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 exitMenuItem =
-      new GMenu.menu_item (GtkMenu.MenuItem.cast
-        (Glade.get_widget_msg ~name:"ExitMenuItem" ~info:"GtkMenuItem" xmldata))
-    method exitMenuItem = exitMenuItem
-    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 showProofMenuItem =
-      new GMenu.check_menu_item (GtkMenu.CheckMenuItem.cast
-        (Glade.get_widget_msg ~name:"ShowProofMenuItem" ~info:"GtkCheckMenuItem" xmldata))
-    method showProofMenuItem = showProofMenuItem
-    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 proofStatus =
-      new GBin.scrolled_window (GtkBin.ScrolledWindow.cast
-        (Glade.get_widget_msg ~name:"ProofStatus" ~info:"GtkScrolledWindow" xmldata))
-    method proofStatus = proofStatus
-    val scrolledUserInput =
-      new GBin.scrolled_window (GtkBin.ScrolledWindow.cast
-        (Glade.get_widget_msg ~name:"ScrolledUserInput" ~info:"GtkScrolledWindow" xmldata))
-    method scrolledUserInput = scrolledUserInput
-    val userInput =
-      new GText.view (GtkText.View.cast
-        (Glade.get_widget_msg ~name:"UserInput" ~info:"GtkTextView" xmldata))
-    method userInput = userInput
-    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;
-      toplevel#destroy ()
-    method check_widgets () = ()
-  end
-class proofWin ?(file="mathita.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
-    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 ()
-    method check_widgets () = ()
-  end
-class fileSelectionWin ?(file="mathita.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 cancel_button1 =
-      new GButton.button (GtkButton.Button.cast
-        (Glade.get_widget_msg ~name:"cancel_button1" ~info:"GtkButton" xmldata))
-    method cancel_button1 = cancel_button1
-    val ok_button1 =
-      new GButton.button (GtkButton.Button.cast
-        (Glade.get_widget_msg ~name:"ok_button1" ~info:"GtkButton" xmldata))
-    method ok_button1 = ok_button1
-    method check_widgets () = ()
-  end
-class toolBarWin ?(file="mathita.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 vbox1 =
-      new GPack.box (GtkPack.Box.cast
-        (Glade.get_widget_msg ~name:"vbox1" ~info:"GtkVBox" xmldata))
-    method vbox1 = vbox1
-    val button1 =
-      new GButton.button (GtkButton.Button.cast
-        (Glade.get_widget_msg ~name:"button1" ~info:"GtkButton" xmldata))
-    method button1 = button1
-    val button2 =
-      new GButton.button (GtkButton.Button.cast
-        (Glade.get_widget_msg ~name:"button2" ~info:"GtkButton" xmldata))
-    method button2 = button2
-    val button3 =
-      new GButton.button (GtkButton.Button.cast
-        (Glade.get_widget_msg ~name:"button3" ~info:"GtkButton" xmldata))
-    method button3 = button3
-    val button4 =
-      new GButton.button (GtkButton.Button.cast
-        (Glade.get_widget_msg ~name:"button4" ~info:"GtkButton" xmldata))
-    method button4 = button4
-    method reparent parent =
-      toolBarEventBox#misc#reparent parent;
-      toplevel#destroy ()
-    method check_widgets () = ()
-  end
-class genericDialog ?(file="mathita.glade") ?domain ?autoconnect(*=true*) () =
-  let xmldata = Glade.create ~file  ~root:"GenericDialog" ?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))
-    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 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 =
-      new GButton.button (GtkButton.Button.cast
-        (Glade.get_widget_msg ~name:"cancelbutton1" ~info:"GtkButton" xmldata))
-    method cancelbutton1 = cancelbutton1
-    val okbutton1 =
-      new GButton.button (GtkButton.Button.cast
-        (Glade.get_widget_msg ~name:"okbutton1" ~info:"GtkButton" xmldata))
-    method okbutton1 = okbutton1
-    method reparent parent =
-      dialog_vbox1#misc#reparent parent;
-      toplevel#destroy ()
-    method check_widgets () = ()
+(*
+class stringListModel' uriChoiceDialog =
+  let tree_view = uriChoiceDialog#uriChoiceTreeView in
+  let column_list = new GTree.column_list in
+  let text_column = column_list#add Gobject.Data.string in
+  let list_store = GTree.list_store column_list in
+  let renderer = (GTree.cell_renderer_text [], ["text", text_column]) in
+  let view_column = GTree.view_column ~renderer () in
+  let _ = tree_view#set_model (Some (list_store :> GTree.model)) in
+  let _ = tree_view#append_column view_column in
+  object
+    method append s =
+      let tree_iter = list_store#append () in
+      list_store#set ~row:tree_iter ~column:text_column s
+    method clear () = list_store#clear ()
   end
-class aboutWin ?(file="mathita.glade") ?domain ?autoconnect(*=true*) () =
-  let xmldata = Glade.create ~file  ~root:"AboutWin" ?domain () in
+*)
+
+open MathitaGeneratedGui
+open MathitaGtkMisc
+
+class gui file =
+    (* creation order _is_ relevant for windows placement *)
+  let toolbar = new toolBarWin ~file () in
+  let main = new mainWin ~file () in
+  let about = new aboutWin ~file () in
+  let dialog = new genericDialog ~file () in
+  let uriChoice = new uriChoiceDialog ~file () in
+  let interpChoice = new interpChoiceDialog ~file () in
+  let fileSel = new fileSelectionWin ~file () in
+  let proof = new proofWin ~file () in
+  let keyBindingBoxes = (* event boxes which should receive global key events *)
+    [ toolbar#toolBarEventBox; proof#proofWinEventBox ]
+  in
+  let uriChoices = new stringListModel uriChoice#uriChoiceTreeView 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:"AboutWin" ~info:"GtkDialog" xmldata))
-    method toplevel = toplevel
-    val aboutWin : [`NONE | `DELETE_EVENT | `ID of int] GWindow.dialog =
-      new GWindow.dialog (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 okbutton2 =
-      new GButton.button (GtkButton.Button.cast
-        (Glade.get_widget_msg ~name:"okbutton2" ~info:"GtkButton" xmldata))
-    method okbutton2 = okbutton2
-    method reparent parent =
-      dialog_vbox2#misc#reparent parent;
-      toplevel#destroy ()
-    method check_widgets () = ()
+    initializer
+        (* glade's check widgets *)
+      List.iter (fun w -> w#check_widgets ())
+        (let c w = (w :> <check_widgets: unit -> unit>) in
+         [ c about; c dialog; c fileSel; c main; c proof; c toolbar;
+           c uriChoice; c interpChoice ]);
+        (* show/hide commands *)
+      toggle_visibility toolbar#toolBarWin main#showToolBarMenuItem;
+      toggle_visibility proof#proofWin main#showProofMenuItem;
+        (* "global" key bindings *)
+      List.iter (fun (key, callback) -> self#addKeyBinding key callback)
+        [ GdkKeysyms._F3,
+            toggle_win ~check:main#showProofMenuItem proof#proofWin;
+        ];
+        (* about win *)
+      ignore (about#aboutWin#event#connect#delete (fun _ -> true));
+      ignore (main#aboutMenuItem#connect#activate (fun _ ->
+        about#aboutWin#show ()));
+      ignore (about#aboutDismissButton#connect#clicked (fun _ ->
+        about#aboutWin#misc#hide ()));
+        (* menus *)
+      List.iter (fun w -> w#misc#set_sensitive false)
+        [ main#saveMenuItem; main#saveAsMenuItem ];
+      main#helpMenu#set_right_justified true;
+        (* uri choice *)
+      ()
+
+    method toolbar = toolbar
+    method main = main
+    method about = about
+    method dialog = dialog
+    method uriChoice = uriChoice
+    method interpChoice = interpChoice
+    method fileSel = fileSel
+    method proof = proof
+
+    method private addKeyBinding key callback =
+      List.iter (fun evbox -> add_key_binding key callback evbox)
+        keyBindingBoxes
+
+    method setQuitCallback callback =
+      ignore (main#toplevel#connect#destroy callback);
+      ignore (main#quitMenuItem#connect#activate callback);
+      self#addKeyBinding GdkKeysyms._q callback
+
+    method uriChoices = uriChoices
+
   end
 
-let check_all ?(show=false) () =
-  ignore (GMain.Main.init ());
-  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 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 ();
-  if show then GMain.Main.main ()
-;;