X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fhbugs%2Fcommon%2Fhbugs_messages.ml;h=b320501ba70eb4b570a9ffae0f74d517c3425fdf;hb=1fb8d0192e1f7ee891c53dc282c9c9f111e63e3c;hp=c0f70948462badd3f2a6678a7fafea2e365ce758;hpb=4651ed901a51659c31dbcb9a8b4f75d17321be14;p=helm.git

diff --git a/helm/hbugs/common/hbugs_messages.ml b/helm/hbugs/common/hbugs_messages.ml
index c0f709484..b320501ba 100644
--- a/helm/hbugs/common/hbugs_messages.ml
+++ b/helm/hbugs/common/hbugs_messages.ml
@@ -33,9 +33,13 @@ open Pxp_dtd;;
 open Pxp_types;;
 open Pxp_yacc;;
 
-let debug = true;;
+let debug = 2;; (*  0 -> no debug
+                    1 -> waiting for an answer / answer received
+                    2 -> XML messages dumping
+                *)
 
 exception Attribute_not_found of string;;
+exception Empty_node;;  (** found a node with no _element_ children *)
 exception No_element_found of string;;
 exception Parse_error of string * string;;  (* parsing subject, reason *)
 exception Unexpected_message of message;;
@@ -47,17 +51,18 @@ let get_attr node name =
     | Value s -> s
     | _ -> raise Not_found)
   with Not_found -> raise (Attribute_not_found name)
+let assert_element n name =
+  match n#node_type with
+  | T_element n when n = name ->
+      ()
+  | _ -> raise (Parse_error ("", "Expected node: " ^ name))
 
   (** given a string representation of a proof asistant state (e.g. the first
   child of the XML root of a State_change or Start_musing message), build from
   it an HBugs view of a proof assistant state *)
 let parse_state (root: ('a node extension as 'a) node) =
-  let assert_element n name =
-    match n#node_type with
-    | T_element n when n = name ->
-        ()
-    | _ -> raise (Parse_error ("", "Expected node: " ^ name))
-  in
+  if (List.filter is_xml_element root#sub_nodes) = [] then
+    raise Empty_node;
   let buf = Buffer.create 10240 in
   let node_to_string (node: ('a node extension as 'a) node) =
     Buffer.clear buf;
@@ -69,15 +74,14 @@ let parse_state (root: ('a node extension as 'a) node) =
   let (goal_node, type_node, body_node) =
     try
       (find_element "CurrentGoal" root,
-       find_element "ConstantType" root,  (* TODO e' sempre ConstantType? *)
+       find_element "ConstantType" root,
        find_element "CurrentProof" root)
     with Not_found ->
       raise (Parse_error ("", "Malformed HBugs status XML document"))
   in
   assert_element root "gTopLevelStatus";
   assert_element goal_node "CurrentGoal";
-  assert_element type_node "ConstantType";  (* TODO: tutti gli xml 'type' hanno
-                                            come root element "ConstantType"? *)
+  assert_element type_node "ConstantType";
   assert_element body_node "CurrentProof";
   goal_node#write (`Out_buffer buf) `Enc_utf8;
   let (type_string, body_string) =
@@ -93,23 +97,29 @@ let parse_state (root: ('a node extension as 'a) node) =
 
   (** parse an hint from an XML node, XML node should have type 'T_element _'
   (the name is ignored), attributes on it are ignored *)
-let rec parse_hint node =
-  let child = node#nth_node 0 in
-  match child#node_type with
-  | T_element "ring" -> Use_ring_Luke
-  | T_element "fourier" -> Use_fourier_Luke
-  | T_element "reflexivity" -> Use_reflexivity_Luke
-  | T_element "symmetry" -> Use_symmetry_Luke
-  | T_element "assumption" -> Use_assumption_Luke
-  | T_element "contradiction" -> Use_contradiction_Luke
-  | T_element "exists" -> Use_exists_Luke
-  | T_element "split" -> Use_split_Luke
-  | T_element "left" -> Use_left_Luke
-  | T_element "right" -> Use_right_Luke
-  | T_element "apply" -> Use_apply_Luke node#data
-  | T_element "hints" ->
-      Hints (List.map parse_hint (List.filter is_xml_element node#sub_nodes))
-  | _ -> assert false
+let parse_hint node =
+ let rec parse_hint_node node =
+   match node#node_type with
+   | T_element "ring" -> Use_ring_Luke
+   | T_element "fourier" -> Use_fourier_Luke
+   | T_element "reflexivity" -> Use_reflexivity_Luke
+   | T_element "symmetry" -> Use_symmetry_Luke
+   | T_element "assumption" -> Use_assumption_Luke
+   | T_element "contradiction" -> Use_contradiction_Luke
+   | T_element "exists" -> Use_exists_Luke
+   | T_element "split" -> Use_split_Luke
+   | T_element "left" -> Use_left_Luke
+   | T_element "right" -> Use_right_Luke
+   | T_element "apply" -> Use_apply_Luke node#data
+   | T_element "hints" ->
+       Hints
+        (List.map parse_hint_node (List.filter is_xml_element node#sub_nodes))
+   | _ -> assert false (* CSC: should this assert false be a raise something? *)
+ in
+  match List.filter is_xml_element node#sub_nodes with
+     [node] -> parse_hint_node node
+   | _ -> assert false (* CSC: should this assert false be a raise something? *)
+
 let parse_hint_type n = n#data (* TODO parsare il possibile tipo di suggerimento *)
 let parse_tutor_dscs n =
   List.map
@@ -142,10 +152,14 @@ 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 -> (try Some (parse_state n) with Empty_node -> None)
+        | None -> None)
   | T_element "wow" -> Wow (get_attr root "id")
 
     (* tutor -> broker *)
@@ -205,6 +219,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)
 
@@ -213,18 +229,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 />"
@@ -309,7 +324,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) ->
@@ -320,7 +336,7 @@ let string_of_msg = function
 
   (* debugging function that dump on stderr the sent messages *)
 let dump_msg msg =
-  if debug then
+  if debug >= 2 then
     prerr_endline
       (sprintf "<SENDING_MESSAGE>\n%s\n</SENDING_MESSAGE>"
         (match msg with
@@ -330,11 +346,11 @@ let dump_msg msg =
 
 let submit_req ~url msg =
   dump_msg msg;
-  if debug then (prerr_string "Waiting for an answer ... "; flush stderr);
+  if debug >= 1 then (prerr_string "Waiting for an answer ... "; flush stderr);
   let res =
     msg_of_string (Hbugs_misc.http_post ~body:(string_of_msg msg) url)
   in
-  if debug then (prerr_string "answer received!\n"; flush stderr);
+  if debug >= 1 then (prerr_string "answer received!\n"; flush stderr);
   res
 ;;
 let return_xml_msg body outchan =