first check in of mathita gui

diff --git a/helm/mathita/.cvsignore b/helm/mathita/.cvsignore
new file mode 100644 (file)
index 0000000..bba30b0
--- /dev/null
+++ b/helm/mathita/.cvsignore
@@ -0,0 +1,4 @@
+mathita
+*.cm[aiox]
+*.cmxa
+*.[ao]

diff --git a/helm/mathita/.depend b/helm/mathita/.depend
new file mode 100644 (file)
index 0000000..d55a5e4
--- /dev/null
+++ b/helm/mathita/.depend
@@ -0,0 +1,4 @@
+mathitaGui.cmo: mathitaGui.cmi 
+mathitaGui.cmx: mathitaGui.cmi 
+mathita.cmo: mathitaGui.cmi 
+mathita.cmx: mathitaGui.cmx 

diff --git a/helm/mathita/Makefile b/helm/mathita/Makefile
new file mode 100644 (file)
index 0000000..02b52ea
--- /dev/null
+++ b/helm/mathita/Makefile
@@ -0,0 +1,41 @@
+
+OCAMLFIND = ocamlfind
+REQUIRES = lablgtk2.glade
+OCAML_FLAGS = -package "$(REQUIRES)" -pp camlp4o
+OCAML_THREADS_FLAGS = -thread
+OCAML_DEBUG_FLAGS =
+OCAMLC = $(OCAMLFIND) ocamlc $(OCAML_FLAGS) $(OCAML_THREADS_FLAGS) $(OCAML_DEBUG_FLAGS)
+OCAMLOPT = $(OCAMLFIND) opt $(OCAML_FLAGS) $(OCAML_THREADS_FLAGS) $(OCAML_DEBUG_FLAGS)
+OCAMLDEP = $(OCAMLFIND) ocamldep $(OCAML_FLAGS)
+LABLGLADECC = lablgladecc2
+CMOS = \
+       mathitaGui.cmo
+
+all: mathita
+
+mathita: $(CMOS) mathita.ml
+       $(OCAMLC) -linkpkg -o $@ $^
+
+mathitaGui.ml mathitaGui.mli: mathita.glade
+       $(LABLGLADECC) $< > $@
+       $(OCAMLC) -i mathitaGui.ml > mathitaGui.mli
+
+%.cmi: %.mli
+       $(OCAMLC) -c $<
+%.cmo %.cmi: %.ml
+       $(OCAMLC) -c $<
+%.cmx: %.ml
+       $(OCAMLOPT) -c $<
+%.ml %.mli: %.mly
+       $(OCAMLYACC) $<
+
+clean:
+       rm -rf *.cm[aoix] *.cmxa *.[ao] mathita
+distclean: clean
+       rm -f mathitaGui.ml
+
+depend: mathitaGui.ml
+       $(OCAMLDEP) *.ml *.mli > .depend
+
+include .depend
+

