From: Stefano Zacchiroli Date: Tue, 20 Apr 2004 09:27:36 +0000 (+0000) Subject: renamed mathita to matita X-Git-Tag: dead_dir_walking~26 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=c5d4ad1c98c1434b95a8a9b1c8697dd36cf39623;p=helm.git renamed mathita to matita --- diff --git a/helm/mathita/.cvsignore b/helm/mathita/.cvsignore deleted file mode 100644 index bba30b067..000000000 --- a/helm/mathita/.cvsignore +++ /dev/null @@ -1,4 +0,0 @@ -mathita -*.cm[aiox] -*.cmxa -*.[ao] diff --git a/helm/mathita/.depend b/helm/mathita/.depend deleted file mode 100644 index 1fea79aff..000000000 --- a/helm/mathita/.depend +++ /dev/null @@ -1,9 +0,0 @@ -mathitaGeneratedGui.cmo: mathitaGeneratedGui.cmi -mathitaGeneratedGui.cmx: mathitaGeneratedGui.cmi -mathitaGtkMisc.cmo: mathitaGtkMisc.cmi -mathitaGtkMisc.cmx: mathitaGtkMisc.cmi -mathitaGui.cmo: mathitaGeneratedGui.cmi mathitaGtkMisc.cmi mathitaGui.cmi -mathitaGui.cmx: mathitaGeneratedGui.cmx mathitaGtkMisc.cmx mathitaGui.cmi -mathita.cmo: mathitaGeneratedGui.cmi mathitaGui.cmi -mathita.cmx: mathitaGeneratedGui.cmx mathitaGui.cmx -mathitaGui.cmi: mathitaGeneratedGui.cmi mathitaGtkMisc.cmi diff --git a/helm/mathita/Makefile b/helm/mathita/Makefile deleted file mode 100644 index 59cbbea6f..000000000 --- a/helm/mathita/Makefile +++ /dev/null @@ -1,43 +0,0 @@ - -OCAMLFIND = ocamlfind -REQUIRES = lablgtk2.glade helm-registry -OCAML_FLAGS = -package "$(REQUIRES)" -pp camlp4o -OCAML_THREADS_FLAGS = -thread -OCAML_DEBUG_FLAGS = -OCAMLC = $(OCAMLFIND) ocamlc $(OCAML_FLAGS) $(OCAML_THREADS_FLAGS) $(OCAML_DEBUG_FLAGS) -OCAMLOPT = $(OCAMLFIND) opt $(OCAML_FLAGS) $(OCAML_THREADS_FLAGS) $(OCAML_DEBUG_FLAGS) -OCAMLDEP = $(OCAMLFIND) ocamldep $(OCAML_FLAGS) -LABLGLADECC = lablgladecc2 -CMOS = \ - mathitaGeneratedGui.cmo \ - mathitaGtkMisc.cmo \ - mathitaGui.cmo - -all: mathita - -mathita: $(CMOS) mathita.ml - $(OCAMLC) -linkpkg -o $@ $^ - -mathitaGeneratedGui.ml mathitaGeneratedGui.mli: mathita.glade - $(LABLGLADECC) $< > $@ - $(OCAMLC) -i mathitaGeneratedGui.ml > mathitaGeneratedGui.mli - -%.cmi: %.mli - $(OCAMLC) -c $< -%.cmo %.cmi: %.ml - $(OCAMLC) -c $< -%.cmx: %.ml - $(OCAMLOPT) -c $< -%.ml %.mli: %.mly - $(OCAMLYACC) $< - -clean: - rm -rf *.cm[aoix] *.cmxa *.[ao] mathita -distclean: clean - rm -f mathitaGeneratedGui.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 deleted file mode 100644 index e9d4576b1..000000000 --- a/helm/mathita/mathita.conf.xml.sample +++ /dev/null @@ -1,7 +0,0 @@ - - -
- mathita.glade - true -
- diff --git a/helm/mathita/mathita.glade b/helm/mathita/mathita.glade deleted file mode 100644 index cc299bad6..000000000 --- a/helm/mathita/mathita.glade +++ /dev/null @@ -1,1080 +0,0 @@ - - - - - - - True - Mathita - GTK_WINDOW_TOPLEVEL - GTK_WIN_POS_NONE - False - 800 - 600 - True - False - - - - True - False - 0 - - - - True - - - - True - _File - True - - - - - - - True - _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 - - - - - - - - - - - - True - _Edit - True - - - - - - True - _View - True - - - - - - - True - Show Button Bar - True - True - - - - - - True - Show Proof Window - True - False - - - - - - - - - - - True - Debug - True - - - - - - - True - 0 - True - - - - - - True - 1 - True - - - - - - True - 2 - True - - - - - - - - - - True - _Help - True - - - - - - - True - About... - True - - - - - - - - - 0 - False - False - - - - - - True - True - 450 - - - - True - GTK_POLICY_ALWAYS - GTK_POLICY_ALWAYS - GTK_SHADOW_NONE - GTK_CORNER_TOP_LEFT - - - - - - - True - False - - - - - - True - GTK_POLICY_NEVER - GTK_POLICY_ALWAYS - GTK_SHADOW_IN - GTK_CORNER_TOP_LEFT - - - - - - - True - True - - - - - 0 - True - True - - - - - - True - True - - - 0 - False - False - - - - - - - - Mathita: current proof - GTK_WINDOW_TOPLEVEL - GTK_WIN_POS_NONE - False - 700 - 525 - True - False - - - - True - - - - True - GTK_POLICY_ALWAYS - GTK_POLICY_ALWAYS - GTK_SHADOW_NONE - GTK_CORNER_TOP_LEFT - - - - True - GTK_SHADOW_IN - - - - - - - - - - - - - - 10 - Select File - GTK_WINDOW_TOPLEVEL - GTK_WIN_POS_CENTER - True - True - False - True - - - - True - True - True - GTK_RELIEF_NORMAL - - - - - - True - True - True - GTK_RELIEF_NORMAL - - - - - - 130 - 450 - True - ToolBar - GTK_WINDOW_TOPLEVEL - GTK_WIN_POS_NONE - False - False - False - - - - True - - - - True - False - 0 - - - - True - GTK_BUTTONBOX_DEFAULT_STYLE - 0 - - - - 120 - True - True - True - button1 - True - GTK_RELIEF_NORMAL - - - - - - True - True - True - button2 - True - GTK_RELIEF_NORMAL - - - - - - True - True - True - button3 - True - GTK_RELIEF_NORMAL - - - - - - True - True - True - button4 - True - GTK_RELIEF_NORMAL - - - - - 0 - False - True - - - - - - True - - - 5 - False - True - - - - - - - - - - - - - - DUMMY - GTK_WINDOW_TOPLEVEL - GTK_WIN_POS_CENTER - True - False - False - True - - - - True - False - 0 - - - - True - GTK_BUTTONBOX_END - - - - 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 - - - - - - - - - - - - Mathita: about - GTK_WINDOW_TOPLEVEL - GTK_WIN_POS_CENTER - True - False - False - True - - - - True - False - 0 - - - - True - GTK_BUTTONBOX_END - - - - True - True - True - gtk-ok - True - GTK_RELIEF_NORMAL - -5 - - - - - 0 - False - True - GTK_PACK_END - - - - - - - - - - - - 280 - 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 - False - 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 - - - - - - - - True - dialog1 - GTK_WINDOW_TOPLEVEL - GTK_WIN_POS_NONE - 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-ok - True - GTK_RELIEF_NORMAL - -5 - - - - - 0 - False - True - GTK_PACK_END - - - - - - - - - - - diff --git a/helm/mathita/mathita.gladep b/helm/mathita/mathita.gladep deleted file mode 100644 index 996d23c10..000000000 --- a/helm/mathita/mathita.gladep +++ /dev/null @@ -1,8 +0,0 @@ - - - - - Mathita - mathita - FALSE - diff --git a/helm/mathita/mathita.ml b/helm/mathita/mathita.ml deleted file mode 100644 index f22a035a5..000000000 --- a/helm/mathita/mathita.ml +++ /dev/null @@ -1,154 +0,0 @@ -(* 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/ - *) - -exception Not_implemented of string -let not_implemented feature = raise (Not_implemented feature) - - (** exceptions whose content should be presented to the user *) -exception Failure of string -let error s = raise (Failure s) - -let _ = Helm_registry.load_from "mathita.conf.xml" -let _ = GMain.Main.init () -let gui = new MathitaGui.gui (Helm_registry.get "mathita.glade_file") - -let interactive_user_uri_choice - ~(selection_mode:[`MULTIPLE|`SINGLE]) ?(nonvars_button=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) && - (Helm_registry.get_bool "mathita.auto_disambiguation") - then - Lazy.force only_constant_choices - else begin - let win = gui#uriChoice in - let choices = ref [] in - let chosen = ref false in - let use_only_constants = ref false in - win#uriChoiceDialog#set_title title; - win#uriChoiceLabel#set_text msg; - gui#uriChoices#list_store#clear (); - List.iter gui#uriChoices#easy_append uris; - win#uriChoiceConstantsButton#misc#set_sensitive nonvars_button; - let bye = ref (fun () -> ()) in - let id1 = - win#uriChoiceConstantsButton#connect#clicked (fun _ -> - use_only_constants := true; - !bye ()) - in - let id2 = - win#uriChoiceAutoButton#connect#clicked (fun _ -> - use_only_constants := true ; - Helm_registry.set_bool "mathita.auto_disambiguation" true; - !bye ()) - in - let id3 = - win#uriChoiceSelectedButton#connect#clicked (fun _ -> - choices := gui#uriChoices#easy_selection (); - !bye ()) - in - bye := (fun () -> - win#uriChoiceDialog#misc#hide (); - win#uriChoiceConstantsButton#misc#disconnect id1; - win#uriChoiceAutoButton#misc#disconnect id2; - win#uriChoiceSelectedButton#misc#disconnect id3; - prerr_endline "quit"; - GMain.Main.quit ()); - win#uriChoiceDialog#show (); - GtkThread.main (); - if !use_only_constants then - Lazy.force only_constant_choices - else - match !choices with - | [] -> error "No choice" - | choices -> choices - end - -(* -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 -*) - -let debugDialog () = - let dialog = - new MathitaGeneratedGui.debug - ~file:(Helm_registry.get "mathita.glade_file") () - in - let retval = ref None in - let return v = - retval := Some v; - dialog#debug#destroy (); - GMain.Main.quit () - in - ignore (dialog#debug#event#connect#delete (fun _ -> true)); - ignore (dialog#okbutton2#connect#clicked (fun _ -> return 1)); - ignore (dialog#cancelbutton2#connect#clicked (fun _ -> return 2)); - dialog#debug#show (); - GtkThread.main (); - (match !retval with None -> assert false | Some v -> v) - -let _ = - gui#main#debugMenuItem2#connect#activate (fun _ -> - prerr_endline (string_of_int (debugDialog ()))) - - (** quit program, possibly asking for confirmation *) -let quit () = GMain.Main.quit () -let _ = gui#setQuitCallback quit -let _ = - gui#main#debugMenuItem0#connect#activate (fun _ -> - let uris = - interactive_user_uri_choice - ~selection_mode:`MULTIPLE - ~nonvars_button:false - ~title:"titolo" - ~msg:"messaggio" - ["cic:/uno.con"; "cic:/due.var"; "cic:/tre.con"; "cic:/quattro.con"; - "cic:/cinque.var"] - in - List.iter prerr_endline uris; print_newline ()) -let _ = - gui#main#debugMenuItem1#connect#activate (fun _ -> - Helm_registry.set_bool "mathita.auto_disambiguation" - (not (Helm_registry.get_bool "mathita.auto_disambiguation"))) - -let _ = -(* gui#uriChoices#easy_append "pippo"; *) -(* gui#uriChoices#list_store#clear (); *) - GtkThread.main () - diff --git a/helm/mathita/mathitaGeneratedGui.ml b/helm/mathita/mathitaGeneratedGui.ml deleted file mode 100644 index 2b2e03ded..000000000 --- a/helm/mathita/mathitaGeneratedGui.ml +++ /dev/null @@ -1,504 +0,0 @@ -(* 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 image40 = - new GMisc.image (GtkMisc.Image.cast - (Glade.get_widget_msg ~name:"image40" ~info:"GtkImage" xmldata)) - method image40 = image40 - 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 image41 = - new GMisc.image (GtkMisc.Image.cast - (Glade.get_widget_msg ~name:"image41" ~info:"GtkImage" xmldata)) - method image41 = image41 - val saveMenuItem = - new GMenu.image_menu_item (GtkMenu.ImageMenuItem.cast - (Glade.get_widget_msg ~name:"SaveMenuItem" ~info:"GtkImageMenuItem" xmldata)) - method saveMenuItem = saveMenuItem - val image42 = - new GMisc.image (GtkMisc.Image.cast - (Glade.get_widget_msg ~name:"image42" ~info:"GtkImage" xmldata)) - method image42 = image42 - val saveAsMenuItem = - new GMenu.image_menu_item (GtkMenu.ImageMenuItem.cast - (Glade.get_widget_msg ~name:"SaveAsMenuItem" ~info:"GtkImageMenuItem" xmldata)) - method saveAsMenuItem = saveAsMenuItem - val image43 = - new GMisc.image (GtkMisc.Image.cast - (Glade.get_widget_msg ~name:"image43" ~info:"GtkImage" xmldata)) - method image43 = image43 - 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 image44 = - new GMisc.image (GtkMisc.Image.cast - (Glade.get_widget_msg ~name:"image44" ~info:"GtkImage" xmldata)) - method image44 = image44 - 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 debugMenu = - new GMenu.menu_item (GtkMenu.MenuItem.cast - (Glade.get_widget_msg ~name:"DebugMenu" ~info:"GtkMenuItem" xmldata)) - method debugMenu = debugMenu - val debugMenu_menu = - new GMenu.menu (GtkMenu.Menu.cast - (Glade.get_widget_msg ~name:"DebugMenu_menu" ~info:"GtkMenu" xmldata)) - method debugMenu_menu = debugMenu_menu - val debugMenuItem0 = - new GMenu.menu_item (GtkMenu.MenuItem.cast - (Glade.get_widget_msg ~name:"DebugMenuItem0" ~info:"GtkMenuItem" xmldata)) - method debugMenuItem0 = debugMenuItem0 - val debugMenuItem1 = - new GMenu.menu_item (GtkMenu.MenuItem.cast - (Glade.get_widget_msg ~name:"DebugMenuItem1" ~info:"GtkMenuItem" xmldata)) - method debugMenuItem1 = debugMenuItem1 - val debugMenuItem2 = - new GMenu.menu_item (GtkMenu.MenuItem.cast - (Glade.get_widget_msg ~name:"DebugMenuItem2" ~info:"GtkMenuItem" xmldata)) - method debugMenuItem2 = debugMenuItem2 - 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 -class debug ?(file="mathita.glade") ?domain ?autoconnect(*=true*) () = - let xmldata = Glade.create ~file ~root:"Debug" ?domain () in - object (self) - inherit Glade.xml ?autoconnect xmldata - val toplevel : [`NONE | `DELETE_EVENT | `ID of int] GWindow.dialog = - new GWindow.dialog (GtkWindow.Dialog.cast - (Glade.get_widget_msg ~name:"Debug" ~info:"GtkDialog" xmldata)) - method toplevel = toplevel - val debug : [`NONE | `DELETE_EVENT | `ID of int] GWindow.dialog = - new GWindow.dialog (GtkWindow.Dialog.cast - (Glade.get_widget_msg ~name:"Debug" ~info:"GtkDialog" xmldata)) - method debug = debug - val dialog_vbox5 = - new GPack.box (GtkPack.Box.cast - (Glade.get_widget_msg ~name:"dialog-vbox5" ~info:"GtkVBox" xmldata)) - method dialog_vbox5 = dialog_vbox5 - val cancelbutton2 = - new GButton.button (GtkButton.Button.cast - (Glade.get_widget_msg ~name:"cancelbutton2" ~info:"GtkButton" xmldata)) - method cancelbutton2 = cancelbutton2 - val okbutton2 = - new GButton.button (GtkButton.Button.cast - (Glade.get_widget_msg ~name:"okbutton2" ~info:"GtkButton" xmldata)) - method okbutton2 = okbutton2 - method reparent parent = - dialog_vbox5#misc#reparent parent; - toplevel#destroy () - method check_widgets () = () - end - -let check_all ?(show=false) () = - ignore (GMain.Main.init ()); - let debug = new debug () in - if show then debug#toplevel#show (); - debug#check_widgets (); - let 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/mathitaGeneratedGui.mli b/helm/mathita/mathitaGeneratedGui.mli deleted file mode 100644 index 6b72a8b27..000000000 --- a/helm/mathita/mathitaGeneratedGui.mli +++ /dev/null @@ -1,309 +0,0 @@ -class mainWin : - ?file:string -> - ?domain:string -> - ?autoconnect:bool -> - unit -> - object - val aboutMenuItem : GMenu.menu_item - val debugMenu : GMenu.menu_item - val debugMenuItem0 : GMenu.menu_item - val debugMenuItem1 : GMenu.menu_item - val debugMenuItem2 : GMenu.menu_item - val debugMenu_menu : GMenu.menu - 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 image40 : GMisc.image - val image41 : GMisc.image - val image42 : GMisc.image - val image43 : GMisc.image - val image44 : 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 debugMenu : GMenu.menu_item - method debugMenuItem0 : GMenu.menu_item - method debugMenuItem1 : GMenu.menu_item - method debugMenuItem2 : GMenu.menu_item - method debugMenu_menu : GMenu.menu - 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 image40 : GMisc.image - method image41 : GMisc.image - method image42 : GMisc.image - method image43 : GMisc.image - method image44 : 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 -class debug : - ?file:string -> - ?domain:string -> - ?autoconnect:bool -> - unit -> - object - val cancelbutton2 : GButton.button - val debug : [ `DELETE_EVENT | `ID of int | `NONE ] GWindow.dialog - val dialog_vbox5 : GPack.box - val okbutton2 : 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 cancelbutton2 : GButton.button - method check_widgets : unit -> unit - method debug : [ `DELETE_EVENT | `ID of int | `NONE ] GWindow.dialog - method dialog_vbox5 : 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 diff --git a/helm/mathita/mathitaGtkMisc.ml b/helm/mathita/mathitaGtkMisc.ml deleted file mode 100644 index fc4fecc8f..000000000 --- a/helm/mathita/mathitaGtkMisc.ml +++ /dev/null @@ -1,77 +0,0 @@ -(* 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)) - -class stringListModel (tree_view: GTree.view) = - let column_list = new GTree.column_list in - let text_column = column_list#add Gobject.Data.string in - let list_store = GTree.list_store column_list in - object (self) - - initializer - let renderer = (GTree.cell_renderer_text [], ["text", text_column]) in - let view_column = GTree.view_column ~renderer () in - tree_view#set_model (Some (list_store :> GTree.model)); - ignore (tree_view#append_column view_column) - - method list_store = list_store - - method easy_append s = - let tree_iter = list_store#append () in - list_store#set ~row:tree_iter ~column:text_column s - - method easy_insert pos s = - let tree_iter = list_store#insert pos in - list_store#set ~row:tree_iter ~column:text_column s - - method easy_selection () = - List.map - (fun tree_path -> - let iter = list_store#get_iter tree_path in - list_store#get ~row:iter ~column:text_column) - tree_view#selection#get_selected_rows - - end - diff --git a/helm/mathita/mathitaGtkMisc.mli b/helm/mathita/mathitaGtkMisc.mli deleted file mode 100644 index 03847ac87..000000000 --- a/helm/mathita/mathitaGtkMisc.mli +++ /dev/null @@ -1,48 +0,0 @@ -(* 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 - - (** single string column list *) -class stringListModel: - GTree.view -> - object - method list_store: GTree.list_store (** list_store forwarding *) - - method easy_append: string -> unit (** append + set *) - method easy_insert: int -> string -> unit (** insert + set *) - method easy_selection: unit -> string list - end - diff --git a/helm/mathita/mathitaGui.ml b/helm/mathita/mathitaGui.ml deleted file mode 100644 index 957c5edcc..000000000 --- a/helm/mathita/mathitaGui.ml +++ /dev/null @@ -1,110 +0,0 @@ -(* 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 stringListModel' uriChoiceDialog = - let tree_view = uriChoiceDialog#uriChoiceTreeView in - let column_list = new GTree.column_list in - let text_column = column_list#add Gobject.Data.string in - let list_store = GTree.list_store column_list in - let renderer = (GTree.cell_renderer_text [], ["text", text_column]) in - let view_column = GTree.view_column ~renderer () in - let _ = tree_view#set_model (Some (list_store :> GTree.model)) in - let _ = tree_view#append_column view_column in - object - method append s = - let tree_iter = list_store#append () in - list_store#set ~row:tree_iter ~column:text_column s - method clear () = list_store#clear () - end -*) - -open MathitaGeneratedGui -open MathitaGtkMisc - -class gui file = - (* creation order _is_ relevant for windows placement *) - let toolbar = new toolBarWin ~file () in - let main = new mainWin ~file () in - let about = new aboutWin ~file () in - let dialog = new genericDialog ~file () in - let uriChoice = new uriChoiceDialog ~file () in - let interpChoice = new interpChoiceDialog ~file () in - let fileSel = new fileSelectionWin ~file () in - let proof = new proofWin ~file () in - let keyBindingBoxes = (* event boxes which should receive global key events *) - [ toolbar#toolBarEventBox; proof#proofWinEventBox ] - in - let uriChoices = new stringListModel uriChoice#uriChoiceTreeView in - object (self) - 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 - - method uriChoices = uriChoices - - end - diff --git a/helm/mathita/mathitaGui.mli b/helm/mathita/mathitaGui.mli deleted file mode 100644 index 4dcc0a5d7..000000000 --- a/helm/mathita/mathitaGui.mli +++ /dev/null @@ -1,55 +0,0 @@ -(* 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 type stringListModel = - object - method clear: unit -> unit - method append: string -> unit - end -*) - - (** @param fname name of the Glade file describing the GUI *) -class gui : - string -> - object - - method setQuitCallback : (unit -> unit) -> unit - - method uriChoices: MathitaGtkMisc.stringListModel - - (** {2 Access to low-level GTK widgets} *) - - method about : MathitaGeneratedGui.aboutWin - method dialog : MathitaGeneratedGui.genericDialog - method fileSel : MathitaGeneratedGui.fileSelectionWin - method interpChoice : MathitaGeneratedGui.interpChoiceDialog - method main : MathitaGeneratedGui.mainWin - method proof : MathitaGeneratedGui.proofWin - method toolbar : MathitaGeneratedGui.toolBarWin - method uriChoice : MathitaGeneratedGui.uriChoiceDialog - - end - diff --git a/helm/matita/.cvsignore b/helm/matita/.cvsignore new file mode 100644 index 000000000..ef69ec2b7 --- /dev/null +++ b/helm/matita/.cvsignore @@ -0,0 +1,11 @@ +Makefile +buildTimeConf.ml +config.status +configure +config.log +autom4te.cache +matita +matita.opt +*.cm[aiox] +*.cmxa +*.[ao] diff --git a/helm/matita/.depend b/helm/matita/.depend new file mode 100644 index 000000000..d6894d903 --- /dev/null +++ b/helm/matita/.depend @@ -0,0 +1,9 @@ +matitaGeneratedGui.cmo: matitaGeneratedGui.cmi +matitaGeneratedGui.cmx: matitaGeneratedGui.cmi +matitaGtkMisc.cmo: matitaGtkMisc.cmi +matitaGtkMisc.cmx: matitaGtkMisc.cmi +matitaGui.cmo: matitaGeneratedGui.cmi matitaGtkMisc.cmi matitaGui.cmi +matitaGui.cmx: matitaGeneratedGui.cmx matitaGtkMisc.cmx matitaGui.cmi +matita.cmo: matitaGeneratedGui.cmi matitaGui.cmi +matita.cmx: matitaGeneratedGui.cmx matitaGui.cmx +matitaGui.cmi: matitaGeneratedGui.cmi matitaGtkMisc.cmi diff --git a/helm/matita/Makefile.in b/helm/matita/Makefile.in new file mode 100644 index 000000000..02686b0fb --- /dev/null +++ b/helm/matita/Makefile.in @@ -0,0 +1,53 @@ + +OCAMLFIND = @OCAMLFIND@ +CAMLP4O = @CAMLP4O@ +LABLGLADECC = @LABLGLADECC@ + +REQUIRES = lablgtk2.glade helm-registry +OCAML_FLAGS = -package "$(REQUIRES)" -pp $(CAMLP4O) +OCAML_THREADS_FLAGS = -thread +OCAML_DEBUG_FLAGS = +OCAMLC = $(OCAMLFIND) ocamlc $(OCAML_FLAGS) $(OCAML_THREADS_FLAGS) $(OCAML_DEBUG_FLAGS) +OCAMLOPT = $(OCAMLFIND) opt $(OCAML_FLAGS) $(OCAML_THREADS_FLAGS) $(OCAML_DEBUG_FLAGS) +OCAMLDEP = $(OCAMLFIND) ocamldep $(OCAML_FLAGS) +CMOS = \ + buildTimeConf.cmo \ + matitaGeneratedGui.cmo \ + matitaGtkMisc.cmo \ + matitaGui.cmo +CMXS = $(patsubst %.cmo,%.cmx,$(CMOS)) + +all: matita +opt: matita.opt + +matita: $(CMOS) matita.ml + $(OCAMLC) -linkpkg -o $@ $^ +matita.opt: $(CMXS) matita.ml + $(OCAMLOPT) -linkpkg -o $@ $^ + +matitaGeneratedGui.ml matitaGeneratedGui.mli: matita.glade + $(LABLGLADECC) $< > $@ + $(OCAMLC) -i matitaGeneratedGui.ml > matitaGeneratedGui.mli + +%.cmi: %.mli + $(OCAMLC) -c $< +%.cmo %.cmi: %.ml + $(OCAMLC) -c $< +%.cmx: %.ml + $(OCAMLOPT) -c $< + +clean: + rm -rf *.cma *.cmo *.cmi *.cmx *.cmxa *.a *.o matita matita.opt +distclean: clean + rm -f matitaGeneratedGui.ml matitaGeneratedGui.mli + rm -f config.log config.status configure Makefile buildTimeConf.ml + rm -f matita.glade.bak matita.gladep.bak + rm -rf autom4te.cache/ + +depend: matitaGeneratedGui.ml matitaGeneratedGui.mli + $(OCAMLDEP) *.ml *.mli > .depend + +include .depend + +.PHONY: all opt clean distclean depend + diff --git a/helm/matita/buildTimeConf.ml.in b/helm/matita/buildTimeConf.ml.in new file mode 100644 index 000000000..e69de29bb diff --git a/helm/matita/configure.ac b/helm/matita/configure.ac new file mode 100644 index 000000000..cc0c50349 --- /dev/null +++ b/helm/matita/configure.ac @@ -0,0 +1,31 @@ +AC_INIT(matita.ml) + +AC_CHECK_PROG(HAVE_OCAMLFIND, ocamlfind, yes, no) +if test $HAVE_OCAMLFIND = "yes"; then + OCAMLFIND="ocamlfind" +else + AC_MSG_ERROR(could not find ocamlfind) +fi + +AC_CHECK_PROG(HAVE_LABLGLADECC, lablgladecc2, yes, no) +if test $HAVE_LABLGLADECC = "yes"; then + LABLGLADECC="lablgladecc2" +else + AC_MSG_ERROR(could not find lablgladecc2) +fi + +AC_CHECK_PROG(HAVE_CAMLP4O, camlp4o, yes, no) +if test $HAVE_CAMLP4O = "yes"; then + CAMLP4O="camlp4o" +else + AC_MSG_ERROR(could not find camlp4o) +fi + +AC_SUBST(OCAMLFIND) +AC_SUBST(CAMLP4O) +AC_SUBST(LABLGLADECC) + +AC_OUTPUT([ + buildTimeConf.ml + Makefile +]) diff --git a/helm/matita/matita.conf.xml.sample b/helm/matita/matita.conf.xml.sample new file mode 100644 index 000000000..751fed97d --- /dev/null +++ b/helm/matita/matita.conf.xml.sample @@ -0,0 +1,7 @@ + + +
+ matita.glade + true +
+ diff --git a/helm/matita/matita.glade b/helm/matita/matita.glade new file mode 100644 index 000000000..6eba147fd --- /dev/null +++ b/helm/matita/matita.glade @@ -0,0 +1,1080 @@ + + + + + + + True + Matita + GTK_WINDOW_TOPLEVEL + GTK_WIN_POS_NONE + False + 800 + 600 + True + False + + + + True + False + 0 + + + + True + + + + True + _File + True + + + + + + + True + _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 + + + + + + + + + + + + True + _Edit + True + + + + + + True + _View + True + + + + + + + True + Show Button Bar + True + True + + + + + + True + Show Proof Window + True + False + + + + + + + + + + + True + Debug + True + + + + + + + True + 0 + True + + + + + + True + 1 + True + + + + + + True + 2 + True + + + + + + + + + + True + _Help + True + + + + + + + True + About... + True + + + + + + + + + 0 + False + False + + + + + + True + True + 450 + + + + True + GTK_POLICY_ALWAYS + GTK_POLICY_ALWAYS + GTK_SHADOW_NONE + GTK_CORNER_TOP_LEFT + + + + + + + True + False + + + + + + True + GTK_POLICY_NEVER + GTK_POLICY_ALWAYS + GTK_SHADOW_IN + GTK_CORNER_TOP_LEFT + + + + + + + True + True + + + + + 0 + True + True + + + + + + True + True + + + 0 + False + False + + + + + + + + Matita: current proof + GTK_WINDOW_TOPLEVEL + GTK_WIN_POS_NONE + False + 700 + 525 + True + False + + + + True + + + + True + GTK_POLICY_ALWAYS + GTK_POLICY_ALWAYS + GTK_SHADOW_NONE + GTK_CORNER_TOP_LEFT + + + + True + GTK_SHADOW_IN + + + + + + + + + + + + + + 10 + Select File + GTK_WINDOW_TOPLEVEL + GTK_WIN_POS_CENTER + True + True + False + True + + + + True + True + True + GTK_RELIEF_NORMAL + + + + + + True + True + True + GTK_RELIEF_NORMAL + + + + + + 130 + 450 + True + ToolBar + GTK_WINDOW_TOPLEVEL + GTK_WIN_POS_NONE + False + False + False + + + + True + + + + True + False + 0 + + + + True + GTK_BUTTONBOX_DEFAULT_STYLE + 0 + + + + 120 + True + True + True + button1 + True + GTK_RELIEF_NORMAL + + + + + + True + True + True + button2 + True + GTK_RELIEF_NORMAL + + + + + + True + True + True + button3 + True + GTK_RELIEF_NORMAL + + + + + + True + True + True + button4 + True + GTK_RELIEF_NORMAL + + + + + 0 + False + True + + + + + + True + + + 5 + False + True + + + + + + + + + + + + + + DUMMY + GTK_WINDOW_TOPLEVEL + GTK_WIN_POS_CENTER + True + False + False + True + + + + True + False + 0 + + + + True + GTK_BUTTONBOX_END + + + + 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 + + + + + + + + + + + + Matita: about + GTK_WINDOW_TOPLEVEL + GTK_WIN_POS_CENTER + True + False + False + True + + + + True + False + 0 + + + + True + GTK_BUTTONBOX_END + + + + True + True + True + gtk-ok + True + GTK_RELIEF_NORMAL + -5 + + + + + 0 + False + True + GTK_PACK_END + + + + + + + + + + + + 280 + 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 + False + 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 + + + + + + + + True + dialog1 + GTK_WINDOW_TOPLEVEL + GTK_WIN_POS_NONE + 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-ok + True + GTK_RELIEF_NORMAL + -5 + + + + + 0 + False + True + GTK_PACK_END + + + + + + + + + + + diff --git a/helm/matita/matita.gladep b/helm/matita/matita.gladep new file mode 100644 index 000000000..cc3340fc9 --- /dev/null +++ b/helm/matita/matita.gladep @@ -0,0 +1,8 @@ + + + + + Matita + matita + FALSE + diff --git a/helm/matita/matita.ml b/helm/matita/matita.ml new file mode 100644 index 000000000..5056a88a2 --- /dev/null +++ b/helm/matita/matita.ml @@ -0,0 +1,154 @@ +(* 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/ + *) + +exception Not_implemented of string +let not_implemented feature = raise (Not_implemented feature) + + (** exceptions whose content should be presented to the user *) +exception Failure of string +let error s = raise (Failure s) + +let _ = Helm_registry.load_from "matita.conf.xml" +let _ = GMain.Main.init () +let gui = new MatitaGui.gui (Helm_registry.get "matita.glade_file") + +let interactive_user_uri_choice + ~(selection_mode:[`MULTIPLE|`SINGLE]) ?(nonvars_button=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) && + (Helm_registry.get_bool "matita.auto_disambiguation") + then + Lazy.force only_constant_choices + else begin + let win = gui#uriChoice in + let choices = ref [] in + let chosen = ref false in + let use_only_constants = ref false in + win#uriChoiceDialog#set_title title; + win#uriChoiceLabel#set_text msg; + gui#uriChoices#list_store#clear (); + List.iter gui#uriChoices#easy_append uris; + win#uriChoiceConstantsButton#misc#set_sensitive nonvars_button; + let bye = ref (fun () -> ()) in + let id1 = + win#uriChoiceConstantsButton#connect#clicked (fun _ -> + use_only_constants := true; + !bye ()) + in + let id2 = + win#uriChoiceAutoButton#connect#clicked (fun _ -> + use_only_constants := true ; + Helm_registry.set_bool "matita.auto_disambiguation" true; + !bye ()) + in + let id3 = + win#uriChoiceSelectedButton#connect#clicked (fun _ -> + choices := gui#uriChoices#easy_selection (); + !bye ()) + in + bye := (fun () -> + win#uriChoiceDialog#misc#hide (); + win#uriChoiceConstantsButton#misc#disconnect id1; + win#uriChoiceAutoButton#misc#disconnect id2; + win#uriChoiceSelectedButton#misc#disconnect id3; + prerr_endline "quit"; + GMain.Main.quit ()); + win#uriChoiceDialog#show (); + GtkThread.main (); + if !use_only_constants then + Lazy.force only_constant_choices + else + match !choices with + | [] -> error "No choice" + | choices -> choices + end + +(* +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 +*) + +let debugDialog () = + let dialog = + new MatitaGeneratedGui.debug + ~file:(Helm_registry.get "matita.glade_file") () + in + let retval = ref None in + let return v = + retval := Some v; + dialog#debug#destroy (); + GMain.Main.quit () + in + ignore (dialog#debug#event#connect#delete (fun _ -> true)); + ignore (dialog#okbutton2#connect#clicked (fun _ -> return 1)); + ignore (dialog#cancelbutton2#connect#clicked (fun _ -> return 2)); + dialog#debug#show (); + GtkThread.main (); + (match !retval with None -> assert false | Some v -> v) + +let _ = + gui#main#debugMenuItem2#connect#activate (fun _ -> + prerr_endline (string_of_int (debugDialog ()))) + + (** quit program, possibly asking for confirmation *) +let quit () = GMain.Main.quit () +let _ = gui#setQuitCallback quit +let _ = + gui#main#debugMenuItem0#connect#activate (fun _ -> + let uris = + interactive_user_uri_choice + ~selection_mode:`MULTIPLE + ~nonvars_button:false + ~title:"titolo" + ~msg:"messaggio" + ["cic:/uno.con"; "cic:/due.var"; "cic:/tre.con"; "cic:/quattro.con"; + "cic:/cinque.var"] + in + List.iter prerr_endline uris; print_newline ()) +let _ = + gui#main#debugMenuItem1#connect#activate (fun _ -> + Helm_registry.set_bool "matita.auto_disambiguation" + (not (Helm_registry.get_bool "matita.auto_disambiguation"))) + +let _ = +(* gui#uriChoices#easy_append "pippo"; *) +(* gui#uriChoices#list_store#clear (); *) + GtkThread.main () + diff --git a/helm/matita/matitaGeneratedGui.ml b/helm/matita/matitaGeneratedGui.ml new file mode 100644 index 000000000..f912ef0f9 --- /dev/null +++ b/helm/matita/matitaGeneratedGui.ml @@ -0,0 +1,504 @@ +(* Automatically generated from matita.glade by lablgladecc *) + +class mainWin ?(file="matita.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 image40 = + new GMisc.image (GtkMisc.Image.cast + (Glade.get_widget_msg ~name:"image40" ~info:"GtkImage" xmldata)) + method image40 = image40 + 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 image41 = + new GMisc.image (GtkMisc.Image.cast + (Glade.get_widget_msg ~name:"image41" ~info:"GtkImage" xmldata)) + method image41 = image41 + val saveMenuItem = + new GMenu.image_menu_item (GtkMenu.ImageMenuItem.cast + (Glade.get_widget_msg ~name:"SaveMenuItem" ~info:"GtkImageMenuItem" xmldata)) + method saveMenuItem = saveMenuItem + val image42 = + new GMisc.image (GtkMisc.Image.cast + (Glade.get_widget_msg ~name:"image42" ~info:"GtkImage" xmldata)) + method image42 = image42 + val saveAsMenuItem = + new GMenu.image_menu_item (GtkMenu.ImageMenuItem.cast + (Glade.get_widget_msg ~name:"SaveAsMenuItem" ~info:"GtkImageMenuItem" xmldata)) + method saveAsMenuItem = saveAsMenuItem + val image43 = + new GMisc.image (GtkMisc.Image.cast + (Glade.get_widget_msg ~name:"image43" ~info:"GtkImage" xmldata)) + method image43 = image43 + 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 image44 = + new GMisc.image (GtkMisc.Image.cast + (Glade.get_widget_msg ~name:"image44" ~info:"GtkImage" xmldata)) + method image44 = image44 + 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 debugMenu = + new GMenu.menu_item (GtkMenu.MenuItem.cast + (Glade.get_widget_msg ~name:"DebugMenu" ~info:"GtkMenuItem" xmldata)) + method debugMenu = debugMenu + val debugMenu_menu = + new GMenu.menu (GtkMenu.Menu.cast + (Glade.get_widget_msg ~name:"DebugMenu_menu" ~info:"GtkMenu" xmldata)) + method debugMenu_menu = debugMenu_menu + val debugMenuItem0 = + new GMenu.menu_item (GtkMenu.MenuItem.cast + (Glade.get_widget_msg ~name:"DebugMenuItem0" ~info:"GtkMenuItem" xmldata)) + method debugMenuItem0 = debugMenuItem0 + val debugMenuItem1 = + new GMenu.menu_item (GtkMenu.MenuItem.cast + (Glade.get_widget_msg ~name:"DebugMenuItem1" ~info:"GtkMenuItem" xmldata)) + method debugMenuItem1 = debugMenuItem1 + val debugMenuItem2 = + new GMenu.menu_item (GtkMenu.MenuItem.cast + (Glade.get_widget_msg ~name:"DebugMenuItem2" ~info:"GtkMenuItem" xmldata)) + method debugMenuItem2 = debugMenuItem2 + 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="matita.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="matita.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="matita.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="matita.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="matita.glade") ?domain ?autoconnect(*=true*) () = + let xmldata = Glade.create ~file ~root:"AboutWin" ?domain () in + object (self) + inherit Glade.xml ?autoconnect xmldata + val toplevel : [`NONE | `DELETE_EVENT | `ID of int] GWindow.dialog = + new GWindow.dialog (GtkWindow.Dialog.cast + (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="matita.glade") ?domain ?autoconnect(*=true*) () = + let xmldata = Glade.create ~file ~root:"UriChoiceDialog" ?domain () in + object (self) + inherit Glade.xml ?autoconnect xmldata + val toplevel : [`NONE | `DELETE_EVENT | `ID of int] GWindow.dialog = + new GWindow.dialog (GtkWindow.Dialog.cast + (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="matita.glade") ?domain ?autoconnect(*=true*) () = + let xmldata = Glade.create ~file ~root:"InterpChoiceDialog" ?domain () in + object (self) + inherit Glade.xml ?autoconnect xmldata + val toplevel : [`NONE | `DELETE_EVENT | `ID of int] GWindow.dialog = + new GWindow.dialog (GtkWindow.Dialog.cast + (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 +class debug ?(file="matita.glade") ?domain ?autoconnect(*=true*) () = + let xmldata = Glade.create ~file ~root:"Debug" ?domain () in + object (self) + inherit Glade.xml ?autoconnect xmldata + val toplevel : [`NONE | `DELETE_EVENT | `ID of int] GWindow.dialog = + new GWindow.dialog (GtkWindow.Dialog.cast + (Glade.get_widget_msg ~name:"Debug" ~info:"GtkDialog" xmldata)) + method toplevel = toplevel + val debug : [`NONE | `DELETE_EVENT | `ID of int] GWindow.dialog = + new GWindow.dialog (GtkWindow.Dialog.cast + (Glade.get_widget_msg ~name:"Debug" ~info:"GtkDialog" xmldata)) + method debug = debug + val dialog_vbox5 = + new GPack.box (GtkPack.Box.cast + (Glade.get_widget_msg ~name:"dialog-vbox5" ~info:"GtkVBox" xmldata)) + method dialog_vbox5 = dialog_vbox5 + val cancelbutton2 = + new GButton.button (GtkButton.Button.cast + (Glade.get_widget_msg ~name:"cancelbutton2" ~info:"GtkButton" xmldata)) + method cancelbutton2 = cancelbutton2 + val okbutton2 = + new GButton.button (GtkButton.Button.cast + (Glade.get_widget_msg ~name:"okbutton2" ~info:"GtkButton" xmldata)) + method okbutton2 = okbutton2 + method reparent parent = + dialog_vbox5#misc#reparent parent; + toplevel#destroy () + method check_widgets () = () + end + +let check_all ?(show=false) () = + ignore (GMain.Main.init ()); + let debug = new debug () in + if show then debug#toplevel#show (); + debug#check_widgets (); + let 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/matita/matitaGeneratedGui.mli b/helm/matita/matitaGeneratedGui.mli new file mode 100644 index 000000000..6b72a8b27 --- /dev/null +++ b/helm/matita/matitaGeneratedGui.mli @@ -0,0 +1,309 @@ +class mainWin : + ?file:string -> + ?domain:string -> + ?autoconnect:bool -> + unit -> + object + val aboutMenuItem : GMenu.menu_item + val debugMenu : GMenu.menu_item + val debugMenuItem0 : GMenu.menu_item + val debugMenuItem1 : GMenu.menu_item + val debugMenuItem2 : GMenu.menu_item + val debugMenu_menu : GMenu.menu + 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 image40 : GMisc.image + val image41 : GMisc.image + val image42 : GMisc.image + val image43 : GMisc.image + val image44 : 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 debugMenu : GMenu.menu_item + method debugMenuItem0 : GMenu.menu_item + method debugMenuItem1 : GMenu.menu_item + method debugMenuItem2 : GMenu.menu_item + method debugMenu_menu : GMenu.menu + 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 image40 : GMisc.image + method image41 : GMisc.image + method image42 : GMisc.image + method image43 : GMisc.image + method image44 : 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 +class debug : + ?file:string -> + ?domain:string -> + ?autoconnect:bool -> + unit -> + object + val cancelbutton2 : GButton.button + val debug : [ `DELETE_EVENT | `ID of int | `NONE ] GWindow.dialog + val dialog_vbox5 : GPack.box + val okbutton2 : 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 cancelbutton2 : GButton.button + method check_widgets : unit -> unit + method debug : [ `DELETE_EVENT | `ID of int | `NONE ] GWindow.dialog + method dialog_vbox5 : 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 diff --git a/helm/matita/matitaGtkMisc.ml b/helm/matita/matitaGtkMisc.ml new file mode 100644 index 000000000..fc4fecc8f --- /dev/null +++ b/helm/matita/matitaGtkMisc.ml @@ -0,0 +1,77 @@ +(* 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)) + +class stringListModel (tree_view: GTree.view) = + let column_list = new GTree.column_list in + let text_column = column_list#add Gobject.Data.string in + let list_store = GTree.list_store column_list in + object (self) + + initializer + let renderer = (GTree.cell_renderer_text [], ["text", text_column]) in + let view_column = GTree.view_column ~renderer () in + tree_view#set_model (Some (list_store :> GTree.model)); + ignore (tree_view#append_column view_column) + + method list_store = list_store + + method easy_append s = + let tree_iter = list_store#append () in + list_store#set ~row:tree_iter ~column:text_column s + + method easy_insert pos s = + let tree_iter = list_store#insert pos in + list_store#set ~row:tree_iter ~column:text_column s + + method easy_selection () = + List.map + (fun tree_path -> + let iter = list_store#get_iter tree_path in + list_store#get ~row:iter ~column:text_column) + tree_view#selection#get_selected_rows + + end + diff --git a/helm/matita/matitaGtkMisc.mli b/helm/matita/matitaGtkMisc.mli new file mode 100644 index 000000000..03847ac87 --- /dev/null +++ b/helm/matita/matitaGtkMisc.mli @@ -0,0 +1,48 @@ +(* 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 + + (** single string column list *) +class stringListModel: + GTree.view -> + object + method list_store: GTree.list_store (** list_store forwarding *) + + method easy_append: string -> unit (** append + set *) + method easy_insert: int -> string -> unit (** insert + set *) + method easy_selection: unit -> string list + end + diff --git a/helm/matita/matitaGui.ml b/helm/matita/matitaGui.ml new file mode 100644 index 000000000..16af24434 --- /dev/null +++ b/helm/matita/matitaGui.ml @@ -0,0 +1,110 @@ +(* 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 stringListModel' uriChoiceDialog = + let tree_view = uriChoiceDialog#uriChoiceTreeView in + let column_list = new GTree.column_list in + let text_column = column_list#add Gobject.Data.string in + let list_store = GTree.list_store column_list in + let renderer = (GTree.cell_renderer_text [], ["text", text_column]) in + let view_column = GTree.view_column ~renderer () in + let _ = tree_view#set_model (Some (list_store :> GTree.model)) in + let _ = tree_view#append_column view_column in + object + method append s = + let tree_iter = list_store#append () in + list_store#set ~row:tree_iter ~column:text_column s + method clear () = list_store#clear () + end +*) + +open MatitaGeneratedGui +open MatitaGtkMisc + +class gui file = + (* creation order _is_ relevant for windows placement *) + let toolbar = new toolBarWin ~file () in + let main = new mainWin ~file () in + let about = new aboutWin ~file () in + let dialog = new genericDialog ~file () in + let uriChoice = new uriChoiceDialog ~file () in + let interpChoice = new interpChoiceDialog ~file () in + let fileSel = new fileSelectionWin ~file () in + let proof = new proofWin ~file () in + let keyBindingBoxes = (* event boxes which should receive global key events *) + [ toolbar#toolBarEventBox; proof#proofWinEventBox ] + in + let uriChoices = new stringListModel uriChoice#uriChoiceTreeView in + object (self) + 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 + + method uriChoices = uriChoices + + end + diff --git a/helm/matita/matitaGui.mli b/helm/matita/matitaGui.mli new file mode 100644 index 000000000..734f1cefe --- /dev/null +++ b/helm/matita/matitaGui.mli @@ -0,0 +1,55 @@ +(* 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 type stringListModel = + object + method clear: unit -> unit + method append: string -> unit + end +*) + + (** @param fname name of the Glade file describing the GUI *) +class gui : + string -> + object + + method setQuitCallback : (unit -> unit) -> unit + + method uriChoices: MatitaGtkMisc.stringListModel + + (** {2 Access to low-level GTK widgets} *) + + method about : MatitaGeneratedGui.aboutWin + method dialog : MatitaGeneratedGui.genericDialog + method fileSel : MatitaGeneratedGui.fileSelectionWin + method interpChoice : MatitaGeneratedGui.interpChoiceDialog + method main : MatitaGeneratedGui.mainWin + method proof : MatitaGeneratedGui.proofWin + method toolbar : MatitaGeneratedGui.toolBarWin + method uriChoice : MatitaGeneratedGui.uriChoiceDialog + + end +