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 let _ = Helm_registry.load_from "mathita.conf.xml"
30 let _ = GMain.Main.init ()
31 let gui = new MathitaGui.gui (Helm_registry.get "mathita.glade_file")
34 let interactive_user_uri_choice
35 ~selection_mode:[`MULTIPLE|`SINGLE] ?(ok="Ok")
36 ?(enable_button_for_non_vars=false) ~title ~msg
39 let only_constant_choices =
42 (fun uri -> not (String.sub uri (String.length uri - 4) 4 = ".var"))
45 if selection_mode <> `SINGLE && !auto_disambiguation then
46 Lazy.force only_constant_choices
48 let choices = ref [] in
49 let chosen = ref false in
50 let use_only_constants = ref false in
51 gui#uriChoice#uriChoiceDialog#set_title title;
52 gui#uriChoice#uriChoiceLabel#set_text msg;
56 let expected_height = 18 * List.length uris in
57 let height = if expected_height > 400 then 400 else expected_height in
58 GList.clist ~columns:1 ~packing:scrolled_window#add
59 ~height ~selection_mode:(selection_mode :> Gtk.Tags.selection_mode) () in
60 let _ = List.map (function x -> clist#append [x]) uris in
62 GPack.hbox ~border_width:0
63 ~packing:(window#vbox#pack ~expand:false ~fill:false ~padding:5) () in
65 GMisc.label ~text:"None of the above. Try this one:"
66 ~packing:(hbox2#pack ~expand:false ~fill:false ~padding:5) () in
68 GEdit.entry ~editable:true
69 ~packing:(hbox2#pack ~expand:true ~fill:true ~padding:5) () in
71 GPack.hbox ~border_width:0 ~packing:window#action_area#add () in
73 GButton.button ~label:ok
74 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
75 let _ = okb#misc#set_sensitive false in
80 if enable_button_for_non_vars then
81 hbox#pack ~expand:false ~fill:false ~padding:5 w)
82 ~label:"Try constants only" () in
87 if enable_button_for_non_vars then
88 hbox#pack ~expand:false ~fill:false ~padding:5 w)
91 GButton.button ~label:"Check"
92 ~packing:(hbox#pack ~padding:5) () in
93 let _ = checkb#misc#set_sensitive false in
95 GButton.button ~label:"Abort"
96 ~packing:(hbox#pack ~expand:false ~fill:false ~padding:5) () in
98 let check_callback () =
99 assert (List.length !choices > 0) ;
100 check_window !choices
102 ignore (window#connect#destroy GMain.Main.quit) ;
103 ignore (cancelb#connect#clicked window#destroy) ;
105 (okb#connect#clicked (function () -> chosen := true ; window#destroy ())) ;
107 (nonvarsb#connect#clicked
109 use_only_constants := true ;
113 ignore (autob#connect#clicked (fun () ->
114 auto_disambiguation := true;
115 (rendering_window ())#set_auto_disambiguation true;
116 use_only_constants := true ;
119 ignore (checkb#connect#clicked check_callback) ;
121 (clist#connect#select_row
122 (fun ~row ~column ~event ->
123 checkb#misc#set_sensitive true ;
124 okb#misc#set_sensitive true ;
125 choices := (List.nth uris row)::!choices)) ;
127 (clist#connect#unselect_row
128 (fun ~row ~column ~event ->
130 List.filter (function uri -> uri != (List.nth uris row)) !choices)) ;
132 (manual_input#connect#changed
134 if manual_input#text = "" then
137 checkb#misc#set_sensitive false ;
138 okb#misc#set_sensitive false ;
139 clist#misc#set_sensitive true
143 choices := [manual_input#text] ;
144 clist#unselect_all () ;
145 checkb#misc#set_sensitive true ;
146 okb#misc#set_sensitive true ;
147 clist#misc#set_sensitive false
149 window#set_position `CENTER ;
153 if !use_only_constants then
154 Lazy.force only_constant_choices
156 if List.length !choices > 0 then !choices else raise NoChoice
164 module DisambiguateCallbacks =
166 let interactive_user_uri_choice =
167 assert false (* TODO *)
168 (* interactive_user_uri_choice *)
169 let interactive_interpretation_choice choices =
170 assert false (* TODO *)
171 let input_or_locate_uri ~title =
172 assert false (* TODO *)
176 (** quit program, possibly asking for confirmation *)
177 let quit () = GMain.Main.quit ()
178 let _ = gui#setQuitCallback quit
180 let _ = GtkThread.main ()