3 * Stefano Zacchiroli <zack@cs.unibo.it>
4 * for the HELM Team http://helm.cs.unibo.it/
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.
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.
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.
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,
25 * For details, see the HELM World-Wide-Web page,
26 * http://helm.cs.unibo.it/
29 type broker_id = string
30 type client_id = string
31 type musing_id = string
32 type tutor_id = string
33 type tutor_dsc = tutor_id * string (* tutor id, tutor description *)
35 type state = string (* TODO stato del proof assistant *)
37 type hint = string (* TODO consiglio per l'utente *)
38 type hint_type = string (* TODO consiglio per l'utente *)
41 | Eureka of string (* extra information, if any, parsed depending
42 on tutor's hint_type *)
45 (* for each message, first component is an ID that identify the sender *)
49 | Help (* help request *)
50 | Usage of string (* help response *) (* usage string *)
51 | Exception of string * string (* name, value *)
53 (* client -> broker *)
54 | Register_client of client_id * string (* client id, client url *)
55 | Unregister_client of client_id (* client id *)
56 | List_tutors of client_id (* client_id *)
57 | Subscribe of client_id * tutor_id list (* client id, tutor id list *)
58 | State_change of client_id * state (* client_id, new state *)
61 | Register_tutor of tutor_id * string * hint_type * string
62 (* tutor id, tutor url, hint type,
64 | Unregister_tutor of tutor_id (* tutor id *)
65 | Musing_started of tutor_id * musing_id (* tutor id, musing id *)
66 | Musing_aborted of tutor_id * musing_id (* tutor id, musing id *)
67 | Musing_completed of tutor_id * musing_id * musing_result
68 (* tutor id, musing id, result *)
70 (* broker -> client *)
71 | Client_registered of broker_id (* broker id *)
72 | Client_unregistered of broker_id (* broker id *)
73 | Tutor_list of broker_id * tutor_dsc list (* broker id, tutor list *)
74 | Subscribed of broker_id * tutor_id list (* broker id, tutor list *)
75 | State_accepted of broker_id * musing_id list * musing_id list
76 (* broker id, stopped musing ids,
78 | Hint of broker_id * hint (* broker id, hint *)
81 | Tutor_registered of broker_id (* broker id *)
82 | Tutor_unregistered of broker_id (* broker id *)
83 | Start_musing of broker_id * state (* broker id, state *)
84 | Abort_musing of broker_id * musing_id (* broker id, musing id *)
85 | Thanks of broker_id * musing_id (* broker id, musing id *)