X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fhbugs%2Fcommon%2Fhbugs_types.ml;h=ebfa179941430605e843045ad8761fb79151c798;hb=1fb8d0192e1f7ee891c53dc282c9c9f111e63e3c;hp=0e580886b567bdff500c3adeff6eb27cfead2dd3;hpb=3c1a6c534877f7b7266809e4d92de02c7f1ee9d4;p=helm.git

diff --git a/helm/hbugs/common/hbugs_types.ml b/helm/hbugs/common/hbugs_types.ml
index 0e580886b..ebfa17994 100644
--- a/helm/hbugs/common/hbugs_types.ml
+++ b/helm/hbugs/common/hbugs_types.ml
@@ -1,5 +1,7 @@
 (*
- *  Copyright (C) 2003, HELM Team.
+ * Copyright (C) 2003:
+ *    Stefano Zacchiroli <zack@cs.unibo.it>
+ *    for the HELM Team http://helm.cs.unibo.it/
  *
  *  This file is part of HELM, an Hypertextual, Electronic
  *  Library of Mathematics, developed at the Computer Science
@@ -21,7 +23,7 @@
  *  MA  02111-1307, USA.
  *
  *  For details, see the HELM World-Wide-Web page,
- *  http://cs.unibo.it/helm/.
+ *  http://helm.cs.unibo.it/
  *)
 
 type broker_id = string
@@ -30,13 +32,29 @@ type musing_id = string
 type tutor_id = string
 type tutor_dsc = tutor_id * string  (* tutor id, tutor description *)
 
-type state = string             (* TODO stato del proof assistant *)
+type state =  (* proof assitant's state: proof type, proof body, goal *)
+  string * string * int
 
-type hint = string              (* TODO consiglio per l'utente *)
-type hint_type = string              (* TODO consiglio per l'utente *)
+type hint =
+    (* tactics usage related hints *)
+  | Use_ring_Luke
+  | Use_fourier_Luke
+  | Use_reflexivity_Luke
+  | Use_symmetry_Luke
+  | Use_assumption_Luke
+  | Use_contradiction_Luke
+  | Use_exists_Luke
+  | Use_split_Luke
+  | Use_left_Luke
+  | Use_right_Luke
+  | Use_apply_Luke of string        (* use apply tactic on embedded term *)
+    (* hints list *)
+  | Hints of hint list
+
+type hint_type = string              (* TODO tipo di consiglio per l'utente *)
 
 type musing_result =
-  | Eureka of string            (* extra information, if any, parsed depending
+  | Eureka of hint            (* extra information, if any, parsed depending
                                 on tutor's hint_type *)
   | Sorry
 
@@ -44,6 +62,8 @@ type musing_result =
 type message =
 
   (* general purpose *)
+  | Help  (* help request *)
+  | Usage of string (* help response *)       (* usage string *)
   | Exception of string * string              (* name, value *)
 
   (* client -> broker *)
@@ -51,7 +71,8 @@ type message =
   | Unregister_client of client_id            (* client id *)
   | List_tutors of client_id                  (* client_id *)
   | Subscribe of client_id * tutor_id list    (* client id, tutor id list *)
-  | State_change of client_id * state         (* client_id, new state *)
+  | State_change of client_id * state option  (* client_id, new state *)
+  | Wow of client_id                          (* client_id *)
 
   (* tutor -> broker *)
   | Register_tutor of tutor_id * string * hint_type * string
@@ -79,4 +100,5 @@ type message =
   | Start_musing of broker_id * state         (* broker id, state *)
   | Abort_musing of broker_id * musing_id     (* broker id, musing id *)
   | Thanks of broker_id * musing_id           (* broker id, musing id *)
+  | Too_late of broker_id * musing_id         (* broker id, musing id *)