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/
26 exception Not_implemented of string
27 let not_implemented feature = raise (Not_implemented feature)
29 (** exceptions whose content should be presented to the user *)
30 exception Failure of string
31 let error s = raise (Failure s)
33 let _ = Helm_registry.load_from "matita.conf.xml"
34 let _ = GMain.Main.init ()
35 let gui = new MatitaGui.gui (Helm_registry.get "matita.glade_file")
37 let interactive_user_uri_choice
38 ~(selection_mode:[`MULTIPLE|`SINGLE]) ?(nonvars_button=false) ~title ~msg
41 let only_constant_choices =
44 (fun uri -> not (String.sub uri (String.length uri - 4) 4 = ".var"))
47 if (selection_mode <> `SINGLE) &&
48 (Helm_registry.get_bool "matita.auto_disambiguation")
50 Lazy.force only_constant_choices
52 let win = gui#uriChoice in
53 let choices = ref [] in
54 let chosen = ref false in
55 let use_only_constants = ref false in
56 win#uriChoiceDialog#set_title title;
57 win#uriChoiceLabel#set_text msg;
58 gui#uriChoices#list_store#clear ();
59 List.iter gui#uriChoices#easy_append uris;
60 win#uriChoiceConstantsButton#misc#set_sensitive nonvars_button;
61 let bye = ref (fun () -> ()) in
63 win#uriChoiceConstantsButton#connect#clicked (fun _ ->
64 use_only_constants := true;
68 win#uriChoiceAutoButton#connect#clicked (fun _ ->
69 use_only_constants := true ;
70 Helm_registry.set_bool "matita.auto_disambiguation" true;
74 win#uriChoiceSelectedButton#connect#clicked (fun _ ->
75 choices := gui#uriChoices#easy_selection ();
79 win#uriChoiceDialog#misc#hide ();
80 win#uriChoiceConstantsButton#misc#disconnect id1;
81 win#uriChoiceAutoButton#misc#disconnect id2;
82 win#uriChoiceSelectedButton#misc#disconnect id3;
85 win#uriChoiceDialog#show ();
87 if !use_only_constants then
88 Lazy.force only_constant_choices
91 | [] -> error "No choice"
96 module DisambiguateCallbacks =
98 let interactive_user_uri_choice =
99 assert false (* TODO *)
100 (* interactive_user_uri_choice *)
101 let interactive_interpretation_choice choices =
102 assert false (* TODO *)
103 let input_or_locate_uri ~title =
104 assert false (* TODO *)
110 new MatitaGeneratedGui.debug
111 ~file:(Helm_registry.get "matita.glade_file") ()
113 let retval = ref None in
116 dialog#debug#destroy ();
119 ignore (dialog#debug#event#connect#delete (fun _ -> true));
120 ignore (dialog#okbutton2#connect#clicked (fun _ -> return 1));
121 ignore (dialog#cancelbutton2#connect#clicked (fun _ -> return 2));
122 dialog#debug#show ();
124 (match !retval with None -> assert false | Some v -> v)
127 gui#main#debugMenuItem2#connect#activate (fun _ ->
128 prerr_endline (string_of_int (debugDialog ())))
130 (** quit program, possibly asking for confirmation *)
131 let quit () = GMain.Main.quit ()
132 let _ = gui#setQuitCallback quit
134 gui#main#debugMenuItem0#connect#activate (fun _ ->
136 interactive_user_uri_choice
137 ~selection_mode:`MULTIPLE
138 ~nonvars_button:false
141 ["cic:/uno.con"; "cic:/due.var"; "cic:/tre.con"; "cic:/quattro.con";
144 List.iter prerr_endline uris; print_newline ())
146 gui#main#debugMenuItem1#connect#activate (fun _ ->
147 Helm_registry.set_bool "matita.auto_disambiguation"
148 (not (Helm_registry.get_bool "matita.auto_disambiguation")))
151 (* gui#uriChoices#easy_append "pippo"; *)
152 (* gui#uriChoices#list_store#clear (); *)