From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 16 Apr 2003 12:04:35 +0000 (+0000)
Subject: - support None state
X-Git-Tag: before_refactoring~18
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=ebccc569eb763c210602cd17790a5731c83fe5fb;p=helm.git

- support None state
- added (de)serialization of Too_late
---

diff --git a/helm/hbugs/common/hbugs_messages.ml b/helm/hbugs/common/hbugs_messages.ml
index 0cc0f1b1f..836008e40 100644
--- a/helm/hbugs/common/hbugs_messages.ml
+++ b/helm/hbugs/common/hbugs_messages.ml
@@ -148,10 +148,19 @@ let msg_of_string' s =
   | T_element "state_change" ->
       let state_node =
         try
-          find_element ~deeply:false "gTopLevelStatus" root
-        with Not_found -> raise (No_element_found "gTopLevelStatus")
+          Some (find_element ~deeply:false "gTopLevelStatus" root)
+        with Not_found -> None
       in
-      State_change (get_attr root "id", parse_state state_node)
+      State_change
+        (get_attr root "id",
+        match state_node with
+        | Some n ->
+            if n#sub_nodes = [] then  (* TODO don't trust all sub_nodes,
+                                      consider only element sub_nodes *)
+              None
+            else
+              Some (parse_state n)
+        | None -> None)
   | T_element "wow" -> Wow (get_attr root "id")
 
     (* tutor -> broker *)
@@ -211,6 +220,8 @@ let msg_of_string' s =
   | T_element "abort_musing" ->
       Abort_musing (get_attr root "id", get_attr root "musing_id")
   | T_element "thanks" -> Thanks (get_attr root "id", get_attr root "musing_id")
+  | T_element "too_late" ->
+      Too_late (get_attr root "id", get_attr root "musing_id")
 
   | _ -> raise (No_element_found s)
 
@@ -219,18 +230,17 @@ let msg_of_string s =
     msg_of_string' s
   with e -> raise (Parse_error (s, Printexc.to_string e))
 
-let pp_state (type_string, body_string, goal) =
-  (* ASSUMPTION: type_string and body_string are well formed XML document
-  contents (i.e. they don't contain heading <?xml ... ?> declaration nor DOCTYPE
-  one *)
-  let res =
+let pp_state = function
+  | Some (type_string, body_string, goal) ->
+    (* ASSUMPTION: type_string and body_string are well formed XML document
+    contents (i.e. they don't contain heading <?xml ... ?> declaration nor
+    DOCTYPE one *)
     "<gTopLevelStatus>\n" ^
     (sprintf "<CurrentGoal>%d</CurrentGoal>\n" goal) ^
     type_string ^ "\n" ^
     body_string ^ "\n" ^
     "</gTopLevelStatus>\n"
-  in
-  res
+  | None -> "<gTopLevelStatus />\n"
 
 let rec pp_hint = function
   | Use_ring_Luke -> sprintf "<ring />"
@@ -315,7 +325,8 @@ let string_of_msg = function
   | Tutor_registered id -> sprintf "<tutor_registered id=\"%s\" />" id
   | Tutor_unregistered id -> sprintf "<tutor_unregistered id=\"%s\" />" id
   | Start_musing (id, state) ->
-      sprintf "<start_musing id=\"%s\">%s</start_musing>" id (pp_state state)
+      sprintf "<start_musing id=\"%s\">%s</start_musing>"
+        id (pp_state (Some state))
   | Abort_musing (id, musing_id) ->
       sprintf "<abort_musing id=\"%s\" musing_id=\"%s\" />" id musing_id
   | Thanks (id, musing_id) ->
diff --git a/helm/hbugs/common/hbugs_messages.mli b/helm/hbugs/common/hbugs_messages.mli
index 85ffe66c9..642c0b0e2 100644
--- a/helm/hbugs/common/hbugs_messages.mli
+++ b/helm/hbugs/common/hbugs_messages.mli
@@ -45,5 +45,5 @@ val respond_exc: string -> string -> out_channel -> unit
 val parse_state:
   ('a Pxp_document.node Pxp_document.extension as 'a) Pxp_document.node ->
     (string * string * int)
-val pp_state: (string * string * int) -> string
+val pp_state: (string * string * int) option -> string