From ca8cb7b6303e56a91823b2a14891d7de0b0d4130 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Tue, 24 Feb 2004 17:30:06 +0000 Subject: [PATCH] snapshot --- helm/mathita/.depend | 10 +- helm/mathita/Makefile | 12 +- helm/mathita/mathita.conf.xml.sample | 7 + helm/mathita/mathita.glade | 562 +++++++++++++++++- helm/mathita/mathita.ml | 203 +++++-- helm/mathita/mathitaGeneratedGui.ml | 452 ++++++++++++++ ...mathitaGui.mli => mathitaGeneratedGui.mli} | 124 +++- helm/mathita/mathitaGtkMisc.ml | 46 ++ helm/mathita/mathitaGtkMisc.mli | 37 ++ helm/mathita/mathitaGui.ml | 341 +++-------- 10 files changed, 1447 insertions(+), 347 deletions(-) create mode 100644 helm/mathita/mathita.conf.xml.sample create mode 100644 helm/mathita/mathitaGeneratedGui.ml rename helm/mathita/{mathitaGui.mli => mathitaGeneratedGui.mli} (55%) create mode 100644 helm/mathita/mathitaGtkMisc.ml create mode 100644 helm/mathita/mathitaGtkMisc.mli diff --git a/helm/mathita/.depend b/helm/mathita/.depend index d55a5e488..33e1356a1 100644 --- a/helm/mathita/.depend +++ b/helm/mathita/.depend @@ -1,4 +1,8 @@ -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 diff --git a/helm/mathita/Makefile b/helm/mathita/Makefile index 02b52eab3..59cbbea6f 100644 --- a/helm/mathita/Makefile +++ b/helm/mathita/Makefile @@ -1,6 +1,6 @@ OCAMLFIND = ocamlfind -REQUIRES = lablgtk2.glade +REQUIRES = lablgtk2.glade helm-registry OCAML_FLAGS = -package "$(REQUIRES)" -pp camlp4o OCAML_THREADS_FLAGS = -thread OCAML_DEBUG_FLAGS = @@ -9,6 +9,8 @@ OCAMLOPT = $(OCAMLFIND) opt $(OCAML_FLAGS) $(OCAML_THREADS_FLAGS) $(OCAML_DEBUG_ OCAMLDEP = $(OCAMLFIND) ocamldep $(OCAML_FLAGS) LABLGLADECC = lablgladecc2 CMOS = \ + mathitaGeneratedGui.cmo \ + mathitaGtkMisc.cmo \ mathitaGui.cmo all: mathita @@ -16,9 +18,9 @@ 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 $< @@ -32,9 +34,9 @@ mathitaGui.ml mathitaGui.mli: mathita.glade 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 diff --git a/helm/mathita/mathita.conf.xml.sample b/helm/mathita/mathita.conf.xml.sample new file mode 100644 index 000000000..e9d4576b1 --- /dev/null +++ b/helm/mathita/mathita.conf.xml.sample @@ -0,0 +1,7 @@ + + +
+ mathita.glade + true +
+ diff --git a/helm/mathita/mathita.glade b/helm/mathita/mathita.glade index a1150cfbc..9f5a5f4f6 100644 --- a/helm/mathita/mathita.glade +++ b/helm/mathita/mathita.glade @@ -25,20 +25,142 @@ True - + True _File True - + - + True - Exit + _New + True + + + + True + gtk-new + 1 + 0.5 + 0.5 + 0 + 0 + + + + + + + + + True + _Proof or definition ... + True + + + + + + + True + (Co)Inductive _definitions ... + True + + + + + + + + + + True + _Open... + True + + + + + True + gtk-open + 1 + 0.5 + 0.5 + 0 + 0 + + + + + + + + True + _Save + True + + + + + True + gtk-save + 1 + 0.5 + 0.5 + 0 + 0 + + + + + + + + True + Save _As ... + True + + + + True + gtk-save-as + 1 + 0.5 + 0.5 + 0 + 0 + + + + + + + + True + + + + + + True + _Quit True + + + + True + gtk-quit + 1 + 0.5 + 0.5 + 0 + 0 + + @@ -147,21 +269,7 @@ GTK_CORNER_TOP_LEFT - - True - True - False - GTK_JUSTIFY_LEFT - GTK_WRAP_WORD - True - 0 - 0 - 0 - 0 - 0 - 0 - - + @@ -234,7 +342,7 @@ 10 Select File GTK_WINDOW_TOPLEVEL - GTK_WIN_POS_NONE + GTK_WIN_POS_CENTER True True False @@ -361,7 +469,7 @@ DUMMY GTK_WINDOW_TOPLEVEL - GTK_WIN_POS_NONE + GTK_WIN_POS_CENTER True False False @@ -420,7 +528,7 @@ Mathita: about GTK_WINDOW_TOPLEVEL - GTK_WIN_POS_NONE + GTK_WIN_POS_CENTER True False False @@ -438,7 +546,7 @@ GTK_BUTTONBOX_END - + True True True @@ -464,4 +572,412 @@ + + 280 + True + Uri choice + GTK_WINDOW_TOPLEVEL + GTK_WIN_POS_CENTER + True + True + False + True + + + + True + False + 0 + + + + True + GTK_BUTTONBOX_END + + + + True + True + True + gtk-cancel + True + GTK_RELIEF_NORMAL + -6 + + + + + + True + True + True + GTK_RELIEF_NORMAL + 0 + + + + True + 0.5 + 0.5 + 0 + 0 + + + + True + False + 2 + + + + True + gtk-index + 4 + 0.5 + 0.5 + 0 + 0 + + + 0 + False + False + + + + + + True + Try _Selected + True + False + GTK_JUSTIFY_LEFT + False + False + 0.5 + 0.5 + 0 + 0 + + + 0 + False + False + + + + + + + + + + + + True + True + True + Try Constants + True + GTK_RELIEF_NORMAL + 0 + + + + + + True + True + True + GTK_RELIEF_NORMAL + 0 + + + + True + 0.5 + 0.5 + 0 + 0 + + + + True + False + 2 + + + + True + gtk-ok + 4 + 0.5 + 0.5 + 0 + 0 + + + 0 + False + False + + + + + + True + _Auto + True + False + GTK_JUSTIFY_LEFT + False + False + 0.5 + 0.5 + 0 + 0 + + + 0 + False + False + + + + + + + + + + + 0 + False + True + GTK_PACK_END + + + + + + True + False + 0 + + + + True + some informative message here ... + False + False + GTK_JUSTIFY_LEFT + False + False + 0.5 + 0.5 + 0 + 0 + + + 0 + False + False + + + + + + True + True + GTK_POLICY_ALWAYS + GTK_POLICY_ALWAYS + GTK_SHADOW_NONE + GTK_CORNER_TOP_LEFT + + + + True + True + False + False + False + True + + + + + 0 + True + True + + + + + + True + False + 0 + + + + True + URI: + False + False + GTK_JUSTIFY_LEFT + False + False + 0.5 + 0.5 + 0 + 0 + + + 0 + False + False + + + + + + True + True + True + True + 0 + + True + * + False + + + 0 + True + True + + + + + 0 + False + True + + + + + 0 + True + True + + + + + + + + Interpretation choice + GTK_WINDOW_TOPLEVEL + GTK_WIN_POS_NONE + True + True + False + True + + + + True + False + 0 + + + + True + GTK_BUTTONBOX_END + + + + True + True + True + gtk-help + True + GTK_RELIEF_NORMAL + -11 + + + + + + True + True + True + gtk-cancel + True + GTK_RELIEF_NORMAL + -6 + + + + + + True + True + True + gtk-ok + True + GTK_RELIEF_NORMAL + -5 + + + + + 0 + False + True + GTK_PACK_END + + + + + + True + False + 0 + + + + True + some informative message here ... + False + False + GTK_JUSTIFY_LEFT + False + False + 0.5 + 0.5 + 0 + 0 + + + 0 + False + False + + + + + + + + + 0 + True + True + + + + + + diff --git a/helm/mathita/mathita.ml b/helm/mathita/mathita.ml index 0d3b622ff..b1cfaddcc 100644 --- a/helm/mathita/mathita.ml +++ b/helm/mathita/mathita.ml @@ -23,64 +23,159 @@ * 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 :> 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 () diff --git a/helm/mathita/mathitaGeneratedGui.ml b/helm/mathita/mathitaGeneratedGui.ml new file mode 100644 index 000000000..f09c13a11 --- /dev/null +++ b/helm/mathita/mathitaGeneratedGui.ml @@ -0,0 +1,452 @@ +(* 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 () +;; diff --git a/helm/mathita/mathitaGui.mli b/helm/mathita/mathitaGeneratedGui.mli similarity index 55% rename from helm/mathita/mathitaGui.mli rename to helm/mathita/mathitaGeneratedGui.mli index 2f8416c3b..8fa10245f 100644 --- a/helm/mathita/mathitaGui.mli +++ b/helm/mathita/mathitaGeneratedGui.mli @@ -6,22 +6,34 @@ class mainWin : 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 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 userInput : GText.view val viewMenu : GMenu.menu_item val viewMenu_menu : GMenu.menu val xml : Glade.glade_xml Gtk.obj @@ -29,23 +41,35 @@ class mainWin : 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 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 userInput : GText.view method viewMenu : GMenu.menu_item method viewMenu_menu : GMenu.menu method xml : Glade.glade_xml Gtk.obj @@ -148,18 +172,106 @@ class aboutWin : ?autoconnect:bool -> unit -> object + val aboutDismissButton : GButton.button 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 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 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 +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 diff --git a/helm/mathita/mathitaGtkMisc.ml b/helm/mathita/mathitaGtkMisc.ml new file mode 100644 index 000000000..36478d529 --- /dev/null +++ b/helm/mathita/mathitaGtkMisc.ml @@ -0,0 +1,46 @@ +(* 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)) + diff --git a/helm/mathita/mathitaGtkMisc.mli b/helm/mathita/mathitaGtkMisc.mli new file mode 100644 index 000000000..987ad1857 --- /dev/null +++ b/helm/mathita/mathitaGtkMisc.mli @@ -0,0 +1,37 @@ +(* 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 + diff --git a/helm/mathita/mathitaGui.ml b/helm/mathita/mathitaGui.ml index b11877a11..cda4a474f 100644 --- a/helm/mathita/mathitaGui.ml +++ b/helm/mathita/mathitaGui.ml @@ -1,260 +1,89 @@ -(* 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 :> 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 () -;; -- 2.39.2