X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fhbugs%2Fcommon%2Fhbugs_types.ml;h=ebfa179941430605e843045ad8761fb79151c798;hb=d3c72d6856cd185e5b3e9f2e8b928b78c7031ed1;hp=f2b2f20189f372fe5be3f4bd5c3c87ad72c476ff;hpb=5d7d6bd5090f3f82279bef0b93b4b361a5b1d751;p=helm.git

diff --git a/helm/hbugs/common/hbugs_types.ml b/helm/hbugs/common/hbugs_types.ml
index f2b2f2018..ebfa17994 100644
--- a/helm/hbugs/common/hbugs_types.ml
+++ b/helm/hbugs/common/hbugs_types.ml
@@ -32,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
 
@@ -55,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
@@ -83,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 *)