]> matita.cs.unibo.it Git - helm.git/blob - helm/ocaml/hbugs/hbugs_client.ml
Non exhaustive match fixed.
[helm.git] / helm / ocaml / hbugs / hbugs_client.ml
1 (*
2  * Copyright (C) 2003:
3  *    Stefano Zacchiroli <zack@cs.unibo.it>
4  *    for the HELM Team http://helm.cs.unibo.it/
5  *
6  *  This file is part of HELM, an Hypertextual, Electronic
7  *  Library of Mathematics, developed at the Computer Science
8  *  Department, University of Bologna, Italy.
9  *
10  *  HELM is free software; you can redistribute it and/or
11  *  modify it under the terms of the GNU General Public License
12  *  as published by the Free Software Foundation; either version 2
13  *  of the License, or (at your option) any later version.
14  *
15  *  HELM is distributed in the hope that it will be useful,
16  *  but WITHOUT ANY WARRANTY; without even the implied warranty of
17  *  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
18  *  GNU General Public License for more details.
19  *
20  *  You should have received a copy of the GNU General Public License
21  *  along with HELM; if not, write to the Free Software
22  *  Foundation, Inc., 59 Temple Place - Suite 330, Boston,
23  *  MA  02111-1307, USA.
24  *
25  *  For details, see the HELM World-Wide-Web page,
26  *  http://helm.cs.unibo.it/
27  *)
28
29 open Hbugs_common;;
30 open Hbugs_types;;
31 open Printf;;
32
33 exception Invalid_URL of string;;
34
35 let do_nothing _ = ();;
36
37 module SmartHbugs_client_gui =
38  struct
39   class ['a] oneColumnCList gtree_view ~column_type ~column_title
40   =
41    let obj =
42     ((Gobject.unsafe_cast gtree_view#as_widget) : Gtk.tree_view Gtk.obj) in
43    let columns = new GTree.column_list in
44    let col = columns#add column_type in
45    let vcol = GTree.view_column ~title:column_title ()
46     ~renderer:(GTree.cell_renderer_text[], ["text",col]) in
47    let store = GTree.list_store columns in
48    object(self)
49     inherit GTree.view obj
50     method clear = store#clear
51     method append (v : 'a) =
52      let row = store#append () in
53       store#set ~row ~column:col v;
54     method column = col
55     initializer
56      self#set_model (Some (store :> GTree.model)) ;
57      ignore (self#append_column vcol)
58    end
59
60   class ['a,'b] twoColumnsCList gtree_view ~column1_type ~column2_type
61    ~column1_title ~column2_title
62   =
63    let obj =
64     ((Gobject.unsafe_cast gtree_view#as_widget) : Gtk.tree_view Gtk.obj) in
65    let columns = new GTree.column_list in
66    let col1 = columns#add column1_type in
67    let vcol1 = GTree.view_column ~title:column1_title ()
68     ~renderer:(GTree.cell_renderer_text[], ["text",col1]) in
69    let col2 = columns#add column2_type in
70    let vcol2 = GTree.view_column ~title:column2_title ()
71     ~renderer:(GTree.cell_renderer_text[], ["text",col2]) in
72    let store = GTree.list_store columns in
73    object(self)
74     inherit GTree.view obj
75     method clear = store#clear
76     method append (v1 : 'a) (v2 : 'b) =
77      let row = store#append () in
78       store#set ~row ~column:col1 v1;
79       store#set ~row ~column:col2 v2
80     method column1 = col1
81     method column2 = col2
82     initializer
83      self#set_model (Some (store :> GTree.model)) ;
84      ignore (self#append_column vcol1) ;
85      ignore (self#append_column vcol2) ;
86    end
87
88   class subscribeWindow () =
89    object(self)
90     inherit Hbugs_client_gui.subscribeWindow ()
91     val mutable tutorsSmartCList = None
92     method tutorsSmartCList =
93      match tutorsSmartCList with
94         None -> assert false
95       | Some w -> w
96     initializer
97      tutorsSmartCList <-
98       Some
99        (new twoColumnsCList self#tutorsCList
100          ~column1_type:Gobject.Data.string ~column2_type:Gobject.Data.string
101          ~column1_title:"Id" ~column2_title:"Description")
102    end
103
104   class hbugsMainWindow () =
105    object(self)
106     inherit Hbugs_client_gui.hbugsMainWindow ()
107     val mutable subscriptionSmartCList = None
108     val mutable hintsSmartCList = None
109     method subscriptionSmartCList =
110      match subscriptionSmartCList with
111         None -> assert false
112       | Some w -> w
113     method hintsSmartCList =
114      match hintsSmartCList with
115         None -> assert false
116       | Some w -> w
117     initializer
118      subscriptionSmartCList <-
119       Some
120        (new oneColumnCList self#subscriptionCList
121          ~column_type:Gobject.Data.string ~column_title:"Description")
122     initializer
123      hintsSmartCList <-
124       Some
125        (new oneColumnCList self#hintsCList
126          ~column_type:Gobject.Data.string ~column_title:"Description")
127    end
128
129  end
130 ;;
131
132 class hbugsClient
133   ?(use_hint_callback: hint -> unit = do_nothing)
134   ?(describe_hint_callback: hint -> unit = do_nothing)
135   ?(destroy_callback: unit -> unit = do_nothing)
136   ()
137   =
138
139   let http_url_RE = Pcre.regexp "^(http://)?(.*):(\\d+)" in
140   let port_of_http_url url =
141     try
142       let subs = Pcre.extract ~rex:http_url_RE url in
143       int_of_string subs.(3)
144     with e -> raise (Invalid_URL url)
145   in
146
147   object (self)
148
149     val mainWindow = new SmartHbugs_client_gui.hbugsMainWindow ()
150     val subscribeWindow = new SmartHbugs_client_gui.subscribeWindow ()
151     val messageDialog = new Hbugs_client_gui.messageDialog ()
152     val myOwnId = Hbugs_id_generator.new_client_id ()
153     val mutable use_hint_callback = use_hint_callback
154     val mutable myOwnUrl = "localhost:49082"
155     val mutable brokerUrl = "localhost:49081"
156     val mutable brokerId: broker_id option = None
157       (* all available tutors, saved last time a List_tutors message was sent to
158       broker *)
159     val mutable availableTutors: tutor_dsc list = []
160     val mutable statusContext = None
161     val mutable subscribeWindowStatusContext = None
162     val mutable debug = false (* enable/disable debugging buttons *)
163     val mutable hints = []  (* actually available hints *)
164
165     initializer
166       self#initGui;
167       self#startLocalHttpDaemon ();
168       self#testLocalHttpDaemon ();
169       self#testBroker ();
170       self#registerToBroker ();
171       self#reconfigDebuggingButtons
172
173     method show = mainWindow#hbugsMainWindow#show
174     method hide = mainWindow#hbugsMainWindow#misc#hide
175
176     method setUseHintCallback callback =
177      use_hint_callback <- callback
178
179     method private debugButtons =
180       List.map
181         (fun (b: GButton.button) -> new GObj.misc_ops b#as_widget)
182         [ mainWindow#startLocalHttpDaemonButton;
183         mainWindow#testLocalHttpDaemonButton; mainWindow#testBrokerButton ]
184
185     method private initGui =
186
187         (* GUI: main window *)
188
189           (* ignore delete events so that hbugs window is closable only using
190           menu; on destroy (e.g. while quitting gTopLevel) self#quit is invoked
191           *)
192
193       ignore (mainWindow#hbugsMainWindow#event#connect#delete (fun _ -> true));
194       ignore (mainWindow#hbugsMainWindow#event#connect#destroy
195         (fun _ -> self#quit (); false));
196
197         (* GUI main window's menu *)
198       mainWindow#toggleDebuggingMenuItem#set_active debug;
199       ignore (mainWindow#toggleDebuggingMenuItem#connect#toggled
200         self#toggleDebug);
201
202         (* GUI: local HTTP daemon settings *)
203       ignore (mainWindow#clientUrlEntry#connect#changed
204         (fun _ -> myOwnUrl <- mainWindow#clientUrlEntry#text));
205       mainWindow#clientUrlEntry#set_text myOwnUrl;
206       ignore (mainWindow#startLocalHttpDaemonButton#connect#clicked
207         self#startLocalHttpDaemon);
208       ignore (mainWindow#testLocalHttpDaemonButton#connect#clicked
209         self#testLocalHttpDaemon);
210
211         (* GUI: broker choice *)
212       ignore (mainWindow#brokerUrlEntry#connect#changed
213         (fun _ -> brokerUrl <- mainWindow#brokerUrlEntry#text));
214       mainWindow#brokerUrlEntry#set_text brokerUrl;
215       ignore (mainWindow#testBrokerButton#connect#clicked self#testBroker);
216       mainWindow#clientIdLabel#set_text myOwnId;
217
218         (* GUI: client registration *)
219       ignore (mainWindow#registerClientButton#connect#clicked
220         self#registerToBroker);
221
222         (* GUI: subscriptions *)
223       ignore (mainWindow#showSubscriptionWindowButton#connect#clicked
224         (fun () ->
225           self#listTutors ();
226           subscribeWindow#subscribeWindow#show ()));
227
228       let get_selected_row_index () =
229        match mainWindow#hintsCList#selection#get_selected_rows with
230           [path] ->
231             (match GTree.Path.get_indices path with
232                 [|n|] -> n
233               | _ -> assert false)
234         | _ -> assert false
235       in
236         (* GUI: hints list *)
237       ignore (
238        let event_ops = new GObj.event_ops mainWindow#hintsCList#as_widget in
239         event_ops#connect#button_press
240          (fun event ->
241            if GdkEvent.get_type event = `TWO_BUTTON_PRESS then
242             use_hint_callback (self#hint (get_selected_row_index ())) ;
243            false));
244
245       ignore (mainWindow#hintsCList#selection#connect#changed
246        (fun () ->
247          describe_hint_callback (self#hint (get_selected_row_index ())))) ;
248
249         (* GUI: main status bar *)
250       let ctxt = mainWindow#mainWindowStatusBar#new_context "0" in
251       statusContext <- Some ctxt;
252       ignore (ctxt#push "Ready");
253
254         (* GUI: subscription window *)
255       subscribeWindow#tutorsCList#selection#set_mode `MULTIPLE;
256       ignore (subscribeWindow#subscribeWindow#event#connect#delete
257         (fun _ -> subscribeWindow#subscribeWindow#misc#hide (); true));
258       ignore (subscribeWindow#listTutorsButton#connect#clicked self#listTutors);
259       ignore (subscribeWindow#subscribeButton#connect#clicked
260         self#subscribeSelected);
261       ignore (subscribeWindow#subscribeAllButton#connect#clicked
262         self#subscribeAll);
263       (subscribeWindow#tutorsCList#get_column 0)#set_visible false;
264       let ctxt = subscribeWindow#subscribeWindowStatusBar#new_context "0" in
265       subscribeWindowStatusContext <- Some ctxt;
266       ignore (ctxt#push "Ready");
267
268         (* GUI: message dialog *)
269       ignore (messageDialog#messageDialog#event#connect#delete
270         (fun _ -> messageDialog#messageDialog#misc#hide (); true));
271       ignore (messageDialog#okDialogButton#connect#clicked
272         (fun _ -> messageDialog#messageDialog#misc#hide ()))
273
274     (* accessory methods *)
275
276       (** pop up a (modal) dialog window showing msg to the user *)
277     method private showDialog msg =
278       messageDialog#dialogLabel#set_text msg;
279       messageDialog#messageDialog#show ()
280       (** use showDialog to display an hbugs message to the user *)
281     method private showMsgInDialog msg =
282       self#showDialog (Hbugs_messages.string_of_msg msg)
283
284       (** create a new thread which sends msg to broker, wait for an answer and
285       invoke callback passing response message as argument *)
286     method private sendReq ?(wait = false) ~msg callback =
287       let thread () =
288         try
289           callback (Hbugs_messages.submit_req ~url:(brokerUrl ^ "/act") msg)
290         with 
291         | (Hbugs_messages.Parse_error (subj, reason)) as e ->
292             self#showDialog
293               (sprintf
294 "Parse_error, unable to fullfill request. Details follow.
295 Request: %s
296 Error: %s"
297                 (Hbugs_messages.string_of_msg msg) (Printexc.to_string e));
298         | (Unix.Unix_error _) as e ->
299             self#showDialog
300               (sprintf
301 "Can't connect to HBugs Broker
302 Url: %s
303 Error: %s"
304                 brokerUrl (Printexc.to_string e))
305         | e ->
306             self#showDialog
307               (sprintf "hbugsClient#sendReq: Uncaught exception: %s"
308                 (Printexc.to_string e))
309       in
310       let th = Thread.create thread () in
311       if wait then
312         Thread.join th
313       else ()
314
315       (** check if a broker is authenticated using its broker_id
316       [ Background: during client registration, client save broker_id of its
317       broker, further messages from broker are accepted only if they carry the
318       same broker id ] *)
319     method private isAuthenticated id =
320       match brokerId with
321       | None -> false
322       | Some broker_id -> (id = broker_id)
323
324     (* actions *)
325
326     method private startLocalHttpDaemon =
327         (* flatten an hint tree to an hint list *)
328       let rec flatten_hint = function
329         | Hints hints -> List.concat (List.map flatten_hint hints)
330         | hint -> [hint]
331       in
332       fun () ->
333       let callback req outchan =
334         try
335           (match Hbugs_messages.msg_of_string req#body with
336           | Help ->
337               Hbugs_messages.respond_msg
338                 (Usage "Local Http Daemon up and running!") outchan
339           | Hint (broker_id, hint) ->
340               if self#isAuthenticated broker_id then begin
341                 let received_hints = flatten_hint hint in
342                 List.iter
343                   (fun h ->
344                     (match h with Hints _ -> assert false | _ -> ());
345                     ignore(mainWindow#hintsSmartCList#append(string_of_hint h)))
346                   received_hints;
347                 hints <- hints @ received_hints;
348                 Hbugs_messages.respond_msg (Wow myOwnId) outchan
349               end else  (* msg from unauthorized broker *)
350                 Hbugs_messages.respond_exc "forbidden" broker_id outchan
351           | msg ->
352               Hbugs_messages.respond_exc
353                 "unexpected_msg" (Hbugs_messages.string_of_msg msg) outchan)
354         with (Hbugs_messages.Parse_error _) as e ->
355           Hbugs_messages.respond_exc
356             "parse_error" (Printexc.to_string e) outchan
357       in
358       let addr = "0.0.0.0" in (* TODO actually user specified "My URL" is used
359                               only as a value to be sent to broker, local HTTP
360                               daemon will listen on "0.0.0.0", port is parsed
361                               from My URL though *)
362       let httpDaemonThread () =
363         try
364           Http_daemon.start'
365             ~addr ~port:(port_of_http_url myOwnUrl) ~mode:`Single callback
366         with
367         | Invalid_URL url -> self#showDialog (sprintf "Invalid URL: \"%s\"" url)
368         | e ->
369             self#showDialog (sprintf "Can't start local HTTP daemon: %s"
370               (Printexc.to_string e))
371       in
372       ignore (Thread.create httpDaemonThread ())
373
374     method private testLocalHttpDaemon () =
375       try
376         let msg =
377           Hbugs_misc.http_post ~body:(Hbugs_messages.string_of_msg Help)
378             myOwnUrl
379         in
380         ignore msg
381 (*         self#showDialog msg *)
382       with
383       | Hbugs_misc.Malformed_URL url ->
384           self#showDialog
385             (sprintf
386               "Handshake with local HTTP daemon failed, Invalid URL: \"%s\""
387               url)
388       | Hbugs_misc.Malformed_HTTP_response res ->
389           self#showDialog
390             (sprintf
391     "Handshake with local HTTP daemon failed, can't parse HTTP response: \"%s\""
392               res)
393       | (Unix.Unix_error _) as e ->
394           self#showDialog
395             (sprintf
396               "Handshake with local HTTP daemon failed, can't connect: \"%s\""
397               (Printexc.to_string e))
398
399     method private testBroker () =
400       self#sendReq ~msg:Help
401         (function
402           | Usage _ -> ()
403           | unexpected_msg ->
404               self#showDialog
405                 (sprintf
406                   "Handshake with HBugs Broker failed, unexpected message:\n%s"
407                   (Hbugs_messages.string_of_msg unexpected_msg)))
408
409     method registerToBroker () =
410       (match brokerId with  (* undo previous registration, if any *)
411       | Some id -> self#unregisterFromBroker ()
412       | _ -> ());
413       self#sendReq ~msg:(Register_client (myOwnId, myOwnUrl))
414         (function
415           | Client_registered broker_id -> (brokerId <- Some broker_id)
416           | unexpected_msg ->
417               self#showDialog
418                 (sprintf "Client NOT registered, unexpected message:\n%s"
419                   (Hbugs_messages.string_of_msg unexpected_msg)))
420
421     method unregisterFromBroker () =
422       self#sendReq ~wait:true ~msg:(Unregister_client myOwnId)
423         (function
424           | Client_unregistered _ -> (brokerId <- None)
425           | unexpected_msg -> ())
426 (*
427               self#showDialog
428                 (sprintf "Client NOT unregistered, unexpected message:\n%s"
429                   (Hbugs_messages.string_of_msg unexpected_msg)))
430 *)
431
432     method stateChange new_state =
433       mainWindow#hintsSmartCList#clear ();
434       hints <- [];
435       self#sendReq
436         ~msg:(State_change (myOwnId, new_state))
437         (function
438           | State_accepted _ -> ()
439           | unexpected_msg ->
440               self#showDialog
441                 (sprintf "State NOT accepted by Hbugs, unexpected message:\n%s"
442                   (Hbugs_messages.string_of_msg unexpected_msg)))
443
444     method hint = List.nth hints
445
446     method private listTutors () =
447         (* wait is set to true just to make sure that after invoking listTutors
448         "availableTutors" is correctly filled *)
449       self#sendReq ~wait:true ~msg:(List_tutors myOwnId)
450         (function
451           | Tutor_list (_, descriptions) ->
452               availableTutors <-  (* sort accordingly to tutor description *)
453                 List.sort (fun (a,b) (c,d) -> compare (b,a) (d,c)) descriptions;
454               subscribeWindow#tutorsSmartCList#clear ();
455               List.iter
456                 (fun (id, dsc) ->
457                   ignore (subscribeWindow#tutorsSmartCList#append id dsc))
458                 availableTutors
459           | unexpected_msg ->
460               self#showDialog
461                 (sprintf "Can't list tutors, unexpected message:\n%s"
462                   (Hbugs_messages.string_of_msg unexpected_msg)))
463
464       (* low level used by subscribeSelected and subscribeAll *)
465     method private subscribe' tutors_id =
466       self#sendReq ~msg:(Subscribe (myOwnId, tutors_id))
467         (function
468           | (Subscribed (_, subscribedTutors)) as msg ->
469               let sort = List.sort compare in
470               mainWindow#subscriptionSmartCList#clear ();
471               List.iter
472                 (fun tutor_id ->
473                   ignore
474                     (mainWindow#subscriptionSmartCList#append
475                       ( try
476                           List.assoc tutor_id availableTutors
477                         with Not_found -> assert false )))
478                 tutors_id;
479               subscribeWindow#subscribeWindow#misc#hide ();
480               if sort subscribedTutors <> sort tutors_id then
481                 self#showDialog
482                   (sprintf "Subscription mismatch\n: %s"
483                     (Hbugs_messages.string_of_msg msg))
484           | unexpected_msg ->
485               mainWindow#subscriptionSmartCList#clear ();
486               self#showDialog
487                 (sprintf "Subscription FAILED, unexpected message:\n%s"
488                   (Hbugs_messages.string_of_msg unexpected_msg)))
489
490     method private subscribeSelected () =
491      let tutorsSmartCList = subscribeWindow#tutorsSmartCList in
492      let selectedTutors =
493        List.map
494         (fun p ->
495           tutorsSmartCList#model#get
496            ~row:(tutorsSmartCList#model#get_iter p)
497            ~column:tutorsSmartCList#column1)
498         tutorsSmartCList#selection#get_selected_rows
499      in
500       self#subscribe' selectedTutors
501
502     method subscribeAll () =
503       self#listTutors ();  (* this fills 'availableTutors' field *)
504       self#subscribe' (List.map fst availableTutors)
505
506     method private quit () =
507       self#unregisterFromBroker ();
508       destroy_callback ()
509
510       (** enable/disable debugging *)
511     method private setDebug value = debug <- value
512
513     method private reconfigDebuggingButtons =
514       List.iter (* debug value changed, reconfigure buttons *)
515         (fun (b: GObj.misc_ops) -> if debug then b#show () else b#hide ())
516         self#debugButtons;
517     
518     method private toggleDebug () =
519       self#setDebug (not debug);
520       self#reconfigDebuggingButtons
521
522   end
523 ;;
524