1 (* Copyright (C) 2004, HELM Team.
3 * This file is part of HELM, an Hypertextual, Electronic
4 * Library of Mathematics, developed at the Computer Science
5 * Department, University of Bologna, Italy.
7 * HELM is free software; you can redistribute it and/or
8 * modify it under the terms of the GNU General Public License
9 * as published by the Free Software Foundation; either version 2
10 * of the License, or (at your option) any later version.
12 * HELM is distributed in the hope that it will be useful,
13 * but WITHOUT ANY WARRANTY; without even the implied warranty of
14 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
15 * GNU General Public License for more details.
17 * You should have received a copy of the GNU General Public License
18 * along with HELM; if not, write to the Free Software
19 * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
22 * For details, see the HELM World-Wide-Web page,
23 * http://helm.cs.unibo.it/
28 open MatitaGeneratedGui
32 let gui_instance = ref None ;;
34 class console ~evbox ~phrase_sep ~packing ~paned () =
35 let console = MatitaConsole.console ~evbox ~phrase_sep ~packing ~paned () in
37 method clear = console#clear
38 method echo_error = console#echo_error
39 method echo_message = console#echo_message
40 method wrap_exn: 'a. (unit -> 'a) -> 'a option = console#wrap_exn
41 method choose_uri uris =
42 let g = match !gui_instance with None -> assert false | Some g -> g in
43 let ul = g#newUriDialog () in
45 let model = new stringListModel ul#uriChoiceTreeView in
46 List.iter model#easy_append uris;
47 ul#uriChoiceDialog#set_title "Hints";
48 ul#uriChoiceLabel#set_text "Suggested uris";
49 ul#uriChoiceAbortButton#misc#hide ();
50 ul#uriChoiceAutoButton#misc#hide ();
51 ul#uriChoiceConstantsButton#misc#hide ();
52 ul#hbox2#misc#hide ();
53 ul#uriChoiceTreeView#selection#set_mode
54 (`SINGLE :> Gtk.Tags.selection_mode);
55 let _ = ul#uriChoiceTreeView#selection#connect#changed
56 ~callback:(fun () -> ()) in
57 let _ = ul#toplevel#connect#destroy
58 ~callback:(fun () -> GMain.Main.quit ()) in
59 let choices = ref None in
60 let _ = ul#uriChoiceSelectedButton#connect#clicked
62 (match model#easy_selection () with
64 | [uri] -> choices := (Some uri)
66 ul#uriChoiceDialog#destroy ();
67 GMain.Main.quit ()) in
71 | None -> raise MatitaTypes.Cancel
73 method show = console#show
75 method console = console
79 (* creation order _is_ relevant for windows placement *)
80 let toolbar = new toolBarWin ~file () in
81 let main = new mainWin ~file () in
82 let about = new aboutWin ~file () in
83 let fileSel = new fileSelectionWin ~file () in
84 let script = new scriptWin ~file () in
85 let keyBindingBoxes = (* event boxes which should receive global key events *)
86 [ toolbar#toolBarEventBox; main#mainWinEventBox;
87 script#scriptWinEventBox; main#consoleEventBox ]
90 new console ~evbox:main#consoleEventBox
91 ~phrase_sep:BuildTimeConf.phrase_sep
92 ~packing:main#scrolledConsole#add ~paned:main#mainVPanes ()
95 val mutable chosen_file = None
98 (* glade's check widgets *)
99 List.iter (fun w -> w#check_widgets ())
100 (let c w = (w :> <check_widgets: unit -> unit>) in
101 [ c about; c fileSel; c main; c toolbar; c script ]);
103 List.iter (* global key bindings *)
104 (fun (key, callback) -> self#addKeyBinding key callback)
107 toggle_win ~check:main#showProofMenuItem proof#proofWin;
109 toggle_win ~check:main#showCheckMenuItem check#checkWin;
112 toggle_win ~check:main#showScriptMenuItem script#scriptWin;
113 GdkKeysyms._x, (fun () -> console#console#toggle ());
115 add_key_binding GdkKeysyms._Escape console#console#hide
116 main#consoleEventBox;
118 ignore (about#aboutWin#event#connect#delete (fun _ -> true));
119 ignore (main#aboutMenuItem#connect#activate (fun _ ->
120 about#aboutWin#show ()));
121 connect_button about#aboutDismissButton (fun _ ->
122 about#aboutWin#misc#hide ());
123 about#aboutLabel#set_label (Pcre.replace ~pat:"@VERSION@"
124 ~templ:BuildTimeConf.version about#aboutLabel#label);
125 (* file selection win *)
126 ignore (fileSel#fileSelectionWin#event#connect#delete (fun _ -> true));
127 ignore (fileSel#fileSelectionWin#connect#response (fun event ->
130 fileSel#fileSelectionWin#misc#hide ();
135 let fname = fileSel#fileSelectionWin#filename in
136 if is_regular fname then return (Some fname)
137 | `CANCEL -> return None
139 | `DELETE_EVENT -> return None));
142 toggle_visibility toolbar#toolBarWin main#showToolBarMenuItem;
144 toggle_visibility proof#proofWin main#showProofMenuItem;
145 toggle_visibility check#checkWin main#showCheckMenuItem;
147 toggle_visibility script#scriptWin main#showScriptMenuItem;
148 List.iter (fun w -> w#misc#set_sensitive false)
149 [ main#saveMenuItem; main#saveAsMenuItem ];
150 main#helpMenu#set_right_justified true;
151 ignore (main#showConsoleMenuItem#connect#activate console#console#toggle);
153 connect_button main#hideConsoleButton console#console#hide;
155 console#echo_message (sprintf "\tMatita version %s\n"
156 BuildTimeConf.version);
157 console#console#echo_prompt ();
158 console#console#misc#grab_focus ();
161 method console = (console :> MatitaTypes.console)
162 method fileSel = fileSel
164 method script = script
165 method toolbar = toolbar
167 method newBrowserWin () =
168 let win = new browserWin ~file () in
169 win#check_widgets ();
172 method newUriDialog () =
173 let dialog = new uriChoiceDialog ~file () in
174 dialog#check_widgets ();
177 method newInterpDialog () =
178 let dialog = new interpChoiceDialog ~file () in
179 dialog#check_widgets ();
182 method newConfirmationDialog () =
183 let dialog = new confirmationDialog ~file () in
184 dialog#check_widgets ();
187 method newEmptyDialog () =
188 let dialog = new emptyDialog ~file () in
189 dialog#check_widgets ();
192 method private addKeyBinding key callback =
193 List.iter (fun evbox -> add_key_binding key callback evbox)
196 method setQuitCallback callback =
197 ignore (main#toplevel#connect#destroy callback);
198 ignore (main#quitMenuItem#connect#activate callback);
199 self#addKeyBinding GdkKeysyms._q callback
201 method setPhraseCallback = console#console#set_callback
203 method chooseFile () =
204 fileSel#fileSelectionWin#show ();
208 method askText ?(title = "") ?(msg = "") () =
209 let dialog = new textDialog () in
210 dialog#textDialog#set_title title;
211 dialog#textDialogLabel#set_label msg;
212 let text = ref None in
215 dialog#textDialog#destroy ();
218 ignore (dialog#textDialog#event#connect#delete (fun _ -> true));
219 connect_button dialog#textDialogCancelButton (fun _ -> return None);
220 connect_button dialog#textDialogOkButton (fun _ ->
221 let text = dialog#textDialogTextView#buffer#get_text () in
223 dialog#textDialog#show ();
230 let g = new gui (Helm_registry.get "matita.glade_file") in
231 gui_instance := Some g;
234 let instance = singleton gui