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