-mathitaGui.cmo: mathitaGui.cmi
-mathitaGui.cmx: mathitaGui.cmi
-mathita.cmo: mathitaGui.cmi
+mathitaGeneratedGui.cmo: mathitaGeneratedGui.cmi
+mathitaGeneratedGui.cmx: mathitaGeneratedGui.cmi
+mathitaGtkMisc.cmo: mathitaGtkMisc.cmi
+mathitaGtkMisc.cmx: mathitaGtkMisc.cmi
+mathitaGui.cmo: mathitaGeneratedGui.cmi mathitaGtkMisc.cmi
+mathitaGui.cmx: mathitaGeneratedGui.cmx mathitaGtkMisc.cmx
+mathita.cmo: mathitaGui.cmo
mathita.cmx: mathitaGui.cmx
OCAMLFIND = ocamlfind
-REQUIRES = lablgtk2.glade
+REQUIRES = lablgtk2.glade helm-registry
OCAML_FLAGS = -package "$(REQUIRES)" -pp camlp4o
OCAML_THREADS_FLAGS = -thread
OCAML_DEBUG_FLAGS =
OCAMLDEP = $(OCAMLFIND) ocamldep $(OCAML_FLAGS)
LABLGLADECC = lablgladecc2
CMOS = \
+ mathitaGeneratedGui.cmo \
+ mathitaGtkMisc.cmo \
mathitaGui.cmo
all: mathita
mathita: $(CMOS) mathita.ml
$(OCAMLC) -linkpkg -o $@ $^
-mathitaGui.ml mathitaGui.mli: mathita.glade
+mathitaGeneratedGui.ml mathitaGeneratedGui.mli: mathita.glade
$(LABLGLADECC) $< > $@
- $(OCAMLC) -i mathitaGui.ml > mathitaGui.mli
+ $(OCAMLC) -i mathitaGeneratedGui.ml > mathitaGeneratedGui.mli
%.cmi: %.mli
$(OCAMLC) -c $<
clean:
rm -rf *.cm[aoix] *.cmxa *.[ao] mathita
distclean: clean
- rm -f mathitaGui.ml
+ rm -f mathitaGeneratedGui.ml
-depend: mathitaGui.ml
+depend: mathitaGeneratedGui.ml
$(OCAMLDEP) *.ml *.mli > .depend
include .depend
--- /dev/null
+<?xml version="1.0" encoding="utf-8"?>
+<helm_registry>
+ <section name="mathita">
+ <key name="glade_file">mathita.glade</key>
+ <key name="auto_disambiguation">true</key>
+ </section>
+</helm_registry>
<property name="visible">True</property>
<child>
- <widget class="GtkMenuItem" id="fileMenu">
+ <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">
+ <widget class="GtkMenu" id="FileMenu_menu">
<child>
- <widget class="GtkMenuItem" id="ExitMenuItem">
+ <widget class="GtkImageMenuItem" id="NewMenu">
<property name="visible">True</property>
- <property name="label" translatable="yes">Exit</property>
+ <property name="label" translatable="yes">_New</property>
+ <property name="use_underline">True</property>
+
+ <child internal-child="image">
+ <widget class="GtkImage" id="image13">
+ <property name="visible">True</property>
+ <property name="stock">gtk-new</property>
+ <property name="icon_size">1</property>
+ <property name="xalign">0.5</property>
+ <property name="yalign">0.5</property>
+ <property name="xpad">0</property>
+ <property name="ypad">0</property>
+ </widget>
+ </child>
+
+ <child>
+ <widget class="GtkMenu" id="NewMenu_menu">
+
+ <child>
+ <widget class="GtkMenuItem" id="NewProofMenuItem">
+ <property name="visible">True</property>
+ <property name="label" translatable="yes">_Proof or definition ...</property>
+ <property name="use_underline">True</property>
+ <accelerator key="n" modifiers="GDK_CONTROL_MASK" signal="activate"/>
+ </widget>
+ </child>
+
+ <child>
+ <widget class="GtkMenuItem" id="NewDefsMenuItem">
+ <property name="visible">True</property>
+ <property name="label" translatable="yes">(Co)Inductive _definitions ...</property>
+ <property name="use_underline">True</property>
+ </widget>
+ </child>
+ </widget>
+ </child>
+ </widget>
+ </child>
+
+ <child>
+ <widget class="GtkImageMenuItem" id="OpenMenuItem">
+ <property name="visible">True</property>
+ <property name="label" translatable="yes">_Open...</property>
+ <property name="use_underline">True</property>
+ <accelerator key="o" modifiers="GDK_CONTROL_MASK" signal="activate"/>
+
+ <child internal-child="image">
+ <widget class="GtkImage" id="image14">
+ <property name="visible">True</property>
+ <property name="stock">gtk-open</property>
+ <property name="icon_size">1</property>
+ <property name="xalign">0.5</property>
+ <property name="yalign">0.5</property>
+ <property name="xpad">0</property>
+ <property name="ypad">0</property>
+ </widget>
+ </child>
+ </widget>
+ </child>
+
+ <child>
+ <widget class="GtkImageMenuItem" id="SaveMenuItem">
+ <property name="visible">True</property>
+ <property name="label" translatable="yes">_Save</property>
+ <property name="use_underline">True</property>
+ <accelerator key="s" modifiers="GDK_CONTROL_MASK" signal="activate"/>
+
+ <child internal-child="image">
+ <widget class="GtkImage" id="image15">
+ <property name="visible">True</property>
+ <property name="stock">gtk-save</property>
+ <property name="icon_size">1</property>
+ <property name="xalign">0.5</property>
+ <property name="yalign">0.5</property>
+ <property name="xpad">0</property>
+ <property name="ypad">0</property>
+ </widget>
+ </child>
+ </widget>
+ </child>
+
+ <child>
+ <widget class="GtkImageMenuItem" id="SaveAsMenuItem">
+ <property name="visible">True</property>
+ <property name="label" translatable="yes">Save _As ...</property>
+ <property name="use_underline">True</property>
+
+ <child internal-child="image">
+ <widget class="GtkImage" id="image16">
+ <property name="visible">True</property>
+ <property name="stock">gtk-save-as</property>
+ <property name="icon_size">1</property>
+ <property name="xalign">0.5</property>
+ <property name="yalign">0.5</property>
+ <property name="xpad">0</property>
+ <property name="ypad">0</property>
+ </widget>
+ </child>
+ </widget>
+ </child>
+
+ <child>
+ <widget class="GtkMenuItem" id="separator1">
+ <property name="visible">True</property>
+ </widget>
+ </child>
+
+ <child>
+ <widget class="GtkImageMenuItem" id="QuitMenuItem">
+ <property name="visible">True</property>
+ <property name="label" translatable="yes">_Quit</property>
<property name="use_underline">True</property>
<accelerator key="q" modifiers="GDK_CONTROL_MASK" signal="activate"/>
+
+ <child internal-child="image">
+ <widget class="GtkImage" id="image17">
+ <property name="visible">True</property>
+ <property name="stock">gtk-quit</property>
+ <property name="icon_size">1</property>
+ <property name="xalign">0.5</property>
+ <property name="yalign">0.5</property>
+ <property name="xpad">0</property>
+ <property name="ypad">0</property>
+ </widget>
+ </child>
</widget>
</child>
</widget>
<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>
+ <placeholder/>
</child>
</widget>
<packing>
<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="window_position">GTK_WIN_POS_CENTER</property>
<property name="modal">True</property>
<property name="resizable">True</property>
<property name="destroy_with_parent">False</property>
<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="window_position">GTK_WIN_POS_CENTER</property>
<property name="modal">True</property>
<property name="resizable">False</property>
<property name="destroy_with_parent">False</property>
<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="window_position">GTK_WIN_POS_CENTER</property>
<property name="modal">True</property>
<property name="resizable">False</property>
<property name="destroy_with_parent">False</property>
<property name="layout_style">GTK_BUTTONBOX_END</property>
<child>
- <widget class="GtkButton" id="okbutton2">
+ <widget class="GtkButton" id="AboutDismissButton">
<property name="visible">True</property>
<property name="can_default">True</property>
<property name="can_focus">True</property>
</child>
</widget>
+<widget class="GtkDialog" id="UriChoiceDialog">
+ <property name="height_request">280</property>
+ <property name="visible">True</property>
+ <property name="title" translatable="yes">Uri choice</property>
+ <property name="type">GTK_WINDOW_TOPLEVEL</property>
+ <property name="window_position">GTK_WIN_POS_CENTER</property>
+ <property name="modal">True</property>
+ <property name="resizable">True</property>
+ <property name="destroy_with_parent">False</property>
+ <property name="has_separator">True</property>
+
+ <child internal-child="vbox">
+ <widget class="GtkVBox" id="dialog-vbox3">
+ <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_area3">
+ <property name="visible">True</property>
+ <property name="layout_style">GTK_BUTTONBOX_END</property>
+
+ <child>
+ <widget class="GtkButton" id="UriChoiceAbortButton">
+ <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="UriChoiceSelectedButton">
+ <property name="visible">True</property>
+ <property name="can_default">True</property>
+ <property name="can_focus">True</property>
+ <property name="relief">GTK_RELIEF_NORMAL</property>
+ <property name="response_id">0</property>
+
+ <child>
+ <widget class="GtkAlignment" id="alignment2">
+ <property name="visible">True</property>
+ <property name="xalign">0.5</property>
+ <property name="yalign">0.5</property>
+ <property name="xscale">0</property>
+ <property name="yscale">0</property>
+
+ <child>
+ <widget class="GtkHBox" id="hbox3">
+ <property name="visible">True</property>
+ <property name="homogeneous">False</property>
+ <property name="spacing">2</property>
+
+ <child>
+ <widget class="GtkImage" id="image19">
+ <property name="visible">True</property>
+ <property name="stock">gtk-index</property>
+ <property name="icon_size">4</property>
+ <property name="xalign">0.5</property>
+ <property name="yalign">0.5</property>
+ <property name="xpad">0</property>
+ <property name="ypad">0</property>
+ </widget>
+ <packing>
+ <property name="padding">0</property>
+ <property name="expand">False</property>
+ <property name="fill">False</property>
+ </packing>
+ </child>
+
+ <child>
+ <widget class="GtkLabel" id="label3">
+ <property name="visible">True</property>
+ <property name="label" translatable="yes">Try _Selected</property>
+ <property name="use_underline">True</property>
+ <property name="use_markup">False</property>
+ <property name="justify">GTK_JUSTIFY_LEFT</property>
+ <property name="wrap">False</property>
+ <property name="selectable">False</property>
+ <property name="xalign">0.5</property>
+ <property name="yalign">0.5</property>
+ <property name="xpad">0</property>
+ <property name="ypad">0</property>
+ </widget>
+ <packing>
+ <property name="padding">0</property>
+ <property name="expand">False</property>
+ <property name="fill">False</property>
+ </packing>
+ </child>
+ </widget>
+ </child>
+ </widget>
+ </child>
+ </widget>
+ </child>
+
+ <child>
+ <widget class="GtkButton" id="UriChoiceConstantsButton">
+ <property name="visible">True</property>
+ <property name="can_default">True</property>
+ <property name="can_focus">True</property>
+ <property name="label" translatable="yes">Try Constants</property>
+ <property name="use_underline">True</property>
+ <property name="relief">GTK_RELIEF_NORMAL</property>
+ <property name="response_id">0</property>
+ </widget>
+ </child>
+
+ <child>
+ <widget class="GtkButton" id="UriChoiceAutoButton">
+ <property name="visible">True</property>
+ <property name="can_default">True</property>
+ <property name="can_focus">True</property>
+ <property name="relief">GTK_RELIEF_NORMAL</property>
+ <property name="response_id">0</property>
+
+ <child>
+ <widget class="GtkAlignment" id="alignment1">
+ <property name="visible">True</property>
+ <property name="xalign">0.5</property>
+ <property name="yalign">0.5</property>
+ <property name="xscale">0</property>
+ <property name="yscale">0</property>
+
+ <child>
+ <widget class="GtkHBox" id="hbox1">
+ <property name="visible">True</property>
+ <property name="homogeneous">False</property>
+ <property name="spacing">2</property>
+
+ <child>
+ <widget class="GtkImage" id="image18">
+ <property name="visible">True</property>
+ <property name="stock">gtk-ok</property>
+ <property name="icon_size">4</property>
+ <property name="xalign">0.5</property>
+ <property name="yalign">0.5</property>
+ <property name="xpad">0</property>
+ <property name="ypad">0</property>
+ </widget>
+ <packing>
+ <property name="padding">0</property>
+ <property name="expand">False</property>
+ <property name="fill">False</property>
+ </packing>
+ </child>
+
+ <child>
+ <widget class="GtkLabel" id="label1">
+ <property name="visible">True</property>
+ <property name="label" translatable="yes">_Auto</property>
+ <property name="use_underline">True</property>
+ <property name="use_markup">False</property>
+ <property name="justify">GTK_JUSTIFY_LEFT</property>
+ <property name="wrap">False</property>
+ <property name="selectable">False</property>
+ <property name="xalign">0.5</property>
+ <property name="yalign">0.5</property>
+ <property name="xpad">0</property>
+ <property name="ypad">0</property>
+ </widget>
+ <packing>
+ <property name="padding">0</property>
+ <property name="expand">False</property>
+ <property name="fill">False</property>
+ </packing>
+ </child>
+ </widget>
+ </child>
+ </widget>
+ </child>
+ </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>
+ <widget class="GtkVBox" id="vbox2">
+ <property name="visible">True</property>
+ <property name="homogeneous">False</property>
+ <property name="spacing">0</property>
+
+ <child>
+ <widget class="GtkLabel" id="UriChoiceLabel">
+ <property name="visible">True</property>
+ <property name="label" translatable="yes">some informative message here ...</property>
+ <property name="use_underline">False</property>
+ <property name="use_markup">False</property>
+ <property name="justify">GTK_JUSTIFY_LEFT</property>
+ <property name="wrap">False</property>
+ <property name="selectable">False</property>
+ <property name="xalign">0.5</property>
+ <property name="yalign">0.5</property>
+ <property name="xpad">0</property>
+ <property name="ypad">0</property>
+ </widget>
+ <packing>
+ <property name="padding">0</property>
+ <property name="expand">False</property>
+ <property name="fill">False</property>
+ </packing>
+ </child>
+
+ <child>
+ <widget class="GtkScrolledWindow" id="scrolledwindow1">
+ <property name="visible">True</property>
+ <property name="can_focus">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="GtkTreeView" id="UriChoiceTreeView">
+ <property name="visible">True</property>
+ <property name="can_focus">True</property>
+ <property name="headers_visible">False</property>
+ <property name="rules_hint">False</property>
+ <property name="reorderable">False</property>
+ <property name="enable_search">True</property>
+ </widget>
+ </child>
+ </widget>
+ <packing>
+ <property name="padding">0</property>
+ <property name="expand">True</property>
+ <property name="fill">True</property>
+ </packing>
+ </child>
+
+ <child>
+ <widget class="GtkHBox" id="hbox2">
+ <property name="visible">True</property>
+ <property name="homogeneous">False</property>
+ <property name="spacing">0</property>
+
+ <child>
+ <widget class="GtkLabel" id="label2">
+ <property name="visible">True</property>
+ <property name="label" translatable="yes">URI: </property>
+ <property name="use_underline">False</property>
+ <property name="use_markup">False</property>
+ <property name="justify">GTK_JUSTIFY_LEFT</property>
+ <property name="wrap">False</property>
+ <property name="selectable">False</property>
+ <property name="xalign">0.5</property>
+ <property name="yalign">0.5</property>
+ <property name="xpad">0</property>
+ <property name="ypad">0</property>
+ </widget>
+ <packing>
+ <property name="padding">0</property>
+ <property name="expand">False</property>
+ <property name="fill">False</property>
+ </packing>
+ </child>
+
+ <child>
+ <widget class="GtkEntry" id="entry1">
+ <property name="visible">True</property>
+ <property name="can_focus">True</property>
+ <property name="editable">True</property>
+ <property name="visibility">True</property>
+ <property name="max_length">0</property>
+ <property name="text" translatable="yes"></property>
+ <property name="has_frame">True</property>
+ <property name="invisible_char" translatable="yes">*</property>
+ <property name="activates_default">False</property>
+ </widget>
+ <packing>
+ <property name="padding">0</property>
+ <property name="expand">True</property>
+ <property name="fill">True</property>
+ </packing>
+ </child>
+ </widget>
+ <packing>
+ <property name="padding">0</property>
+ <property name="expand">False</property>
+ <property name="fill">True</property>
+ </packing>
+ </child>
+ </widget>
+ <packing>
+ <property name="padding">0</property>
+ <property name="expand">True</property>
+ <property name="fill">True</property>
+ </packing>
+ </child>
+ </widget>
+ </child>
+</widget>
+
+<widget class="GtkDialog" id="InterpChoiceDialog">
+ <property name="title" translatable="yes">Interpretation choice</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="has_separator">True</property>
+
+ <child internal-child="vbox">
+ <widget class="GtkVBox" id="dialog-vbox4">
+ <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_area4">
+ <property name="visible">True</property>
+ <property name="layout_style">GTK_BUTTONBOX_END</property>
+
+ <child>
+ <widget class="GtkButton" id="InterpChoiceHelpButton">
+ <property name="visible">True</property>
+ <property name="can_default">True</property>
+ <property name="can_focus">True</property>
+ <property name="label">gtk-help</property>
+ <property name="use_stock">True</property>
+ <property name="relief">GTK_RELIEF_NORMAL</property>
+ <property name="response_id">-11</property>
+ </widget>
+ </child>
+
+ <child>
+ <widget class="GtkButton" id="InterpChoiceCancelButton">
+ <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="InterpChoiceOkButton">
+ <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>
+ <widget class="GtkVBox" id="vbox3">
+ <property name="visible">True</property>
+ <property name="homogeneous">False</property>
+ <property name="spacing">0</property>
+
+ <child>
+ <widget class="GtkLabel" id="label6">
+ <property name="visible">True</property>
+ <property name="label" translatable="yes">some informative message here ...</property>
+ <property name="use_underline">False</property>
+ <property name="use_markup">False</property>
+ <property name="justify">GTK_JUSTIFY_LEFT</property>
+ <property name="wrap">False</property>
+ <property name="selectable">False</property>
+ <property name="xalign">0.5</property>
+ <property name="yalign">0.5</property>
+ <property name="xpad">0</property>
+ <property name="ypad">0</property>
+ </widget>
+ <packing>
+ <property name="padding">0</property>
+ <property name="expand">False</property>
+ <property name="fill">False</property>
+ </packing>
+ </child>
+
+ <child>
+ <placeholder/>
+ </child>
+ </widget>
+ <packing>
+ <property name="padding">0</property>
+ <property name="expand">True</property>
+ <property name="fill">True</property>
+ </packing>
+ </child>
+ </widget>
+ </child>
+</widget>
+
</glade-interface>
* http://helm.cs.unibo.it/
*)
- (** quit program, possibly asking for confirmation *)
-let quit () =
- GMain.Main.quit ()
+exception Not_implemented of string
+let not_implemented feature = raise (Not_implemented feature)
- (** 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 _ = Helm_registry.load_from "mathita.conf.xml"
+let _ = GMain.Main.init ()
+let gui = new MathitaGui.gui (Helm_registry.get "mathita.glade_file")
-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 interactive_user_uri_choice
+ ~selection_mode:[`MULTIPLE|`SINGLE] ?(ok="Ok")
+ ?(enable_button_for_non_vars=false) ~title ~msg
+ uris
+=
+ let only_constant_choices =
+ lazy
+ (List.filter
+ (fun uri -> not (String.sub uri (String.length uri - 4) 4 = ".var"))
+ uris)
+ in
+ if selection_mode <> `SINGLE && !auto_disambiguation then
+ Lazy.force only_constant_choices
+ else begin
+ let choices = ref [] in
+ let chosen = ref false in
+ let use_only_constants = ref false in
+ gui#uriChoice#uriChoiceDialog#set_title title;
+ gui#uriChoice#uriChoiceLabel#set_text msg;
+ FINQUI
-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
+ let clist =
+ let expected_height = 18 * List.length uris in
+ let height = if expected_height > 400 then 400 else expected_height in
+ GList.clist ~columns:1 ~packing:scrolled_window#add
+ ~height ~selection_mode:(selection_mode :> Gtk.Tags.selection_mode) () in
+ let _ = List.map (function x -> clist#append [x]) uris in
+ let hbox2 =
+ GPack.hbox ~border_width:0
+ ~packing:(window#vbox#pack ~expand:false ~fill:false ~padding:5) () in
+ let explain_label =
+ GMisc.label ~text:"None of the above. Try this one:"
+ ~packing:(hbox2#pack ~expand:false ~fill:false ~padding:5) () in
+ let manual_input =
+ GEdit.entry ~editable:true
+ ~packing:(hbox2#pack ~expand:true ~fill:true ~padding:5) () in
+ let hbox =
+ GPack.hbox ~border_width:0 ~packing:window#action_area#add () in
+ let okb =
+ GButton.button ~label:ok
+ ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
+ let _ = okb#misc#set_sensitive false in
+ let nonvarsb =
+ GButton.button
+ ~packing:
+ (function w ->
+ if enable_button_for_non_vars then
+ hbox#pack ~expand:false ~fill:false ~padding:5 w)
+ ~label:"Try constants only" () in
+ let autob =
+ GButton.button
+ ~packing:
+ (fun w ->
+ if enable_button_for_non_vars then
+ hbox#pack ~expand:false ~fill:false ~padding:5 w)
+ ~label:"Auto" () in
+ let checkb =
+ GButton.button ~label:"Check"
+ ~packing:(hbox#pack ~padding:5) () in
+ let _ = checkb#misc#set_sensitive false in
+ let cancelb =
+ GButton.button ~label:"Abort"
+ ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
+ (* actions *)
+ let check_callback () =
+ assert (List.length !choices > 0) ;
+ check_window !choices
+ in
+ ignore (window#connect#destroy GMain.Main.quit) ;
+ ignore (cancelb#connect#clicked window#destroy) ;
+ ignore
+ (okb#connect#clicked (function () -> chosen := true ; window#destroy ())) ;
+ ignore
+ (nonvarsb#connect#clicked
+ (function () ->
+ use_only_constants := true ;
+ chosen := true ;
+ window#destroy ()
+ )) ;
+ ignore (autob#connect#clicked (fun () ->
+ auto_disambiguation := true;
+ (rendering_window ())#set_auto_disambiguation true;
+ use_only_constants := true ;
+ chosen := true;
+ window#destroy ()));
+ ignore (checkb#connect#clicked check_callback) ;
+ ignore
+ (clist#connect#select_row
+ (fun ~row ~column ~event ->
+ checkb#misc#set_sensitive true ;
+ okb#misc#set_sensitive true ;
+ choices := (List.nth uris row)::!choices)) ;
+ ignore
+ (clist#connect#unselect_row
+ (fun ~row ~column ~event ->
+ choices :=
+ List.filter (function uri -> uri != (List.nth uris row)) !choices)) ;
+ ignore
+ (manual_input#connect#changed
+ (fun _ ->
+ if manual_input#text = "" then
+ begin
+ choices := [] ;
+ checkb#misc#set_sensitive false ;
+ okb#misc#set_sensitive false ;
+ clist#misc#set_sensitive true
+ end
+ else
+ begin
+ choices := [manual_input#text] ;
+ clist#unselect_all () ;
+ checkb#misc#set_sensitive true ;
+ okb#misc#set_sensitive true ;
+ clist#misc#set_sensitive false
+ end));
+ window#set_position `CENTER ;
+ window#show () ;
+ GtkThread.main ();
+ if !chosen then
+ if !use_only_constants then
+ Lazy.force only_constant_choices
+ else
+ if List.length !choices > 0 then !choices else raise NoChoice
+ else
+ raise NoChoice
+ end
+ ;;
+*)
-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;
- ()
+(*
+module DisambiguateCallbacks =
+ struct
+ let interactive_user_uri_choice =
+ assert false (* TODO *)
+(* interactive_user_uri_choice *)
+ let interactive_interpretation_choice choices =
+ assert false (* TODO *)
+ let input_or_locate_uri ~title =
+ assert false (* TODO *)
end
+*)
+
+ (** quit program, possibly asking for confirmation *)
+let quit () = GMain.Main.quit ()
+let _ = gui#setQuitCallback quit
-let _ =
- let glade_file = "mathita.glade" in
- let _ = GMain.Main.init () in
- let gui = new gui glade_file in
- GtkThread.main ()
+let _ = GtkThread.main ()
--- /dev/null
+(* 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 newMenu =
+ new GMenu.image_menu_item (GtkMenu.ImageMenuItem.cast
+ (Glade.get_widget_msg ~name:"NewMenu" ~info:"GtkImageMenuItem" xmldata))
+ method newMenu = newMenu
+ val image13 =
+ new GMisc.image (GtkMisc.Image.cast
+ (Glade.get_widget_msg ~name:"image13" ~info:"GtkImage" xmldata))
+ method image13 = image13
+ val newMenu_menu =
+ new GMenu.menu (GtkMenu.Menu.cast
+ (Glade.get_widget_msg ~name:"NewMenu_menu" ~info:"GtkMenu" xmldata))
+ method newMenu_menu = newMenu_menu
+ val newProofMenuItem =
+ new GMenu.menu_item (GtkMenu.MenuItem.cast
+ (Glade.get_widget_msg ~name:"NewProofMenuItem" ~info:"GtkMenuItem" xmldata))
+ method newProofMenuItem = newProofMenuItem
+ val newDefsMenuItem =
+ new GMenu.menu_item (GtkMenu.MenuItem.cast
+ (Glade.get_widget_msg ~name:"NewDefsMenuItem" ~info:"GtkMenuItem" xmldata))
+ method newDefsMenuItem = newDefsMenuItem
+ val openMenuItem =
+ new GMenu.image_menu_item (GtkMenu.ImageMenuItem.cast
+ (Glade.get_widget_msg ~name:"OpenMenuItem" ~info:"GtkImageMenuItem" xmldata))
+ method openMenuItem = openMenuItem
+ val image14 =
+ new GMisc.image (GtkMisc.Image.cast
+ (Glade.get_widget_msg ~name:"image14" ~info:"GtkImage" xmldata))
+ method image14 = image14
+ val saveMenuItem =
+ new GMenu.image_menu_item (GtkMenu.ImageMenuItem.cast
+ (Glade.get_widget_msg ~name:"SaveMenuItem" ~info:"GtkImageMenuItem" xmldata))
+ method saveMenuItem = saveMenuItem
+ val image15 =
+ new GMisc.image (GtkMisc.Image.cast
+ (Glade.get_widget_msg ~name:"image15" ~info:"GtkImage" xmldata))
+ method image15 = image15
+ val saveAsMenuItem =
+ new GMenu.image_menu_item (GtkMenu.ImageMenuItem.cast
+ (Glade.get_widget_msg ~name:"SaveAsMenuItem" ~info:"GtkImageMenuItem" xmldata))
+ method saveAsMenuItem = saveAsMenuItem
+ val image16 =
+ new GMisc.image (GtkMisc.Image.cast
+ (Glade.get_widget_msg ~name:"image16" ~info:"GtkImage" xmldata))
+ method image16 = image16
+ val separator1 =
+ new GMenu.menu_item (GtkMenu.MenuItem.cast
+ (Glade.get_widget_msg ~name:"separator1" ~info:"GtkMenuItem" 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 image17 =
+ new GMisc.image (GtkMisc.Image.cast
+ (Glade.get_widget_msg ~name:"image17" ~info:"GtkImage" xmldata))
+ method image17 = image17
+ 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 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 aboutDismissButton =
+ new GButton.button (GtkButton.Button.cast
+ (Glade.get_widget_msg ~name:"AboutDismissButton" ~info:"GtkButton" xmldata))
+ method aboutDismissButton = aboutDismissButton
+ method reparent parent =
+ dialog_vbox2#misc#reparent parent;
+ toplevel#destroy ()
+ method check_widgets () = ()
+ end
+class uriChoiceDialog ?(file="mathita.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
+ (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
+ (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 uriChoiceAbortButton =
+ new GButton.button (GtkButton.Button.cast
+ (Glade.get_widget_msg ~name:"UriChoiceAbortButton" ~info:"GtkButton" xmldata))
+ method uriChoiceAbortButton = uriChoiceAbortButton
+ val uriChoiceSelectedButton =
+ new GButton.button (GtkButton.Button.cast
+ (Glade.get_widget_msg ~name:"UriChoiceSelectedButton" ~info:"GtkButton" xmldata))
+ method uriChoiceSelectedButton = uriChoiceSelectedButton
+ val alignment2 =
+ new GBin.alignment (GtkBin.Alignment.cast
+ (Glade.get_widget_msg ~name:"alignment2" ~info:"GtkAlignment" xmldata))
+ method alignment2 = alignment2
+ val hbox3 =
+ new GPack.box (GtkPack.Box.cast
+ (Glade.get_widget_msg ~name:"hbox3" ~info:"GtkHBox" xmldata))
+ method hbox3 = hbox3
+ val image19 =
+ new GMisc.image (GtkMisc.Image.cast
+ (Glade.get_widget_msg ~name:"image19" ~info:"GtkImage" xmldata))
+ method image19 = image19
+ val label3 =
+ new GMisc.label (GtkMisc.Label.cast
+ (Glade.get_widget_msg ~name:"label3" ~info:"GtkLabel" xmldata))
+ method label3 = label3
+ val uriChoiceConstantsButton =
+ new GButton.button (GtkButton.Button.cast
+ (Glade.get_widget_msg ~name:"UriChoiceConstantsButton" ~info:"GtkButton" xmldata))
+ method uriChoiceConstantsButton = uriChoiceConstantsButton
+ val uriChoiceAutoButton =
+ new GButton.button (GtkButton.Button.cast
+ (Glade.get_widget_msg ~name:"UriChoiceAutoButton" ~info:"GtkButton" xmldata))
+ method uriChoiceAutoButton = uriChoiceAutoButton
+ val alignment1 =
+ new GBin.alignment (GtkBin.Alignment.cast
+ (Glade.get_widget_msg ~name:"alignment1" ~info:"GtkAlignment" xmldata))
+ method alignment1 = alignment1
+ val hbox1 =
+ new GPack.box (GtkPack.Box.cast
+ (Glade.get_widget_msg ~name:"hbox1" ~info:"GtkHBox" xmldata))
+ method hbox1 = hbox1
+ val image18 =
+ new GMisc.image (GtkMisc.Image.cast
+ (Glade.get_widget_msg ~name:"image18" ~info:"GtkImage" xmldata))
+ method image18 = image18
+ val label1 =
+ new GMisc.label (GtkMisc.Label.cast
+ (Glade.get_widget_msg ~name:"label1" ~info:"GtkLabel" xmldata))
+ method label1 = label1
+ val vbox2 =
+ new GPack.box (GtkPack.Box.cast
+ (Glade.get_widget_msg ~name:"vbox2" ~info:"GtkVBox" xmldata))
+ method vbox2 = vbox2
+ val uriChoiceLabel =
+ new GMisc.label (GtkMisc.Label.cast
+ (Glade.get_widget_msg ~name:"UriChoiceLabel" ~info:"GtkLabel" xmldata))
+ method uriChoiceLabel = uriChoiceLabel
+ val scrolledwindow1 =
+ new GBin.scrolled_window (GtkBin.ScrolledWindow.cast
+ (Glade.get_widget_msg ~name:"scrolledwindow1" ~info:"GtkScrolledWindow" xmldata))
+ method scrolledwindow1 = scrolledwindow1
+ val uriChoiceTreeView =
+ new GTree.view (GtkTree.TreeView.cast
+ (Glade.get_widget_msg ~name:"UriChoiceTreeView" ~info:"GtkTreeView" xmldata))
+ method uriChoiceTreeView = uriChoiceTreeView
+ val hbox2 =
+ new GPack.box (GtkPack.Box.cast
+ (Glade.get_widget_msg ~name:"hbox2" ~info:"GtkHBox" xmldata))
+ method hbox2 = hbox2
+ val label2 =
+ new GMisc.label (GtkMisc.Label.cast
+ (Glade.get_widget_msg ~name:"label2" ~info:"GtkLabel" xmldata))
+ method label2 = label2
+ val entry1 =
+ new GEdit.entry (GtkEdit.Entry.cast
+ (Glade.get_widget_msg ~name:"entry1" ~info:"GtkEntry" xmldata))
+ method entry1 = entry1
+ method reparent parent =
+ dialog_vbox3#misc#reparent parent;
+ toplevel#destroy ()
+ method check_widgets () = ()
+ end
+class interpChoiceDialog ?(file="mathita.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
+ (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
+ (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 interpChoiceHelpButton =
+ new GButton.button (GtkButton.Button.cast
+ (Glade.get_widget_msg ~name:"InterpChoiceHelpButton" ~info:"GtkButton" xmldata))
+ method interpChoiceHelpButton = interpChoiceHelpButton
+ val interpChoiceCancelButton =
+ new GButton.button (GtkButton.Button.cast
+ (Glade.get_widget_msg ~name:"InterpChoiceCancelButton" ~info:"GtkButton" xmldata))
+ method interpChoiceCancelButton = interpChoiceCancelButton
+ val interpChoiceOkButton =
+ new GButton.button (GtkButton.Button.cast
+ (Glade.get_widget_msg ~name:"InterpChoiceOkButton" ~info:"GtkButton" xmldata))
+ method interpChoiceOkButton = interpChoiceOkButton
+ val vbox3 =
+ new GPack.box (GtkPack.Box.cast
+ (Glade.get_widget_msg ~name:"vbox3" ~info:"GtkVBox" xmldata))
+ method vbox3 = vbox3
+ val label6 =
+ new GMisc.label (GtkMisc.Label.cast
+ (Glade.get_widget_msg ~name:"label6" ~info:"GtkLabel" xmldata))
+ method label6 = label6
+ method reparent parent =
+ dialog_vbox4#misc#reparent parent;
+ toplevel#destroy ()
+ method check_widgets () = ()
+ end
+
+let check_all ?(show=false) () =
+ ignore (GMain.Main.init ());
+ let interpChoiceDialog = new interpChoiceDialog () in
+ if show then interpChoiceDialog#toplevel#show ();
+ interpChoiceDialog#check_widgets ();
+ let uriChoiceDialog = new uriChoiceDialog () in
+ if show then uriChoiceDialog#toplevel#show ();
+ uriChoiceDialog#check_widgets ();
+ let aboutWin = new aboutWin () in
+ if show then aboutWin#toplevel#show ();
+ aboutWin#check_widgets ();
+ let 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 ()
+;;
--- /dev/null
+class mainWin :
+ ?file:string ->
+ ?domain:string ->
+ ?autoconnect:bool ->
+ unit ->
+ object
+ val aboutMenuItem : GMenu.menu_item
+ val editMenu : GMenu.menu_item
+ val fileMenu : GMenu.menu_item
+ val fileMenu_menu : GMenu.menu
+ val helpMenu : GMenu.menu_item
+ val helpMenu_menu : GMenu.menu
+ val image13 : GMisc.image
+ val image14 : GMisc.image
+ val image15 : GMisc.image
+ val image16 : GMisc.image
+ val image17 : GMisc.image
+ val mainMenuBar : GMenu.menu_shell
+ val mainStatusBar : GMisc.statusbar
+ val mainVPanes : GPack.paned
+ val mainWin : GWindow.window
+ val mainWinShape : GPack.box
+ val newDefsMenuItem : GMenu.menu_item
+ val newMenu : GMenu.image_menu_item
+ val newMenu_menu : GMenu.menu
+ val newProofMenuItem : GMenu.menu_item
+ val openMenuItem : GMenu.image_menu_item
+ val proofStatus : GBin.scrolled_window
+ val quitMenuItem : GMenu.image_menu_item
+ val saveAsMenuItem : GMenu.image_menu_item
+ val saveMenuItem : GMenu.image_menu_item
+ val scrolledUserInput : GBin.scrolled_window
+ val separator1 : GMenu.menu_item
+ val showProofMenuItem : GMenu.check_menu_item
+ val showToolBarMenuItem : GMenu.check_menu_item
+ val toplevel : GWindow.window
+ 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 fileMenu : GMenu.menu_item
+ method fileMenu_menu : GMenu.menu
+ method helpMenu : GMenu.menu_item
+ method helpMenu_menu : GMenu.menu
+ method image13 : GMisc.image
+ method image14 : GMisc.image
+ method image15 : GMisc.image
+ method image16 : GMisc.image
+ method image17 : GMisc.image
+ method mainMenuBar : GMenu.menu_shell
+ method mainStatusBar : GMisc.statusbar
+ method mainVPanes : GPack.paned
+ method mainWin : GWindow.window
+ method mainWinShape : GPack.box
+ method newDefsMenuItem : GMenu.menu_item
+ method newMenu : GMenu.image_menu_item
+ method newMenu_menu : GMenu.menu
+ method newProofMenuItem : GMenu.menu_item
+ method openMenuItem : GMenu.image_menu_item
+ method proofStatus : GBin.scrolled_window
+ method quitMenuItem : GMenu.image_menu_item
+ method reparent : GObj.widget -> unit
+ method saveAsMenuItem : GMenu.image_menu_item
+ method saveMenuItem : GMenu.image_menu_item
+ method scrolledUserInput : GBin.scrolled_window
+ method separator1 : GMenu.menu_item
+ method showProofMenuItem : GMenu.check_menu_item
+ method showToolBarMenuItem : GMenu.check_menu_item
+ method toplevel : GWindow.window
+ 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 aboutDismissButton : GButton.button
+ val aboutWin : [ `DELETE_EVENT | `ID of int | `NONE ] GWindow.dialog
+ val dialog_vbox2 : GPack.box
+ val toplevel : [ `DELETE_EVENT | `ID of int | `NONE ] GWindow.dialog
+ val xml : Glade.glade_xml Gtk.obj
+ method aboutDismissButton : GButton.button
+ 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 reparent : GObj.widget -> unit
+ method toplevel : [ `DELETE_EVENT | `ID of int | `NONE ] GWindow.dialog
+ method xml : Glade.glade_xml Gtk.obj
+ end
+class uriChoiceDialog :
+ ?file:string ->
+ ?domain:string ->
+ ?autoconnect:bool ->
+ unit ->
+ object
+ val alignment1 : GBin.alignment
+ val alignment2 : GBin.alignment
+ val dialog_vbox3 : GPack.box
+ val entry1 : GEdit.entry
+ val hbox1 : GPack.box
+ val hbox2 : GPack.box
+ val hbox3 : GPack.box
+ val image18 : GMisc.image
+ val image19 : GMisc.image
+ val label1 : GMisc.label
+ val label2 : GMisc.label
+ val label3 : GMisc.label
+ val scrolledwindow1 : GBin.scrolled_window
+ val toplevel : [ `DELETE_EVENT | `ID of int | `NONE ] GWindow.dialog
+ val uriChoiceAbortButton : GButton.button
+ val uriChoiceAutoButton : GButton.button
+ val uriChoiceConstantsButton : GButton.button
+ val uriChoiceDialog :
+ [ `DELETE_EVENT | `ID of int | `NONE ] GWindow.dialog
+ val uriChoiceLabel : GMisc.label
+ val uriChoiceSelectedButton : GButton.button
+ val uriChoiceTreeView : GTree.view
+ val vbox2 : GPack.box
+ val xml : Glade.glade_xml Gtk.obj
+ method alignment1 : GBin.alignment
+ method alignment2 : GBin.alignment
+ method bind : name:string -> callback:(unit -> unit) -> unit
+ method check_widgets : unit -> unit
+ method dialog_vbox3 : GPack.box
+ method entry1 : GEdit.entry
+ method hbox1 : GPack.box
+ method hbox2 : GPack.box
+ method hbox3 : GPack.box
+ method image18 : GMisc.image
+ method image19 : GMisc.image
+ method label1 : GMisc.label
+ method label2 : GMisc.label
+ method label3 : GMisc.label
+ method reparent : GObj.widget -> unit
+ method scrolledwindow1 : GBin.scrolled_window
+ method toplevel : [ `DELETE_EVENT | `ID of int | `NONE ] GWindow.dialog
+ method uriChoiceAbortButton : GButton.button
+ method uriChoiceAutoButton : GButton.button
+ method uriChoiceConstantsButton : GButton.button
+ method uriChoiceDialog :
+ [ `DELETE_EVENT | `ID of int | `NONE ] GWindow.dialog
+ method uriChoiceLabel : GMisc.label
+ method uriChoiceSelectedButton : GButton.button
+ method uriChoiceTreeView : GTree.view
+ method vbox2 : GPack.box
+ method xml : Glade.glade_xml Gtk.obj
+ end
+class interpChoiceDialog :
+ ?file:string ->
+ ?domain:string ->
+ ?autoconnect:bool ->
+ unit ->
+ object
+ val dialog_vbox4 : GPack.box
+ val interpChoiceCancelButton : GButton.button
+ val interpChoiceDialog :
+ [ `DELETE_EVENT | `ID of int | `NONE ] GWindow.dialog
+ val interpChoiceHelpButton : GButton.button
+ val interpChoiceOkButton : GButton.button
+ val label6 : GMisc.label
+ val toplevel : [ `DELETE_EVENT | `ID of int | `NONE ] GWindow.dialog
+ val vbox3 : GPack.box
+ val xml : Glade.glade_xml Gtk.obj
+ method bind : name:string -> callback:(unit -> unit) -> unit
+ method check_widgets : unit -> unit
+ method dialog_vbox4 : GPack.box
+ method interpChoiceCancelButton : GButton.button
+ method interpChoiceDialog :
+ [ `DELETE_EVENT | `ID of int | `NONE ] GWindow.dialog
+ method interpChoiceHelpButton : GButton.button
+ method interpChoiceOkButton : GButton.button
+ method label6 : GMisc.label
+ method reparent : GObj.widget -> unit
+ method toplevel : [ `DELETE_EVENT | `ID of int | `NONE ] GWindow.dialog
+ method vbox3 : GPack.box
+ method xml : Glade.glade_xml Gtk.obj
+ end
+val check_all : ?show:bool -> unit -> unit
--- /dev/null
+(* 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/
+ *)
+
+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: GMenu.check_menu_item option) (win: GWindow.window) () =
+ 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_binding key callback (evbox: GBin.event_box) =
+ ignore (evbox#event#connect#key_press (function
+ | key' when GdkEvent.Key.keyval key' = key ->
+ callback ();
+ false
+ | _ -> false))
+
--- /dev/null
+(* 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/
+ *)
+
+(** {2 Gtk helpers} *)
+
+ (** 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 *)
+val toggle_visibility:
+ win:GWindow.window -> check:GMenu.check_menu_item -> unit
+
+val toggle_win:
+ ?check:GMenu.check_menu_item -> GWindow.window -> (unit -> unit)
+
+val add_key_binding: Gdk.keysym -> (unit -> 'a) -> GBin.event_box -> unit
+
-(* 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 () = ()
- 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
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
+
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 ()
-;;
+++ /dev/null
-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
projects / helm.git / commitdiff