diff --git a/helm/mathita/mathita.glade b/helm/mathita/mathita.glade
new file mode 100644 (file)
index 0000000..a1150cf
--- /dev/null
+++ b/helm/mathita/mathita.glade
@@ -0,0 +1,467 @@
+<?xml version="1.0" standalone="no"?> <!--*- mode: xml -*-->
+<!DOCTYPE glade-interface SYSTEM "http://glade.gnome.org/glade-2.0.dtd">
+
+<glade-interface>
+
+<widget class="GtkWindow" id="MainWin">
+  <property name="visible">True</property>
+  <property name="title" translatable="yes">Mathita</property>
+  <property name="type">GTK_WINDOW_TOPLEVEL</property>
+  <property name="window_position">GTK_WIN_POS_NONE</property>
+  <property name="modal">False</property>
+  <property name="default_width">800</property>
+  <property name="default_height">600</property>
+  <property name="resizable">True</property>
+  <property name="destroy_with_parent">False</property>
+
+  <child>
+    <widget class="GtkVBox" id="MainWinShape">
+      <property name="visible">True</property>
+      <property name="homogeneous">False</property>
+      <property name="spacing">0</property>
+
+      <child>
+       <widget class="GtkMenuBar" id="MainMenuBar">
+         <property name="visible">True</property>
+
+         <child>
+           <widget class="GtkMenuItem" id="fileMenu">
+             <property name="visible">True</property>
+             <property name="label" translatable="yes">_File</property>
+             <property name="use_underline">True</property>
+
+             <child>
+               <widget class="GtkMenu" id="fileMenu_menu">
+
+                 <child>
+                   <widget class="GtkMenuItem" id="ExitMenuItem">
+                     <property name="visible">True</property>
+                     <property name="label" translatable="yes">Exit</property>
+                     <property name="use_underline">True</property>
+                     <accelerator key="q" modifiers="GDK_CONTROL_MASK" signal="activate"/>
+                   </widget>
+                 </child>
+               </widget>
+             </child>
+           </widget>
+         </child>
+
+         <child>
+           <widget class="GtkMenuItem" id="EditMenu">
+             <property name="visible">True</property>
+             <property name="label" translatable="yes">_Edit</property>
+             <property name="use_underline">True</property>
+           </widget>
+         </child>
+
+         <child>
+           <widget class="GtkMenuItem" id="ViewMenu">
+             <property name="visible">True</property>
+             <property name="label" translatable="yes">_View</property>
+             <property name="use_underline">True</property>
+
+             <child>
+               <widget class="GtkMenu" id="ViewMenu_menu">
+
+                 <child>
+                   <widget class="GtkCheckMenuItem" id="ShowToolBarMenuItem">
+                     <property name="visible">True</property>
+                     <property name="label" translatable="yes">Show Button Bar</property>
+                     <property name="use_underline">True</property>
+                     <property name="active">True</property>
+                   </widget>
+                 </child>
+
+                 <child>
+                   <widget class="GtkCheckMenuItem" id="ShowProofMenuItem">
+                     <property name="visible">True</property>
+                     <property name="label" translatable="yes">Show Proof Window</property>
+                     <property name="use_underline">True</property>
+                     <property name="active">False</property>
+                     <accelerator key="F3" modifiers="0" signal="activate"/>
+                   </widget>
+                 </child>
+               </widget>
+             </child>
+           </widget>
+         </child>
+
+         <child>
+           <widget class="GtkMenuItem" id="HelpMenu">
+             <property name="visible">True</property>
+             <property name="label" translatable="yes">_Help</property>
+             <property name="use_underline">True</property>
+
+             <child>
+               <widget class="GtkMenu" id="HelpMenu_menu">
+
+                 <child>
+                   <widget class="GtkMenuItem" id="AboutMenuItem">
+                     <property name="visible">True</property>
+                     <property name="label" translatable="yes">About...</property>
+                     <property name="use_underline">True</property>
+                   </widget>
+                 </child>
+               </widget>
+             </child>
+           </widget>
+         </child>
+       </widget>
+       <packing>
+         <property name="padding">0</property>
+         <property name="expand">False</property>
+         <property name="fill">False</property>
+       </packing>
+      </child>
+
+      <child>
+       <widget class="GtkVPaned" id="MainVPanes">
+         <property name="visible">True</property>
+         <property name="can_focus">True</property>
+         <property name="position">450</property>
+
+         <child>
+           <widget class="GtkScrolledWindow" id="ProofStatus">
+             <property name="visible">True</property>
+             <property name="hscrollbar_policy">GTK_POLICY_ALWAYS</property>
+             <property name="vscrollbar_policy">GTK_POLICY_ALWAYS</property>
+             <property name="shadow_type">GTK_SHADOW_NONE</property>
+             <property name="window_placement">GTK_CORNER_TOP_LEFT</property>
+
+             <child>
+               <placeholder/>
+             </child>
+           </widget>
+           <packing>
+             <property name="shrink">True</property>
+             <property name="resize">False</property>
+           </packing>
+         </child>
+
+         <child>
+           <widget class="GtkScrolledWindow" id="ScrolledUserInput">
+             <property name="visible">True</property>
+             <property name="hscrollbar_policy">GTK_POLICY_NEVER</property>
+             <property name="vscrollbar_policy">GTK_POLICY_ALWAYS</property>
+             <property name="shadow_type">GTK_SHADOW_IN</property>
+             <property name="window_placement">GTK_CORNER_TOP_LEFT</property>
+
+             <child>
+               <widget class="GtkTextView" id="UserInput">
+                 <property name="visible">True</property>
+                 <property name="can_focus">True</property>
+                 <property name="editable">False</property>
+                 <property name="justification">GTK_JUSTIFY_LEFT</property>
+                 <property name="wrap_mode">GTK_WRAP_WORD</property>
+                 <property name="cursor_visible">True</property>
+                 <property name="pixels_above_lines">0</property>
+                 <property name="pixels_below_lines">0</property>
+                 <property name="pixels_inside_wrap">0</property>
+                 <property name="left_margin">0</property>
+                 <property name="right_margin">0</property>
+                 <property name="indent">0</property>
+                 <property name="text" translatable="yes"></property>
+               </widget>
+             </child>
+           </widget>
+           <packing>
+             <property name="shrink">True</property>
+             <property name="resize">True</property>
+           </packing>
+         </child>
+       </widget>
+       <packing>
+         <property name="padding">0</property>
+         <property name="expand">True</property>
+         <property name="fill">True</property>
+       </packing>
+      </child>
+
+      <child>
+       <widget class="GtkStatusbar" id="MainStatusBar">
+         <property name="visible">True</property>
+         <property name="has_resize_grip">True</property>
+       </widget>
+       <packing>
+         <property name="padding">0</property>
+         <property name="expand">False</property>
+         <property name="fill">False</property>
+       </packing>
+      </child>
+    </widget>
+  </child>
+</widget>
+
+<widget class="GtkWindow" id="ProofWin">
+  <property name="title" translatable="yes">Mathita: current proof</property>
+  <property name="type">GTK_WINDOW_TOPLEVEL</property>
+  <property name="window_position">GTK_WIN_POS_NONE</property>
+  <property name="modal">False</property>
+  <property name="default_width">700</property>
+  <property name="default_height">525</property>
+  <property name="resizable">True</property>
+  <property name="destroy_with_parent">False</property>
+
+  <child>
+    <widget class="GtkEventBox" id="ProofWinEventBox">
+      <property name="visible">True</property>
+
+      <child>
+       <widget class="GtkScrolledWindow" id="ScrolledProof">
+         <property name="visible">True</property>
+         <property name="hscrollbar_policy">GTK_POLICY_ALWAYS</property>
+         <property name="vscrollbar_policy">GTK_POLICY_ALWAYS</property>
+         <property name="shadow_type">GTK_SHADOW_NONE</property>
+         <property name="window_placement">GTK_CORNER_TOP_LEFT</property>
+
+         <child>
+           <widget class="GtkViewport" id="viewport1">
+             <property name="visible">True</property>
+             <property name="shadow_type">GTK_SHADOW_IN</property>
+
+             <child>
+               <placeholder/>
+             </child>
+           </widget>
+         </child>
+       </widget>
+      </child>
+    </widget>
+  </child>
+</widget>
+
+<widget class="GtkFileSelection" id="FileSelectionWin">
+  <property name="border_width">10</property>
+  <property name="title" translatable="yes">Select File</property>
+  <property name="type">GTK_WINDOW_TOPLEVEL</property>
+  <property name="window_position">GTK_WIN_POS_NONE</property>
+  <property name="modal">True</property>
+  <property name="resizable">True</property>
+  <property name="destroy_with_parent">False</property>
+  <property name="show_fileops">True</property>
+
+  <child internal-child="cancel_button">
+    <widget class="GtkButton" id="cancel_button1">
+      <property name="visible">True</property>
+      <property name="can_default">True</property>
+      <property name="can_focus">True</property>
+      <property name="relief">GTK_RELIEF_NORMAL</property>
+    </widget>
+  </child>
+
+  <child internal-child="ok_button">
+    <widget class="GtkButton" id="ok_button1">
+      <property name="visible">True</property>
+      <property name="can_default">True</property>
+      <property name="can_focus">True</property>
+      <property name="relief">GTK_RELIEF_NORMAL</property>
+    </widget>
+  </child>
+</widget>
+
+<widget class="GtkWindow" id="ToolBarWin">
+  <property name="width_request">130</property>
+  <property name="height_request">450</property>
+  <property name="visible">True</property>
+  <property name="title" translatable="yes">ToolBar</property>
+  <property name="type">GTK_WINDOW_TOPLEVEL</property>
+  <property name="window_position">GTK_WIN_POS_NONE</property>
+  <property name="modal">False</property>
+  <property name="resizable">False</property>
+  <property name="destroy_with_parent">False</property>
+
+  <child>
+    <widget class="GtkEventBox" id="ToolBarEventBox">
+      <property name="visible">True</property>
+
+      <child>
+       <widget class="GtkVBox" id="vbox1">
+         <property name="visible">True</property>
+         <property name="homogeneous">False</property>
+         <property name="spacing">0</property>
+
+         <child>
+           <widget class="GtkVButtonBox" id="vbuttonbox1">
+             <property name="visible">True</property>
+             <property name="layout_style">GTK_BUTTONBOX_DEFAULT_STYLE</property>
+             <property name="spacing">0</property>
+
+             <child>
+               <widget class="GtkButton" id="button1">
+                 <property name="width_request">120</property>
+                 <property name="visible">True</property>
+                 <property name="can_default">True</property>
+                 <property name="can_focus">True</property>
+                 <property name="label" translatable="yes">button1</property>
+                 <property name="use_underline">True</property>
+                 <property name="relief">GTK_RELIEF_NORMAL</property>
+               </widget>
+             </child>
+
+             <child>
+               <widget class="GtkButton" id="button2">
+                 <property name="visible">True</property>
+                 <property name="can_default">True</property>
+                 <property name="can_focus">True</property>
+                 <property name="label" translatable="yes">button2</property>
+                 <property name="use_underline">True</property>
+                 <property name="relief">GTK_RELIEF_NORMAL</property>
+               </widget>
+             </child>
+
+             <child>
+               <widget class="GtkButton" id="button3">
+                 <property name="visible">True</property>
+                 <property name="can_default">True</property>
+                 <property name="can_focus">True</property>
+                 <property name="label" translatable="yes">button3</property>
+                 <property name="use_underline">True</property>
+                 <property name="relief">GTK_RELIEF_NORMAL</property>
+               </widget>
+             </child>
+
+             <child>
+               <widget class="GtkButton" id="button4">
+                 <property name="visible">True</property>
+                 <property name="can_default">True</property>
+                 <property name="can_focus">True</property>
+                 <property name="label" translatable="yes">button4</property>
+                 <property name="use_underline">True</property>
+                 <property name="relief">GTK_RELIEF_NORMAL</property>
+               </widget>
+             </child>
+           </widget>
+           <packing>
+             <property name="padding">0</property>
+             <property name="expand">False</property>
+             <property name="fill">True</property>
+           </packing>
+         </child>
+
+         <child>
+           <widget class="GtkHSeparator" id="hseparator1">
+             <property name="visible">True</property>
+           </widget>
+           <packing>
+             <property name="padding">5</property>
+             <property name="expand">False</property>
+             <property name="fill">True</property>
+           </packing>
+         </child>
+
+         <child>
+           <placeholder/>
+         </child>
+       </widget>
+      </child>
+    </widget>
+  </child>
+</widget>
+
+<widget class="GtkDialog" id="GenericDialog">
+  <property name="title" translatable="yes">DUMMY</property>
+  <property name="type">GTK_WINDOW_TOPLEVEL</property>
+  <property name="window_position">GTK_WIN_POS_NONE</property>
+  <property name="modal">True</property>
+  <property name="resizable">False</property>
+  <property name="destroy_with_parent">False</property>
+  <property name="has_separator">True</property>
+
+  <child internal-child="vbox">
+    <widget class="GtkVBox" id="dialog-vbox1">
+      <property name="visible">True</property>
+      <property name="homogeneous">False</property>
+      <property name="spacing">0</property>
+
+      <child internal-child="action_area">
+       <widget class="GtkHButtonBox" id="dialog-action_area1">
+         <property name="visible">True</property>
+         <property name="layout_style">GTK_BUTTONBOX_END</property>
+
+         <child>
+           <widget class="GtkButton" id="cancelbutton1">
+             <property name="visible">True</property>
+             <property name="can_default">True</property>
+             <property name="can_focus">True</property>
+             <property name="label">gtk-cancel</property>
+             <property name="use_stock">True</property>
+             <property name="relief">GTK_RELIEF_NORMAL</property>
+             <property name="response_id">-6</property>
+           </widget>
+         </child>
+
+         <child>
+           <widget class="GtkButton" id="okbutton1">
+             <property name="visible">True</property>
+             <property name="can_default">True</property>
+             <property name="can_focus">True</property>
+             <property name="label">gtk-ok</property>
+             <property name="use_stock">True</property>
+             <property name="relief">GTK_RELIEF_NORMAL</property>
+             <property name="response_id">-5</property>
+           </widget>
+         </child>
+       </widget>
+       <packing>
+         <property name="padding">0</property>
+         <property name="expand">False</property>
+         <property name="fill">True</property>
+         <property name="pack_type">GTK_PACK_END</property>
+       </packing>
+      </child>
+
+      <child>
+       <placeholder/>
+      </child>
+    </widget>
+  </child>
+</widget>
+
+<widget class="GtkDialog" id="AboutWin">
+  <property name="title" translatable="yes">Mathita: about</property>
+  <property name="type">GTK_WINDOW_TOPLEVEL</property>
+  <property name="window_position">GTK_WIN_POS_NONE</property>
+  <property name="modal">True</property>
+  <property name="resizable">False</property>
+  <property name="destroy_with_parent">False</property>
+  <property name="has_separator">True</property>
+
+  <child internal-child="vbox">
+    <widget class="GtkVBox" id="dialog-vbox2">
+      <property name="visible">True</property>
+      <property name="homogeneous">False</property>
+      <property name="spacing">0</property>
+
+      <child internal-child="action_area">
+       <widget class="GtkHButtonBox" id="dialog-action_area2">
+         <property name="visible">True</property>
+         <property name="layout_style">GTK_BUTTONBOX_END</property>
+
+         <child>
+           <widget class="GtkButton" id="okbutton2">
+             <property name="visible">True</property>
+             <property name="can_default">True</property>
+             <property name="can_focus">True</property>
+             <property name="label">gtk-ok</property>
+             <property name="use_stock">True</property>
+             <property name="relief">GTK_RELIEF_NORMAL</property>
+             <property name="response_id">-5</property>
+           </widget>
+         </child>
+       </widget>
+       <packing>
+         <property name="padding">0</property>
+         <property name="expand">False</property>
+         <property name="fill">True</property>
+         <property name="pack_type">GTK_PACK_END</property>
+       </packing>
+      </child>
+
+      <child>
+       <placeholder/>
+      </child>
+    </widget>
+  </child>
+</widget>
+
+</glade-interface>

