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 = (* proof assitant's state: proof type, proof body, goal *)
39 (* tactics usage related hints *)
50 | Use_apply of string (* use apply tactic on embedded term *)
54 type hint_type = string (* TODO tipo di consiglio per l'utente *)
57 | Eureka of hint (* extra information, if any, parsed depending
58 on tutor's hint_type *)
61 (* for each message, first component is an ID that identify the sender *)
65 | Help (* help request *)
66 | Usage of string (* help response *) (* usage string *)
67 | Exception of string * string (* name, value *)
69 (* client -> broker *)
70 | Register_client of client_id * string (* client id, client url *)
71 | Unregister_client of client_id (* client id *)
72 | List_tutors of client_id (* client_id *)
73 | Subscribe of client_id * tutor_id list (* client id, tutor id list *)
74 | State_change of client_id * state option (* client_id, new state *)
75 | Wow of client_id (* client_id *)
78 | Register_tutor of tutor_id * string * hint_type * string
79 (* tutor id, tutor url, hint type,
81 | Unregister_tutor of tutor_id (* tutor id *)
82 | Musing_started of tutor_id * musing_id (* tutor id, musing id *)
83 | Musing_aborted of tutor_id * musing_id (* tutor id, musing id *)
84 | Musing_completed of tutor_id * musing_id * musing_result
85 (* tutor id, musing id, result *)
87 (* broker -> client *)
88 | Client_registered of broker_id (* broker id *)
89 | Client_unregistered of broker_id (* broker id *)
90 | Tutor_list of broker_id * tutor_dsc list (* broker id, tutor list *)
91 | Subscribed of broker_id * tutor_id list (* broker id, tutor list *)
92 | State_accepted of broker_id * musing_id list * musing_id list
93 (* broker id, stopped musing ids,
95 | Hint of broker_id * hint (* broker id, hint *)
98 | Tutor_registered of broker_id (* broker id *)
99 | Tutor_unregistered of broker_id (* broker id *)
100 | Start_musing of broker_id * state (* broker id, state *)
101 | Abort_musing of broker_id * musing_id (* broker id, musing id *)
102 | Thanks of broker_id * musing_id (* broker id, musing id *)
103 | Too_late of broker_id * musing_id (* broker id, musing id *)