diff --git a/helm/mathita/mathita.gladep b/helm/mathita/mathita.gladep
new file mode 100644 (file)
index 0000000..996d23c
--- /dev/null
+++ b/helm/mathita/mathita.gladep
@@ -0,0 +1,8 @@
+<?xml version="1.0" standalone="no"?> <!--*- mode: xml -*-->
+<!DOCTYPE glade-project SYSTEM "http://glade.gnome.org/glade-project-2.0.dtd">
+
+<glade-project>
+  <name>Mathita</name>
+  <program_name>mathita</program_name>
+  <gnome_support>FALSE</gnome_support>
+</glade-project>

diff --git a/helm/mathita/mathita.ml b/helm/mathita/mathita.ml
new file mode 100644 (file)
index 0000000..0d3b622
--- /dev/null
+++ b/helm/mathita/mathita.ml
@@ -0,0 +1,86 @@
+(* 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/
+ *)
+
+  (** quit program, possibly asking for confirmation *)
+let quit () =
+  GMain.Main.quit ()
+
+  (** given a window and a check menu item it links the two so that the former
+   * is only hidden on delete and the latter toggle show/hide of the former *)
+let toggle_visibility (win: GWindow.window) (check: GMenu.check_menu_item) =
+  ignore (check#connect#toggled (fun _ ->
+    if check#active then win#show () else win#misc#hide ()));
+  ignore (win#event#connect#delete (fun _ ->
+    win#misc#hide ();
+    check#set_active false;
+    true))
+
+let toggle_win ?check win () =
+  if win#is_active then win#misc#hide () else win#show ();
+  match check with
+  | None -> ()
+  | Some check -> check#set_active (not check#active)
+
+let add_key_bindings bindings (evbox: GBin.event_box) =
+  List.iter
+    (fun (key, callback) ->
+      ignore (evbox#event#connect#key_press (function
+        | key' when GdkEvent.Key.keyval key' = key ->
+            callback ();
+            false
+        | _ -> false)))
+    bindings
+
+class gui file =
+  object (self)
+    val about = new MathitaGui.aboutWin ~file ()
+    val dialog = new MathitaGui.genericDialog ~file ()
+    val filesel = new MathitaGui.fileSelectionWin ~file ()
+    val main = new MathitaGui.mainWin ~file ()
+    val proof = new MathitaGui.proofWin ~file ()
+    val toolbar = new MathitaGui.toolBarWin ~file ()
+    initializer
+      let c w = (w :> <check_widgets: unit -> unit>) in
+      List.iter (fun w -> w#check_widgets ())
+        [ c about; c dialog; c filesel; c main; c proof; c toolbar ];
+      ignore (main#toplevel#connect#destroy quit);
+      ignore (main#exitMenuItem#connect#activate quit);
+      toggle_visibility toolbar#toolBarWin main#showToolBarMenuItem;
+      toggle_visibility proof#proofWin main#showProofMenuItem;
+      let key_bindings = [
+        GdkKeysyms._F3, toggle_win ~check:main#showProofMenuItem proof#proofWin;
+        GdkKeysyms._q, quit;
+      ] in
+      add_key_bindings key_bindings toolbar#toolBarEventBox;
+      add_key_bindings key_bindings proof#proofWinEventBox;
+      ()
+  end
+
+let _ =
+  let glade_file = "mathita.glade" in
+  let _ = GMain.Main.init () in
+  let gui = new gui glade_file in
+  GtkThread.main ()
+

diff --git a/helm/mathita/mathitaGui.ml b/helm/mathita/mathitaGui.ml
new file mode 100644 (file)
index 0000000..b11877a
--- /dev/null
+++ b/helm/mathita/mathitaGui.ml
@@ -0,0 +1,260 @@
+(* Automatically generated from mathita.glade by lablgladecc *)
+
+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 () = ()
+  end
+class aboutWin ?(file="mathita.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
+        (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 () = ()
+  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 ()
+;;

diff --git a/helm/mathita/mathitaGui.mli b/helm/mathita/mathitaGui.mli
new file mode 100644 (file)
index 0000000..2f8416c
--- /dev/null
+++ b/helm/mathita/mathitaGui.mli
@@ -0,0 +1,165 @@
+class mainWin :
+  ?file:string ->
+  ?domain:string ->
+  ?autoconnect:bool ->
+  unit ->
+  object
+    val aboutMenuItem : GMenu.menu_item
+    val editMenu : GMenu.menu_item
+    val exitMenuItem : GMenu.menu_item
+    val fileMenu : GMenu.menu_item
+    val fileMenu_menu : GMenu.menu
+    val helpMenu : GMenu.menu_item
+    val helpMenu_menu : GMenu.menu
+    val mainMenuBar : GMenu.menu_shell
+    val mainStatusBar : GMisc.statusbar
+    val mainVPanes : GPack.paned
+    val mainWin : GWindow.window
+    val mainWinShape : GPack.box
+    val proofStatus : GBin.scrolled_window
+    val scrolledUserInput : GBin.scrolled_window
+    val showProofMenuItem : GMenu.check_menu_item
+    val showToolBarMenuItem : GMenu.check_menu_item
+    val toplevel : GWindow.window
+    val userInput : GText.view
+    val viewMenu : GMenu.menu_item
+    val viewMenu_menu : GMenu.menu
+    val xml : Glade.glade_xml Gtk.obj
+    method aboutMenuItem : GMenu.menu_item
+    method bind : name:string -> callback:(unit -> unit) -> unit
+    method check_widgets : unit -> unit
+    method editMenu : GMenu.menu_item
+    method exitMenuItem : GMenu.menu_item
+    method fileMenu : GMenu.menu_item
+    method fileMenu_menu : GMenu.menu
+    method helpMenu : GMenu.menu_item
+    method helpMenu_menu : GMenu.menu
+    method mainMenuBar : GMenu.menu_shell
+    method mainStatusBar : GMisc.statusbar
+    method mainVPanes : GPack.paned
+    method mainWin : GWindow.window
+    method mainWinShape : GPack.box
+    method proofStatus : GBin.scrolled_window
+    method reparent : GObj.widget -> unit
+    method scrolledUserInput : GBin.scrolled_window
+    method showProofMenuItem : GMenu.check_menu_item
+    method showToolBarMenuItem : GMenu.check_menu_item
+    method toplevel : GWindow.window
+    method userInput : GText.view
+    method viewMenu : GMenu.menu_item
+    method viewMenu_menu : GMenu.menu
+    method xml : Glade.glade_xml Gtk.obj
+  end
+class proofWin :
+  ?file:string ->
+  ?domain:string ->
+  ?autoconnect:bool ->
+  unit ->
+  object
+    val proofWin : GWindow.window
+    val proofWinEventBox : GBin.event_box
+    val scrolledProof : GBin.scrolled_window
+    val toplevel : GWindow.window
+    val viewport1 : GBin.viewport
+    val xml : Glade.glade_xml Gtk.obj
+    method bind : name:string -> callback:(unit -> unit) -> unit
+    method check_widgets : unit -> unit
+    method proofWin : GWindow.window
+    method proofWinEventBox : GBin.event_box
+    method reparent : GObj.widget -> unit
+    method scrolledProof : GBin.scrolled_window
+    method toplevel : GWindow.window
+    method viewport1 : GBin.viewport
+    method xml : Glade.glade_xml Gtk.obj
+  end
+class fileSelectionWin :
+  ?file:string ->
+  ?domain:string ->
+  ?autoconnect:bool ->
+  unit ->
+  object
+    val cancel_button1 : GButton.button
+    val fileSelectionWin : GWindow.file_selection
+    val ok_button1 : GButton.button
+    val toplevel : GWindow.file_selection
+    val xml : Glade.glade_xml Gtk.obj
+    method bind : name:string -> callback:(unit -> unit) -> unit
+    method cancel_button1 : GButton.button
+    method check_widgets : unit -> unit
+    method fileSelectionWin : GWindow.file_selection
+    method ok_button1 : GButton.button
+    method toplevel : GWindow.file_selection
+    method xml : Glade.glade_xml Gtk.obj
+  end
+class toolBarWin :
+  ?file:string ->
+  ?domain:string ->
+  ?autoconnect:bool ->
+  unit ->
+  object
+    val button1 : GButton.button
+    val button2 : GButton.button
+    val button3 : GButton.button
+    val button4 : GButton.button
+    val toolBarEventBox : GBin.event_box
+    val toolBarWin : GWindow.window
+    val toplevel : GWindow.window
+    val vbox1 : GPack.box
+    val xml : Glade.glade_xml Gtk.obj
+    method bind : name:string -> callback:(unit -> unit) -> unit
+    method button1 : GButton.button
+    method button2 : GButton.button
+    method button3 : GButton.button
+    method button4 : GButton.button
+    method check_widgets : unit -> unit
+    method reparent : GObj.widget -> unit
+    method toolBarEventBox : GBin.event_box
+    method toolBarWin : GWindow.window
+    method toplevel : GWindow.window
+    method vbox1 : GPack.box
+    method xml : Glade.glade_xml Gtk.obj
+  end
+class genericDialog :
+  ?file:string ->
+  ?domain:string ->
+  ?autoconnect:bool ->
+  unit ->
+  object
+    val cancelbutton1 : GButton.button
+    val dialog_vbox1 : GPack.box
+    val genericDialog : [ `DELETE_EVENT | `ID of int | `NONE ] GWindow.dialog
+    val okbutton1 : GButton.button
+    val toplevel : [ `DELETE_EVENT | `ID of int | `NONE ] GWindow.dialog
+    val xml : Glade.glade_xml Gtk.obj
+    method bind : name:string -> callback:(unit -> unit) -> unit
+    method cancelbutton1 : GButton.button
+    method check_widgets : unit -> unit
+    method dialog_vbox1 : GPack.box
+    method genericDialog :
+      [ `DELETE_EVENT | `ID of int | `NONE ] GWindow.dialog
+    method okbutton1 : GButton.button
+    method reparent : GObj.widget -> unit
+    method toplevel : [ `DELETE_EVENT | `ID of int | `NONE ] GWindow.dialog
+    method xml : Glade.glade_xml Gtk.obj
+  end
+class aboutWin :
+  ?file:string ->
+  ?domain:string ->
+  ?autoconnect:bool ->
+  unit ->
+  object
+    val aboutWin : [ `DELETE_EVENT | `ID of int | `NONE ] GWindow.dialog
+    val dialog_vbox2 : GPack.box
+    val okbutton2 : GButton.button
+    val toplevel : [ `DELETE_EVENT | `ID of int | `NONE ] GWindow.dialog
+    val xml : Glade.glade_xml Gtk.obj
+    method aboutWin : [ `DELETE_EVENT | `ID of int | `NONE ] GWindow.dialog
+    method bind : name:string -> callback:(unit -> unit) -> unit
+    method check_widgets : unit -> unit
+    method dialog_vbox2 : GPack.box
+    method okbutton2 : GButton.button
+    method reparent : GObj.widget -> unit
+    method toplevel : [ `DELETE_EVENT | `ID of int | `NONE ] GWindow.dialog
+    method xml : Glade.glade_xml Gtk.obj
+  end
+val check_all : ?show:bool -> unit -> unit